NDLI: Using Abstraction to Verify Arbitrary Temporal Properties

Content Provider	IEEE Xplore Digital Library
Author	Pnueli, A.
Copyright Year	2008
Description	Author affiliation: New York Univ., New York, NY, USA (Pnueli, A.)
Abstract	Summary form only given. It is a known fact that finitary state abstraction methods (i.e. methods in which the abstract domain is finite), such as predicate abstraction, are inadequate for verifying general liveness properties or even termination of sequential programs. In this talk we will present an abstraction approach called ranking abstraction which is sound and complete for verifying all temporally specified properties, including all liveness properties. We will start by presenting a general simple framework for state abstraction emphasizing that, in order to get soundness, it is necessary to apply an over-approximating abstraction to the system and an under-approximating abstraction to the (temporal) property. We show that finitary version of this abstraction are complete for verifying all safety properties. We also show examples of simple programs whose termination provably cannot be established by finitary abstraction. We then consider abstraction approaches to the verification of deadlock freedom, presenting some sufficient conditions guaranteeing that deadlock freedom is inherited from the concrete to the abstract. Finally, we introduce the method of ranking abstraction and illustrate its application to the verification of termination and more general liveness properties. In this presentation we emphasize the similarity between predicate abstraction and its extension into ranking abstraction. In particular, the fact that the user does not have to provide a full ranking function but only to specify the ingredients from which such a function can be constructed. We also sketch how abstraction refinement can be applied to ranking abstraction, thus opening the way to a CEGAR-like methodology. Time permitting, we will present a brief comparison between ranking abstraction and the methods of transition abstraction developed by Podelski, Rybalchenko, and Cook which underly the Terminator system. The talk is based on results obtained through joint research with I. Balaban, Y. Kesten, and L.D. Zuck.
Starting Page	3
Ending Page	3
File Size	141802
Page Count	1
File Format	PDF
ISBN	9780769534466
ISSN	15301362
DOI	10.1109/APSEC.2008.76
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-12-03
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	System recovery Software engineering Electronic mail Safety Sufficient conditions Concrete
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

Making Abstraction Concrete

Automatic Construction of Complete Abstraction by Abstract Interpretation

Proving Temporal Properties of Z Specifications Using Abstraction (2003)

Analysis of structural properties in extended marked graphs

A deadlock detection/resolution algorithm for the OR model

3-Valued Abstraction: More Precision at Less Cost

A temporal logic approach to discrete event control

Testing prototypes validity to enhance code reuse

Necessary and sufficient conditions for resultant siphons to be controlled

Using Abstraction to Verify Arbitrary Temporal Properties

Similar Documents

Making Abstraction Concrete

Automatic Construction of Complete Abstraction by Abstract Interpretation

Proving Temporal Properties of Z Specifications Using Abstraction (2003)

Analysis of structural properties in extended marked graphs

A deadlock detection/resolution algorithm for the OR model

3-Valued Abstraction: More Precision at Less Cost

A temporal logic approach to discrete event control

Testing prototypes validity to enhance code reuse

Necessary and sufficient conditions for resultant siphons to be controlled

Using Abstraction to Verify Arbitrary Temporal Properties