NDLI: Dynamic transition relation simplification for bounded property checking

Content Provider	IEEE Xplore Digital Library
Author	Kuehlmann, A.
Copyright Year	2004
Description	Author affiliation: Cadence Berkeley Labs., CA, USA (Kuehlmann, A.)
Abstract	Bounded model checking (BMC) is an incomplete property checking method that is based on a finite unfolding of the transition relation to disprove the correctness of a set of properties or to prove them for a limited execution length from the initial states. Current BMC techniques repeatedly concatenate the original transition relation to unfold the circuit with increasing depths. In this paper we present a method that is based on a dual unfolding scheme. The first unfolding is non-initialized and progressively simplifies concatenated frames of the transition relation. The tail of the simplified frames is then applied in the second unfolding, which starts from the initial state and checks the properties. We use a circuit graph representation for all functions and perform simplification by merging vertices that are functionally equivalent under given input constraints. In the noninitialized unfolding, previous time frames progressively tighten these constraints thus leading to an asymptotic simplification of the transition relation. As a side benefit, our method can find inductive invariants constructively by detecting when vertices are functionally equivalent across time frames. This information is then used to further simplify the transition relation and, in some cases, prove unbounded correctness of properties. Our experiments using industrial property checking problems demonstrate that the presented method significantly improves the efficiency of BMC.
Starting Page	50
Ending Page	57
File Size	653065
Page Count	8
File Format	PDF
ISBN	0780387023
ISSN	10923152
DOI	10.1109/ICCAD.2004.1382542
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-11-07
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Circuits Concatenated codes Tail Merging Industrial relations Safety History Engines Heuristic algorithms Detection algorithms
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Computer Science Applications 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

Dynamic transition relation simplification for bounded property checking

Dynamic transition relation simplification for bounded property checking.

Dynamic transition relation simplification for bounded property checking (2004).

Improved net merging method for gate matrix layout

Efficient state merging in symbolic execution

Automatic Image Segmentation by Dynamic Region Merging

Timing driven gate duplication: complexity issues and algorithms

Accelerating high-level bounded model checking

Feature suppression based CAD mesh model simplification

Dynamic transition relation simplification for bounded property checking

Similar Documents

Dynamic transition relation simplification for bounded property checking

Dynamic transition relation simplification for bounded property checking.

Dynamic transition relation simplification for bounded property checking (2004).

Improved net merging method for gate matrix layout

Efficient state merging in symbolic execution

Automatic Image Segmentation by Dynamic Region Merging

Timing driven gate duplication: complexity issues and algorithms

Accelerating high-level bounded model checking

Feature suppression based CAD mesh model simplification

Dynamic transition relation simplification for bounded property checking