NDLI: Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking

Content Provider	IEEE Xplore Digital Library
Author	Cabodi, G. Garcia, L.A. Murciano, M. Nocco, S. Quer, S.
Copyright Year	1982
Abstract	Interpolant-based model checking has been shown to be effective on large verification instances, as it efficiently combines automated abstraction and reachability fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper, we propose an integrated approach which combines the abstraction power of interpolation with techniques that rely on and-inverter graph (AIG) and/or binary decision diagram (BDD) representations of states, directly supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG or BDD-based quantifications to limit and restrict the search space and the complexity of the interpolant-based approach. The exploited strategies, most of which are individually well known, are integrated with a new flavor, specifically designed to improve their effectiveness on difficult verification instances. Experimental results, specifically oriented to hard-to-solve verification problems, show the robustness of our approach.
Sponsorship	IEEE Council on Electronic Design Automation IEEE Circuits and Systems Society
Starting Page	382
Ending Page	395
Page Count	14
File Size	710790
File Format	PDF
ISSN	02780070
Volume Number	29
Issue Number	3
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2010-03-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Circuits Interpolation Data structures Boolean functions Formal verification Binary decision diagrams Robustness Hardware Concrete Logic symbolic techniques formal methods formal verification model checking satisfiability
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Electrical and Electronic Engineering Software

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

SAT-based unbounded symbolic model checking

On partitioning and symbolic model checking

Effect of improved lower bounds in dynamic BDD reordering

Symbolic model checking for sequential circuit verification

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement

An industrially effective environment for formal hardware verification

Analyzing Functional Coverage in Bounded Model Checking

Verification of Analog/Mixed-Signal Circuits Using Symbolic Methods

Optimizing symbolic model checking for statecharts

Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking

Similar Documents

SAT-based unbounded symbolic model checking

On partitioning and symbolic model checking

Effect of improved lower bounds in dynamic BDD reordering

Symbolic model checking for sequential circuit verification

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement

An industrially effective environment for formal hardware verification

Analyzing Functional Coverage in Bounded Model Checking

Verification of Analog/Mixed-Signal Circuits Using Symbolic Methods

Optimizing symbolic model checking for statecharts

Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking