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

deductive verificationinput/ output reasoningmulti-threadingsymbolic executionsymmetry reduction

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• 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)

• A Temporal Logic for Multi-threaded Programs
• Key-ABS: a deductive verification tool for the concurrent modelling language ABS
• 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

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

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)