Partial correctness for probabilistic demonic programs

Partial correctness for probabilistic demonic programs

Recent work in sequential program semantics has produced both an operational (He et al., Sci. Comput. Programming 28(2, 3) (1997) 171–192) and an axiomatic (Morgan et al., ACM Trans. Programming Languages Systems 18(3) (1996) 325–353; Seidel et al., Tech Report PRG-TR-6-96, Programming Research grou...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	McIver, A, Morgan, C
Rannpháirtithe:	Plotkin, G
Formáid:	Journal article
Teanga:	English
Foilsithe / Cruthaithe:	Elsevier 2001
Ábhair:	Theory and automated verification Program development and tools

Míreanna comhchosúla

Probabilistic guarded commands mechanized in HOL
de réir: Hurd, J, et al.
Foilsithe / Cruthaithe: (2005)

Quantitative program logic and expected time bounds in probabilistic distributed algorithms
de réir: McIver, A
Foilsithe / Cruthaithe: (2002)

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

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

Monotonicity in shared-memory program verification
de réir: Kaiser, A
Foilsithe / Cruthaithe: (2013)

Program synthesis from domain specific object models
de réir: Faitelson, D
Foilsithe / Cruthaithe: (2008)

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

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

Techniques and tools for the verification of concurrent systems
de réir: Palikareva, H
Foilsithe / Cruthaithe: (2012)

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)

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

The formal semantics of a domain-specific modelling language
de réir: Grealish, C
Foilsithe / Cruthaithe: (2010)

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

Reasoning with !-graphs
de réir: Merry, A
Foilsithe / Cruthaithe: (2013)

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)

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)

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)

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

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

Higher-order semantics for quantum programming languages with classical control
de réir: Atzemoglou, GP
Foilsithe / Cruthaithe: (2012)

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)

TESTed—An educational testing framework with language-agnostic test suites for programming exercises
de réir: Niko Strijbol, et al.
Foilsithe / Cruthaithe: (2023-05-01)

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)

On Construction and Verification of PLC-Programs
de réir: E. V. Kuzmin, et al.
Foilsithe / Cruthaithe: (2015-02-01)

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

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
de réir: M. S. Ushakova, et al.
Foilsithe / Cruthaithe: (2015-08-01)

UCLAONT: Ontology-Based UML Class Models Verification Tool
de réir: Adel Rajab, et al.
Foilsithe / Cruthaithe: (2022-01-01)

Verificator: Educational Tool for Learning Programming
de réir: Danijel RADOSEVIC, et al.
Foilsithe / Cruthaithe: (2009-10-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)

Internet-Portal Of Organizational-Methodical Providing Distancionnikh Olympiads On Programirovaniyu.
de réir: B.N. Lyashenko, et al.
Foilsithe / Cruthaithe: (2009-11-01)