IC3 -- flipping the E in ICE

DOI10.1007/978-3-319-52234-0_28MaRDI QIDQ2961586zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

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)