NDLI: Explaining abstract counterexamples

Content Provider	ACM Digital Library
Author	Strichman, Ofer Groce, Alex Chaki, Sagar
Abstract	When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for explaining and localizing errors based on finding the closest execution to a counterexample, with respect to a distance metric. That approach was applied only to concrete executions of programs. This paper extends and generalizes the approach by combining it with predicate abstraction. Using an abstract state-space increases scalability and makes explanations more informative. Differences between executions are presented in terms of predicates derived from the specification and program, rather than specific changes to variable values. Reasoning to the cause of an error from the factthat in the failing run x < y, but in the successful execution x = y is easier than reasoning from the information that in the failing run y = 239, but in the successful execution y = 232. An abstract explanation is automatically generalized Predicate abstraction has previously been used in model checking purely as a state-space reduction technique. However, an abstraction good enough to enable a model checking tool to find an error is also likely to be useful as an automatically generated high-level description of a state space --- suitable for use by programmers. Results demonstrating the effectiveness of abstract explanations support this claim.
Starting Page	73
Ending Page	82
Page Count	10
File Format	PDF
ISSN	01635948
DOI	10.1145/1041685.1029908
Journal	ACM SIGSOFT Software Engineering Notes (SOEN)
Volume Number	29
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1979-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Fault localization Model checking Predicate abstraction
Content Type	Text
Resource Type	Article

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

Explaining abstract counterexamples

Polymorphic predicate abstraction

Combining predicate and numeric abstraction for software model checking

Competent predicate abstraction in model checking

Transition predicate abstraction and fair termination

Predicate abstraction and CEGAR for higher-order model checking

ABSTRACT Explaining Abstract Counterexamples

Transition predicate abstraction and fair termination

Joining dataflow with predicates

Explaining abstract counterexamples

Similar Documents

Explaining abstract counterexamples

Polymorphic predicate abstraction

Combining predicate and numeric abstraction for software model checking

Competent predicate abstraction in model checking

Transition predicate abstraction and fair termination

Predicate abstraction and CEGAR for higher-order model checking

ABSTRACT Explaining Abstract Counterexamples

Transition predicate abstraction and fair termination

Joining dataflow with predicates

Explaining abstract counterexamples