A dynamic logic for deductive verification of multi-threaded programs

DOI10.1007/s00165-012-0261-4zbMath1298.68165OpenAlexW2081764864MaRDI QIDQ470007

Bernhard Beckert, Vladimir Klebanov

Publication date: 11 November 2014

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0261-4

zbMATH Keywords

symmetry reductionsymbolic executionmulti-threadingdeductive verificationinput/ output reasoning

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• KRAKATOA
• JML
• Bogor
• ESC/Java
• Java PathFinder
• Atomizer

Cites Work

• Communication in concurrent dynamic logic
• Completing the temporal picture
• Proving assertions about parallel programs
• An axiomatic proof technique for parallel programs
• An assertion-based proof system for multithreaded Java
• Model checking JAVA programs using JAVA PathFinder
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Refinement and retrenchment for programming language data types
• Verifying Concurrent Systems with Symbolic Execution
• Atomizer
• A Marriage of Rely/Guarantee and Separation Logic
• Dynamic Logic with Non-rigid Functions
• Concurrent dynamic logic
• Formal verification of parallel programs
• Symbolic execution and program testing
• Hoare logic for Java in Isabelle/HOL
• Verifying safety properties of concurrent Java programs using 3-valued logic
• KeY: A Formal Method for Object-Oriented Systems
• A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item