Proof-guided underapproximation-widening for multi-process systems

DOI10.1145/1040305.1040316MaRDI QIDQ5276140zbMATH OpenOpenAlexFDO

Authors Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald

Publication date 14 July 2017

Published in Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1040305.1040316

zbMATH Keywords

abstractionbounded model checkingSAT proofssoftware verificationunderapproximation-widening

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Concurrent program verification with invariant-guided underapproximation
• Proof spaces for unbounded parallelism
• Towards SAT-based BMC for LTLK over interleaved interpreted systems
• Approximation Refinement for Interpolation-Based Model Checking

Cited in

(6)

• An approach for extracting a small unsatisfiable core
• Dynamic reductions for model checking concurrent software
• Widening with Thresholds for Programs with Complex Control Graphs
• Resolution proof transformation for compression and interpolation
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Underapproximation for model-checking based on universal circuits

This page was built for publication: Proof-guided underapproximation-widening for multi-process systems

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