NDLI: Infinite-state invariant checking with IC3 and predicate abstraction

Content Provider	Springer Nature Link
Author	Cimatti, Alessandro Griggio, Alberto Mover, Sergio Tonetta, Stefa
Copyright Year	2016
Abstract	We address the problem of verifying invariant properties on infinite-state systems. We present a novel approach, IC3ia, for generalizing the IC3 invariant checking algorithm from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit Abstraction, a form of predicate abstraction that expresses abstract paths without computing explicitly the abstract system. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike previous SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available and are often highly inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.
Starting Page	190
Ending Page	218
Page Count	29
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	49
Issue Number	3
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2016-09-23
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Model checking Infinite-state systems IC3 Predicate abstraction SMT Inductive invariants Circuits and Systems Electrical Engineering Computer-Aided Engineering (CAD, CAE) and Design Software Engineering/Programming and Operating Systems
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On recursion-free Horn clauses and Craig interpolation

Action Language verifier: an infinite-state model checker for reactive software specifications

Verification of SpecC using predicate abstraction

From invariant checking to invariant inference using randomized search

An extension of lazy abstraction with interpolation for programs with arrays

SAT solver management strategies in IC3: an experimental approach

Bounded model checking of infinite state systems

Loop summarization using state and transition invariants

Predicate Abstraction of ANSI-C Programs Using SAT

Infinite-state invariant checking with IC3 and predicate abstraction

Similar Documents

On recursion-free Horn clauses and Craig interpolation

Action Language verifier: an infinite-state model checker for reactive software specifications

Verification of SpecC using predicate abstraction

From invariant checking to invariant inference using randomized search

An extension of lazy abstraction with interpolation for programs with arrays

SAT solver management strategies in IC3: an experimental approach

Bounded model checking of infinite state systems

Loop summarization using state and transition invariants

Predicate Abstraction of ANSI-C Programs Using SAT

Infinite-state invariant checking with IC3 and predicate abstraction