Dynamic Path Reduction for Software Model Checking

DOI10.1007/978-3-642-00255-7_22MaRDI QIDQ3605478zbMATH OpenOpenAlexFDO

Authors Zijiang Yang, Bashar al-Rawi, Karem A. Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu

Publication date 24 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00255-7_22

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

• Dynamic reductions for model checking concurrent software
• Dynamic partial-order reduction for model checking software
• Static analysis for state-space reductions preserving temporal logics
• Optimal dynamic partial order reduction
• scientific article; zbMATH DE number 1744960

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• Efficient SAT-based bounded model checking for software verification
• Interpolants and Symbolic Model Checking
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Whodunit? Causal Analysis for Counterexamples

Cited in

(5)

• Counterexample guided path reduction for static program analysis
• Dynamic partial-order reduction for model checking software
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Analysis of the infeasible path based on key branch
• Program analysis via satisfiability modulo path programs

Describes a project that uses

Uses Software

• STP
• DART
• veriSoft

This page was built for publication: Dynamic Path Reduction for Software Model Checking

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