Probabilistic guarded commands mechanized in HOL

Probabilistic guarded commands mechanized in HOL

<p>The probabilistic guarded-command language (<em>pGCL</em>) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Hurd, J, McIver, A, Morgan, C
Formáid:	Journal article
Teanga:	English
Foilsithe / Cruthaithe:	Elsevier 2005
Ábhair:	Theory and automated verification

Míreanna comhchosúla

Partial correctness for probabilistic demonic programs
de réir: McIver, A, et al.
Foilsithe / Cruthaithe: (2001)

Forward looking logics and automata
de réir: Ley, C
Foilsithe / Cruthaithe: (2011)

Automated quantitative software verification
de réir: Kattenbelt, M
Foilsithe / Cruthaithe: (2010)

Intersection types and higer-order model checking
de réir: Ramsay, S, et al.
Foilsithe / Cruthaithe: (2014)

Precise verification of C programs
de réir: Lewis, M
Foilsithe / Cruthaithe: (2014)

Incremental modelling for verified communication architectures
de réir: Boehm, P, et al.
Foilsithe / Cruthaithe: (2011)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
de réir: Adams, S
Foilsithe / Cruthaithe: (2014)

An algebraic theory of componentised interaction
de réir: Chilton, C
Foilsithe / Cruthaithe: (2013)

Functions with local state: regularity and undecidability
de réir: Murawski, A
Foilsithe / Cruthaithe: (2005)

Game semantics based equivalence checking of higher-order programs
de réir: Hopkins, D, et al.
Foilsithe / Cruthaithe: (2012)

On learning assumptions for compositional verification of probabilistic systems
de réir: Feng, L
Foilsithe / Cruthaithe: (2014)

Repairing strings and trees
de réir: Riveros Jaeger, C
Foilsithe / Cruthaithe: (2013)

Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications
de réir: Baier, C, et al.
Foilsithe / Cruthaithe: (2022)

An interpolating decision procedure for transitive relations with uninterpreted functions
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2009)

Quantitative verification of real-time properties with application to medical devices
de réir: Marco Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
de réir: Haitao Wang, et al.
Foilsithe / Cruthaithe: (2021-01-01)

Abstract satisfaction
de réir: Haller, L
Foilsithe / Cruthaithe: (2013)

EL-ifying ontologies
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Pushing the boundaries of tractable ontology reasoning
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Static analyses over weak memory
de réir: Nimal, V, et al.
Foilsithe / Cruthaithe: (2014)

Tractable query answering for description logics via query rewriting
de réir: Perez-Urbina, H, et al.
Foilsithe / Cruthaithe: (2010)

Automated Verification of Building Components Using BIM Models and Point Clouds
de réir: Honti Richard, et al.
Foilsithe / Cruthaithe: (2020-09-01)

Decoding the Atmosphere: Optimising Probabilistic Forecasts with Information Gain
de réir: John R. Lawson, et al.
Foilsithe / Cruthaithe: (2024-04-01)

Verification of asynchronous concurrency and the shaped stack constraint
de réir: Kochems, J
Foilsithe / Cruthaithe: (2014)

Applications of process-oriented design
de réir: Whitehead, J, et al.
Foilsithe / Cruthaithe: (2014)

Program analysis with interpolants
de réir: Weissenbacher, G, et al.
Foilsithe / Cruthaithe: (2010)

Formal methods for the analysis of wireless network protocols
de réir: Fruth, M
Foilsithe / Cruthaithe: (2011)

A hierarchy of failures-based models: theory and application
de réir: Bolton, C, et al.
Foilsithe / Cruthaithe: (2005)

Reasoning about efficiency within a probabilistic calculus
de réir: McIver, A
Foilsithe / Cruthaithe: (1999)

Stateless HOL
de réir: Freek Wiedijk
Foilsithe / Cruthaithe: (2011-03-01)

Synthesis and alternating automata over real time
de réir: Jenkins, M, et al.
Foilsithe / Cruthaithe: (2012)

Topics in monitoring and planning for embedded real-time systems
de réir: Ho, H
Foilsithe / Cruthaithe: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Turba Tol Hol-Hol Tol. Venice, Italy, 2022
de réir: Alfredo Thiermann
Foilsithe / Cruthaithe: (2022-12-01)

Turba Tol Hol-Hol Tol. Venecia, Italia, 2022
de réir: Alfredo Thiermann
Foilsithe / Cruthaithe: (2022-12-01)

Reasoning about efficiency within a probabilistic μ-calculus
de réir: McIver, A
Foilsithe / Cruthaithe: (1999)

Automation Processes for Efficient Verification of Complex Systems: An Empirical Case Study
de réir: Rune Andre Haugen, et al.
Foilsithe / Cruthaithe: (2024-12-01)

AUTOMATION AND GAMIFICATION OF COMPUTER SCIENCE STUDY
de réir: Imre ZSIGMOND
Foilsithe / Cruthaithe: (2019-12-01)

Assessing Critical Adaptations in Automated Adaptive Software Systems by Stage Decomposition
de réir: Shuji Morisaki, et al.
Foilsithe / Cruthaithe: (2024-01-01)

STUDI KASUS LINGUSQL: APLIKASI TRANSAKSI PERDAGANGAN SAHAM
de réir: Rikky Wenang Purbojati, et al.
Foilsithe / Cruthaithe: (2012-07-01)