×

Understanding IC3. (English) Zbl 1273.68222

Cimatti, Alessandro (ed.) et al., Theory and applications of satisfiability testing – SAT 2012. 15th international conference, Trento, Italy, June 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31611-1/pbk). Lecture Notes in Computer Science 7317, 1-14 (2012).
Summary: The recently introduced model checking algorithm, IC3, has proved to be among the best SAT-based safety model checkers. Many implementations now exist. This paper provides the context from which IC3 was developed and explains how the originator of the algorithm understands it. Then it draws parallels between IC3 and the subsequently developed algorithms, FAIR and IICTL, which extend IC3’s ideas to the analysis of \(\omega \)-regular and CTL properties, respectively. Finally, it draws attention to certain challenges that these algorithms pose for the SAT and SMT community.
For the entire collection see [Zbl 1268.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI