Understanding IC3

DOI10.1007/978-3-642-31612-8_1MaRDI QIDQ2843317zbMATH OpenOpenAlexFDO

Authors Aaron R. Bradley

Publication date 12 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-31612-8_1

Mathematics Subject Classification ID

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

Recommendations

• Generalized property directed reachability
• IC3 -- flipping the E in ICE
• Model checking with Boolean Satisfiability
• SAT solver management strategies in IC3: an experimental approach
• Hardware and Software, Verification and Testing

Cited in

(19)

• Model checking with multi-threaded IC3 portfolios
• Global guidance for local generalization in model checking
• Counterexample-preserving reduction for symbolic model checking
• IC3 -- flipping the E in ICE
• Verified AIG algorithms in ACL2
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• \textsf{PrIC3}: property directed reachability for MDPs
• Incremental design-space model checking via reusable reachable state approximations
• SAT-Based Model Checking
• Invariants for one-counter automata with disequality tests
• scientific article; zbMATH DE number 2079690 (Why is no real title available?)
• Generalized property directed reachability
• A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
• When is a formula a loop invariant?
• Learning inductive invariants by sampling from frequency distributions
• Combining Model Checking and Deduction
• Property directed reachability for generalized Petri nets
• Searching for i-good lemmas to accelerate safety model checking
• SAT solver management strategies in IC3: an experimental approach

This page was built for publication: Understanding IC3

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