A dynamic logic for deductive verification of multi-threaded programs

DOI10.1007/S00165-012-0261-4MaRDI QIDQ470007zbMATH OpenOpenAlexWikidataFDO

Authors 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

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

Recommendations

• A tool-supported proof system for multithreaded Java.
• Proof spaces for unbounded parallelism
• scientific article; zbMATH DE number 2080048
• An assertion-based proof system for multithreaded Java
• scientific article; zbMATH DE number 1670562

Cites work

• scientific article; zbMATH DE number 1693527 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• scientific article; zbMATH DE number 2080048 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
• An assertion-based proof system for multithreaded Java
• An axiomatic proof technique for parallel programs
• Atomizer: a dynamic atomicity checker for multithreaded programs
• Communication in concurrent dynamic logic
• Completing the temporal picture
• Concurrent dynamic logic
• Dynamic Logic with Non-rigid Functions
• Formal verification of parallel programs
• Hoare logic for Java in Isabelle/HOL
• KeY: A Formal Method for Object-Oriented Systems
• Model checking JAVA programs using JAVA PathFinder
• Proving assertions about parallel programs
• Refinement and retrenchment for programming language data types
• Space-reduction strategies for model checking dynamic software
• Symbolic execution and program testing
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Verifying Concurrent Systems with Symbolic Execution
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(4)

• Key-ABS: a deductive verification tool for the concurrent modelling language ABS
• A Temporal Logic for Multi-threaded Programs
• scientific article; zbMATH DE number 2080048 (Why is no real title available?)
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)

Describes a project that uses

Uses Software

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

This page was built for publication: A dynamic logic for deductive verification of multi-threaded programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q470007)