Top

Formal Methods in System Design

Published in:

08-12-2022

Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Authors: G. Cabodi, P. E. Camurati, M. Palena, P. Pasini

Published in: Formal Methods in System Design | Issue 2/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) A novel model checking algorithm; (2) A new and flexible way to handle an incremental representation of (over-approximated) forward reachable states. The new model checking algorithm IGR, Interpolation with Guided Refinement, partially takes inspiration from IC3 and interpolation sequences. It bases its robustness and scalability on incremental refinement of state sets, and guided unwinding/simplification of transition relation unrollings. State sets, the central data structure of our algorithm, are incrementally refined, and they represent a valuable information to be shared among related problems, either in concurrent or sequential (multiple-engine or multiple-property) execution schemes. We provide experimental data, showing that IGR extends the capability of a state-of-the-art model checker, with a specific focus on hard-to-prove properties.

next article Control strategies for off-line testing of timed systems

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

We use the notation \({\mathbf {F}}_{\mathbf {i}}\) instead of \(F_i\) to refer to a frame of \({\mathbf {F}}_{\mathbf {k}}\) that does not exists yet and that is being initialized for the first time.

Following [8], we heuristically increment cone bounds by more than 1, based on the depth of the previous ApproxFwdTrav run.

Cabodi G, Palena M, Pasini P (2014) Interpolation with guided refinement: Revisiting incrementality in sat-based unbounded model checking, In: Proceedings of the 14th conference on formal methods in computer-aided design, ser. FMCAD ’14. Austin, TX: FMCAD Inc, pp. 12:43–12:50. [Online]. Available: http://dl.acm.org/citation.cfm?id=2682923.2682938

Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symbol Logic 22(3):269–285MathSciNetCrossRefMATH

Lyndon RC (1959) An interpolation theorem in the predicate calculus. Pacific J Math 9(1):155–164MathSciNetCrossRefMATH

McMillan KL (2003) Interpolation and SAT-based model checking, In: Proceedings computer aided verification, ser. LNCS, vol. 2725. Boulder, CO, USA: Springer, pp. 1–13

Bradley AR (2011) Sat-based model checking without unrolling, In: VMCAI, Austin, Texas, Jan. 2011, pp. 70–87

Biere A, Jussila T The model checking competition web page, http://fmv.jku.at/hwmcc

McMillan KL, Jhala R (2005) Interpolation and SAT-based model checking, In: Proceedings computer aided verification, ser. LNCS, vol. 3725. Edinburgh, Scotland, UK: Springer, pp. 39–51

Marques-Silva J (2005) Improvements to the implementation of Interpolant–based model checking, In: Proceedings correct hardware design and verification methods, ser. LNCS, vol. 3725. Edinburgh, Scotland, UK: Springer, pp. 367–370

D’Silva V, Purandare M, Kroening D (2008) Approximation refinement for interpolation-based model checking, in verification, model checking and abstract interpretation, ser. Lecture Notes in Computer Science, vol. 4905. Springer, pp. 68–82

10.

Cabodi G, Murciano M, Nocco S, Quer S (2008) Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans Design Autom Electr Syst 13(1):309–340

11.

Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking, In: Proceedings international conference on computer-aided design. San Jose, California: ACM Press, Nov. pp. 129–136

12.

D’Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In: Proceedings of the 11th international conference on verification, model checking, and abstract interpretation, ser. VMCAI’10. Berlin, Heidelberg: Springer-Verlag, p. 129–145. [Online]. Available: https://doi.org/10.1007/978-3-642-11319-2_12

13.

Li B, Somenzi F (2006) Efficient abstraction refinement in interpolation-based unbounded model checking, In: Tools and algorithms for the construction and analysis of systems, vol. 3920, pp. 227–241

14.

Cabodi G, Loiacono C, Vendraminetto D (2013) Optimization techniques for Craig interpolant compaction in unbounded model checking, In: Proceedings design automation & test in Europe conference Grenoble, France: IEEE Computer Society, Mar. pp. 1417–1422

15.

Cabodi G, Loiacono C, Vendraminetto D (2015) Optimization techniques for Craig interpolant compaction in unbounded model checking. Form Methods Syst Des 46(2):135–162. https://doi.org/10.1007/s10703-015-0229-0CrossRefMATH

16.

Cabodi G, Camurati PE, Palena M, Pasini P, Vendraminetto D (2016) Reducing interpolant circuit size by ad-hoc logic synthesis and sat-based weakening. In: Proceedings of the 16th conference on formal methods in computer-aided design, ser. FMCAD ’16. Austin, TX: FMCAD Inc, pp. 25–32. [Online]. Available: http://dl.acm.org/citation.cfm?id=3077629.3077640

17.

Goldberg E, Güdemann M, Kroening D, Mukherjee R (2018) Efficient verification of multi-property designs (the benefit of wrong assumptions), In: 2018 Design, automation test in Europe Conference Exhibition (DATE), pp. 43–48

18.

Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement, In: CAV, pp. 154–169

19.

Gupta A, Ganai M, Yang Z, Ashar P (2003) Iterative abstraction using SAT-based BMC with proof analysis, In: Proceedings international conference on computer-aided design, San Jose, California, Nov. pp. 416–423

20.

Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver, In: Proceedings 38th design automation Conference Las Vegas, Nevada: IEEE Computer Society, Jun

21.

Eén N, Sörensson N (2009) The Minisat SAT solver, http://minisat.se, Apr

22.

Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs, In: Proceedings 36th design automation conference. New Orleans, Louisiana: IEEE Computer Society, Jun. pp. 317–320

23.

Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Proceedings formal methods in computer-aided design, ser. LNCS, vol. 2517. Austin, Texas, USA: Springer, Nov. pp. 1–8

24.

Cabodi G, Nocco S, Quer S (2011) Interpolation sequences revisited. In: Proceedings design automation & test in Europe conference Grenoble, France: IEEE Computer Society, Mar. pp. 316–322

25.

Vizel Y, Grumberg O, Shoham S (2013) Intertwined forward-backward reachability analysis using interpolants, In: Tools and algorithms for the construction and analysis of systems, ser. LNCS, vol. 7795. Rome, Italy: Springer, Mar. pp. 308–323

26.

Mishchenko A, Brayton RK (2005) SAT-Based complete Don’t-Care computation for network optimization, In: Proceedings design automation & test in Europe conferenece, pp. 412–417

27.

Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752–794. https://doi.org/10.1145/876638.876643MathSciNetCrossRefMATH

28.

Gupta A, Strichman O (2005) Abstraction refinement for bounded model checking. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 112–124. [Online]. Available: https://doi.org/10.1007/11513988_11

29.

Vizel Y, Grumberg SSO (2012) , Lazy abstraction and SAT-Based reachability in hardware model checking, In: Proceedings formal methods in computer-aided design. Cambridge, UK: IEEE, Oct. pp. 173–181

30.

Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods Syst Design 39(2):205–227CrossRefMATH

31.

Subramanyan P, Vizel Y, Ray S, Malik S (2015) Template-based synthesis of instruction-level abstractions for SOC verification, In: 2015 Formal methods in computer-aided design (FMCAD), pp. 160–167

32.

Baumgartner J, Aziz A (2003) An abstraction algorithm for the verification of level-sensitive latch-based netlists, Formal Methods in System Design, vol. 23, pp. 39–65, 07

33.

Cabodi G, Camurati P, Palena M, Pasini P” (2021) , Igr - experiments, https://github.com/P3900/igr-exp

34.

Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability, In: Proceedings of the 16th international conference on computer aided verification - Vol. 8559. New York, NY, USA: Springer-Verlag New York, Inc., pp. 260–276. [Online]. Available: https://doi.org/10.1007/978-3-319-08867-9_17

35.

Mishchenko A, Brayton R, Jiang J-HR, Jang S (2011) Scalable don’t-care-based logic optimization and resynthesis. ACM Trans Reconfigurable Technol Syst 4(4):1–23. https://doi.org/10.1145/2068716.2068720CrossRef

Title: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
Authors: G. Cabodi
P. E. Camurati
M. Palena
P. Pasini
Publication date: 08-12-2022
Publisher: Springer US
Published in: Formal Methods in System Design / Issue 2/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-022-00406-7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2022

Correction: Parameterized verification of leader/follower systems via first-order temporal logic

Assumption-based Runtime Verification

Specifiable robustness in reactive synthesis

Control strategies for off-line testing of timed systems

LTL model checking of self modifying code

Functional synthesis via input–output separation

Premium Partner