IC3 -- flipping the E in ICE

DOI10.1007/978-3-319-52234-0_28zbMATH Open1484.68105OpenAlexW2574291663MaRDI QIDQ2961586FDOQ2961586

Authors: Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik 

Publication date: 21 February 2017

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

Full work available at URL: https://doi.org/10.1007/978-3-319-52234-0_28

Recommendations

• Understanding IC3
• HoIce: an ICE-based non-linear Horn clause solver
• Infinite-state invariant checking with IC3 and predicate abstraction
• A learning-based approach to synthesizing invariants for incomplete verification engines
• Invariant synthesis for incomplete verification engines

Mathematics Subject Classification ID

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

Cites Work

• Interpolation and SAT-based model checking.
• SAT-Based Model Checking without Unrolling
• A data driven approach for algebraic loop invariants

Cited In (5)

• HoIce: an ICE-based non-linear Horn clause solver
• SAT-based invariant inference and its relation to concept learning
• Understanding IC3
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants

This page was built for publication: IC3 -- flipping the E in ICE

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