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

Descrizione completa

Dettagli Bibliografici
Autori principali:	McIver, A, Morgan, C
Altri autori:	Plotkin, G
Natura:	Journal article
Lingua:	English
Pubblicazione:	Elsevier 2001
Soggetti:	Theory and automated verification Program development and tools

Documenti analoghi

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

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

Program analysis with interpolants
di: Weissenbacher, G, et al.
Pubblicazione: (2010)

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

Monotonicity in shared-memory program verification
di: Kaiser, A
Pubblicazione: (2013)

Program synthesis from domain specific object models
di: Faitelson, D
Pubblicazione: (2008)

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

Precise verification of C programs
di: Lewis, M
Pubblicazione: (2014)

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

Forward looking logics and automata
di: Ley, C
Pubblicazione: (2011)

Automated quantitative software verification
di: Kattenbelt, M
Pubblicazione: (2010)

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

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

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

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

Reasoning with !-graphs
di: Merry, A
Pubblicazione: (2013)

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

An algebraic theory of componentised interaction
di: Chilton, C
Pubblicazione: (2013)

Functions with local state: regularity and undecidability
di: Murawski, A
Pubblicazione: (2005)

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

Repairing strings and trees
di: Riveros Jaeger, C
Pubblicazione: (2013)

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

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

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

Abstract satisfaction
di: Haller, L
Pubblicazione: (2013)

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

EL-ifying ontologies
di: Carral, D, et al.
Pubblicazione: (2014)

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

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

Static analyses over weak memory
di: Nimal, V, et al.
Pubblicazione: (2014)

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

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

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

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

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

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

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

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

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

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