Dynamic Path Reduction for Software Model Checking

DOI10.1007/978-3-642-00255-7_22zbMATH Open1211.68103OpenAlexW1570017391MaRDI QIDQ3605478FDOQ3605478

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

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

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

• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Title not available (Why is that?)
• Interpolants and Symbolic Model Checking
• Whodunit? Causal Analysis for Counterexamples
• Efficient SAT-based bounded model checking for software verification

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

Uses Software

• veriSoft
• DART
• STP

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)