Space-reduction strategies for model checking dynamic software

zbMATH Open1271.68097MaRDI QIDQ2845504FDOQ2845504

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

Recommendations

• scientific article; zbMATH DE number 2087620
• Publication:4942017
• 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

Mathematics Subject Classification ID

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

Cites Work

• Algebraic laws for nondeterminism and concurrency
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lazy abstraction
• Thread-modular abstraction refinement.
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (9)

• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• TASS: the toolkit for accurate scientific software
• Title not available (Why is that?)

Uses Software

• Bogor
• SymmSpin
• Java PathFinder
• Bandera
• dSPIN

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)