Eager abstraction for symbolic model checking

DOI10.1007/978-3-319-96145-3_11MaRDI QIDQ6045004zbMATH OpenOpenAlexFDO

Authors K. L. McMillan

Publication date 26 May 2023

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

Full work available at URL https://doi.org/10.1007/978-3-319-96145-3_11

Mathematics Subject Classification ID

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

Cited in

(6)

• A symbolic semantics for abstract model checking
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Synthesizing history and prophecy variables for symbolic model checking
• Invariant checking for SMT-based systems with quantifiers

This page was built for publication: Eager abstraction for symbolic model checking

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