A system for compositional verification of asynchronous objects

DOI10.1016/j.scico.2010.08.003zbMath1264.68050OpenAlexW2016286256MaRDI QIDQ1951610

Maximilian Dylla, Wolfgang Ahrendt

Publication date: 6 June 2013

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.08.003

zbMATH Keywords

verificationsemanticsconcurrencyobject-orientation

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Modeling Actor Systems Using Dynamic I/O Automata ⋮ Verifying data- and control-oriented properties combining static and runtime verification: theory and tools ⋮ Compositional reasoning about active objects with shared futures ⋮ Observable behavior of distributed systems: component reasoning for concurrent objects ⋮ A sound and complete reasoning system for asynchronous communication with shared futures ⋮ Integrating deployment architectures and resource consumption in timed object-oriented models ⋮ Observable interface behaviour and inheritance ⋮ Validating Timed Models of Deployment Components with Parametric Concurrency

Uses Software

• KeY-C
• ANTLR
• KRAKATOA
• KeYmaera
• Why3
• Caduceus
• ESC/Java
• Boogie
• Creol
• ASMKeY

Cites Work

• Creol: A type-safe object-oriented model for distributed concurrent systems
• A calculus of communicating systems
• Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
• An axiomatic proof technique for parallel programs
• An assertion-based proof system for multithreaded Java
• Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
• Axiomatic semantics of communicating sequential processes
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• A Proof System for Communicating Sequential Processes
• Proofs of Networks of Processes
• The B-Book
• Mathematics of Program Construction
• Object-Oriented Specification and Open Distributed Systems
• Generating Unit Tests from Formal Proofs
• An axiomatic basis for computer programming
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A system for compositional verification of asynchronous objects