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

Descripció completa

Dades bibliogràfiques
Autors principals:	McIver, A, Morgan, C
Altres autors:	Plotkin, G
Format:	Journal article
Idioma:	English
Publicat:	Elsevier 2001
Matèries:	Theory and automated verification Program development and tools

Ítems similars

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

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

Program analysis with interpolants
per: Weissenbacher, G, et al.
Publicat: (2010)

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

Monotonicity in shared-memory program verification
per: Kaiser, A
Publicat: (2013)

Program synthesis from domain specific object models
per: Faitelson, D
Publicat: (2008)

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

Precise verification of C programs
per: Lewis, M
Publicat: (2014)

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

Forward looking logics and automata
per: Ley, C
Publicat: (2011)

Automated quantitative software verification
per: Kattenbelt, M
Publicat: (2010)

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

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

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

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

Reasoning with !-graphs
per: Merry, A
Publicat: (2013)

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

An algebraic theory of componentised interaction
per: Chilton, C
Publicat: (2013)

Functions with local state: regularity and undecidability
per: Murawski, A
Publicat: (2005)

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

Repairing strings and trees
per: Riveros Jaeger, C
Publicat: (2013)

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

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

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

Abstract satisfaction
per: Haller, L
Publicat: (2013)

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

EL-ifying ontologies
per: Carral, D, et al.
Publicat: (2014)

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

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

Static analyses over weak memory
per: Nimal, V, et al.
Publicat: (2014)

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

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

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

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

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

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

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

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

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

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