ICP and IC3 with Stronger Generalization

Konferenz: MBMV 2021 - 24. Workshop MBMV
18.03.2021 - 19.03.2021 in online

Tagungsband: ITG-Fb. 296: MBMV 2021

Seiten: 12Sprache: EnglischTyp: PDF

Winterer, Felix; Seufert, Tobias; Scholl, Chritsoph; Becker, Bernd (University of Freiburg, Freiburg, Germany)
Scheibler, Karsten; Teige, Tino (BTC Embedded Systems AG, Oldenburg, Germany)

Most recently, IC3 was integrated into the SMT solver iSAT3. Thus, iSAT3+IC3 introduces the first IC3 variant based on interval abstraction and Interval Constraint Propagation (ICP). As strong generalization is one of the key aspects for the IC3 algorithm to be successful, we integrate two additional generalization schemes from literature into iSAT3+IC3: Inductive Generalization and Counterexamples To Generalization (CTG). Furthermore, we evaluate the benefits and the drawbacks of different variants of these methods in the context of interval abstraction and ICP.