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

Bibliografski detalji
Glavni autori:	McIver, A, Morgan, C
Daljnji autori:	Plotkin, G
Format:	Journal article
Jezik:	English
Izdano:	Elsevier 2001
Teme:	Theory and automated verification Program development and tools

Slični predmeti

Probabilistic guarded commands mechanized in HOL
od: Hurd, J, i dr.
Izdano: (2005)

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

Program analysis with interpolants
od: Weissenbacher, G, i dr.
Izdano: (2010)

Predicate Abstraction of ANSI-C Programs Using SAT
od: Clarke, E, i dr.
Izdano: (2004)

Monotonicity in shared-memory program verification
od: Kaiser, A
Izdano: (2013)

Program synthesis from domain specific object models
od: Faitelson, D
Izdano: (2008)

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

Precise verification of C programs
od: Lewis, M
Izdano: (2014)

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

Forward looking logics and automata
od: Ley, C
Izdano: (2011)

Automated quantitative software verification
od: Kattenbelt, M
Izdano: (2010)

Intersection types and higer-order model checking
od: Ramsay, S, i dr.
Izdano: (2014)

Incremental modelling for verified communication architectures
od: Boehm, P, i dr.
Izdano: (2011)

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

Game semantics based equivalence checking of higher-order programs
od: Hopkins, D, i dr.
Izdano: (2012)

Reasoning with !-graphs
od: Merry, A
Izdano: (2013)

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

An algebraic theory of componentised interaction
od: Chilton, C
Izdano: (2013)

Functions with local state: regularity and undecidability
od: Murawski, A
Izdano: (2005)

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

Repairing strings and trees
od: Riveros Jaeger, C
Izdano: (2013)

An interpolating decision procedure for transitive relations with uninterpreted functions
od: Kroening, D, i dr.
Izdano: (2009)

Quantitative verification of real-time properties with application to medical devices
od: Marco Diciolla, M, i dr.
Izdano: (2014)

Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications
od: Baier, C, i dr.
Izdano: (2022)

Abstract satisfaction
od: Haller, L
Izdano: (2013)

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

EL-ifying ontologies
od: Carral, D, i dr.
Izdano: (2014)

Pushing the boundaries of tractable ontology reasoning
od: Carral, D, i dr.
Izdano: (2014)

TESTed—An educational testing framework with language-agnostic test suites for programming exercises
od: Niko Strijbol, i dr.
Izdano: (2023-05-01)

Static analyses over weak memory
od: Nimal, V, i dr.
Izdano: (2014)

Tractable query answering for description logics via query rewriting
od: Perez-Urbina, H, i dr.
Izdano: (2010)

Automated Verification of Building Components Using BIM Models and Point Clouds
od: Honti Richard, i dr.
Izdano: (2020-09-01)

On Construction and Verification of PLC-Programs
od: E. V. Kuzmin, i dr.
Izdano: (2015-02-01)

Decoding the Atmosphere: Optimising Probabilistic Forecasts with Information Gain
od: John R. Lawson, i dr.
Izdano: (2024-04-01)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
od: M. S. Ushakova, i dr.
Izdano: (2015-08-01)

UCLAONT: Ontology-Based UML Class Models Verification Tool
od: Adel Rajab, i dr.
Izdano: (2022-01-01)

Verificator: Educational Tool for Learning Programming
od: Danijel RADOSEVIC, i dr.
Izdano: (2009-10-01)

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

Applications of process-oriented design
od: Whitehead, J, i dr.
Izdano: (2014)

Internet-Portal Of Organizational-Methodical Providing Distancionnikh Olympiads On Programirovaniyu.
od: B.N. Lyashenko, i dr.
Izdano: (2009-11-01)