NDLI: Before and after vacuity

Content Provider	Springer Nature Link
Author	Chockler, Hana Strichman, Ofer
Copyright Year	2008
Abstract	In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such “meaningless” passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers.We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving two types of information that are not provided by standard vacuity checks, assuming $M\models\varphi$ for a model M and formula φ: (a) behaviors that are possibly missing from M (or wrongly restricted by the environment) (b) the largest subset of occurrences of literals in φ that can be replaced with false simultaneously without falsifying φ in M. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors.
Starting Page	37
Ending Page	58
Page Count	22
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	34
Issue Number	1
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2008-11-12
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Vacuity Model-checking Complexity Software Engineering/Programming and Operating Systems Computer-Aided Engineering (CAD, CAE) and Design Electrical Engineering Circuits and 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

Beyond vacuity: towards the strongest passing formula

Efficient Detection of Vacuity in Temporal Model Checking

Vacuity in practice: temporal antecedent failure

Model checking parameterized asynchronous shared-memory systems

Deductive Model Checking

Model checking approach to automated planning

Model Checking at IBM

Preface to the special issue on Probabilistic Model Checking

Analyzing probabilistic pushdown automata

Before and after vacuity

Similar Documents

Beyond vacuity: towards the strongest passing formula

Efficient Detection of Vacuity in Temporal Model Checking

Vacuity in practice: temporal antecedent failure

Model checking parameterized asynchronous shared-memory systems

Deductive Model Checking

Model checking approach to automated planning

Model Checking at IBM

Preface to the special issue on Probabilistic Model Checking

Analyzing probabilistic pushdown automata

Before and after vacuity