Space-reduction strategies for model checking dynamic software

MaRDI QIDQ2845504zbMATH OpenFDO

Authors Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif

Publication date 30 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S157106610580009X

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2087620
• scientific article; zbMATH DE number 1418460
• scientific article; zbMATH DE number 2087512
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• Dynamic reductions for model checking concurrent software

Cites work

• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 1744960 (Why is no real title available?)
• scientific article; zbMATH DE number 2087620 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• Algebraic laws for nondeterminism and concurrency
• Lazy abstraction
• Thread-modular abstraction refinement.

Cited in

(9)

• scientific article; zbMATH DE number 1744960 (Why is no real title available?)
• scientific article; zbMATH DE number 2087620 (Why is no real title available?)
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
• Model Checking Software
• Dynamic reductions for model checking concurrent software
• A dynamic logic for deductive verification of multi-threaded programs
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• TASS: the toolkit for accurate scientific software
• scientific article; zbMATH DE number 2087512 (Why is no real title available?)

Describes a project that uses

Uses Software

• dSPIN
• Bandera
• Java PathFinder
• SymmSpin
• Bogor

This page was built for publication: Space-reduction strategies for model checking dynamic software

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