Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions

DOI10.1007/11817963_28MaRDI QIDQ5756735zbMATH OpenOpenAlexFDO

Authors Vineet Kahlon, Aarti Gupta, Nishant Sinha

Publication date 5 September 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11817963_28

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Symbolic model checking of software
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• Combining partial-order reductions with on-the-fly model-checking.
• Dynamic reductions for model checking concurrent software
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique

Cited in

(16)

• Partial order reduction for deep bug finding in synchronous hardware
• Hybrid analysis for partial order reduction of programs with arrays
• Software model checking with explicit scheduler and symbolic threads
• Efficient symbolic model checking of software using partial disjunctive partitioning
• Dynamic reductions for model checking concurrent software
• An automata-theoretic approach to infinite-state systems
• Sequentialization using timestamps
• On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
• Model Checking Software
• Symbolic partial-order execution for testing multi-threaded programs
• Model Checking Software
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• Boosting Lazy Abstraction for SystemC with Partial Order Reduction
• Model Checking Software
• Extracting safe thread schedules from incomplete model checking results
• Symbolic model checking of software

Describes a project that uses

Uses Software

• veriSoft
• Zing

This page was built for publication: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions

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