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...

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	McIver, A, Morgan, C
Awduron Eraill:	Plotkin, G
Fformat:	Journal article
Iaith:	English
Cyhoeddwyd:	Elsevier 2001
Pynciau:	Theory and automated verification Program development and tools

Eitemau Tebyg

Probabilistic guarded commands mechanized in HOL
gan: Hurd, J, et al.
Cyhoeddwyd: (2005)

Quantitative program logic and expected time bounds in probabilistic distributed algorithms
gan: McIver, A
Cyhoeddwyd: (2002)

Program analysis with interpolants
gan: Weissenbacher, G, et al.
Cyhoeddwyd: (2010)

Predicate Abstraction of ANSI-C Programs Using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Monotonicity in shared-memory program verification
gan: Kaiser, A
Cyhoeddwyd: (2013)

Program synthesis from domain specific object models
gan: Faitelson, D
Cyhoeddwyd: (2008)

Formal methods for the analysis of wireless network protocols
gan: Fruth, M
Cyhoeddwyd: (2011)

Precise verification of C programs
gan: Lewis, M
Cyhoeddwyd: (2014)

Techniques and tools for the verification of concurrent systems
gan: Palikareva, H
Cyhoeddwyd: (2012)

Forward looking logics and automata
gan: Ley, C
Cyhoeddwyd: (2011)

Automated quantitative software verification
gan: Kattenbelt, M
Cyhoeddwyd: (2010)

Intersection types and higer-order model checking
gan: Ramsay, S, et al.
Cyhoeddwyd: (2014)

Incremental modelling for verified communication architectures
gan: Boehm, P, et al.
Cyhoeddwyd: (2011)

The formal semantics of a domain-specific modelling language
gan: Grealish, C
Cyhoeddwyd: (2010)

Game semantics based equivalence checking of higher-order programs
gan: Hopkins, D, et al.
Cyhoeddwyd: (2012)

Reasoning with !-graphs
gan: Merry, A
Cyhoeddwyd: (2013)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
gan: Adams, S
Cyhoeddwyd: (2014)

An algebraic theory of componentised interaction
gan: Chilton, C
Cyhoeddwyd: (2013)

Functions with local state: regularity and undecidability
gan: Murawski, A
Cyhoeddwyd: (2005)

On learning assumptions for compositional verification of probabilistic systems
gan: Feng, L
Cyhoeddwyd: (2014)

Repairing strings and trees
gan: Riveros Jaeger, C
Cyhoeddwyd: (2013)

An interpolating decision procedure for transitive relations with uninterpreted functions
gan: Kroening, D, et al.
Cyhoeddwyd: (2009)

Quantitative verification of real-time properties with application to medical devices
gan: Marco Diciolla, M, et al.
Cyhoeddwyd: (2014)

Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications
gan: Baier, C, et al.
Cyhoeddwyd: (2022)

Abstract satisfaction
gan: Haller, L
Cyhoeddwyd: (2013)

Higher-order semantics for quantum programming languages with classical control
gan: Atzemoglou, GP
Cyhoeddwyd: (2012)

EL-ifying ontologies
gan: Carral, D, et al.
Cyhoeddwyd: (2014)

Pushing the boundaries of tractable ontology reasoning
gan: Carral, D, et al.
Cyhoeddwyd: (2014)

TESTed—An educational testing framework with language-agnostic test suites for programming exercises
gan: Niko Strijbol, et al.
Cyhoeddwyd: (2023-05-01)

Static analyses over weak memory
gan: Nimal, V, et al.
Cyhoeddwyd: (2014)

Tractable query answering for description logics via query rewriting
gan: Perez-Urbina, H, et al.
Cyhoeddwyd: (2010)

Automated Verification of Building Components Using BIM Models and Point Clouds
gan: Honti Richard, et al.
Cyhoeddwyd: (2020-09-01)

On Construction and Verification of PLC-Programs
gan: E. V. Kuzmin, et al.
Cyhoeddwyd: (2015-02-01)

Decoding the Atmosphere: Optimising Probabilistic Forecasts with Information Gain
gan: John R. Lawson, et al.
Cyhoeddwyd: (2024-04-01)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
gan: M. S. Ushakova, et al.
Cyhoeddwyd: (2015-08-01)

UCLAONT: Ontology-Based UML Class Models Verification Tool
gan: Adel Rajab, et al.
Cyhoeddwyd: (2022-01-01)

Verificator: Educational Tool for Learning Programming
gan: Danijel RADOSEVIC, et al.
Cyhoeddwyd: (2009-10-01)

Verification of asynchronous concurrency and the shaped stack constraint
gan: Kochems, J
Cyhoeddwyd: (2014)

Applications of process-oriented design
gan: Whitehead, J, et al.
Cyhoeddwyd: (2014)

Internet-Portal Of Organizational-Methodical Providing Distancionnikh Olympiads On Programirovaniyu.
gan: B.N. Lyashenko, et al.
Cyhoeddwyd: (2009-11-01)