NDLI: Permissive interfaces

Content Provider	ACM Digital Library
Author	Majumdar, Rupak Henzinger, Thomas A. Jhala, Ranjit
Abstract	A modular program analysis considers components independently and provides a succinct summary for each component, which is used when checking the rest of the system. Consider a system consisting of a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.
Starting Page	31
Ending Page	40
Page Count	10
File Format	PDF
ISSN	01635948
DOI	10.1145/1095430.1081713
Journal	ACM SIGSOFT Software Engineering Notes (SOEN)
Volume Number	30
Issue Number	5
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	Modular verification Software interfaces
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

Permissive interfaces

An automata-theoretic approach to modular model checking

Model checking and modular verification

Foundations of incremental aspect model-checking

Verifying aspect advice modularly

Modular verification of software components in C

Modular Verification of Open Features Using Three-Valued Model Checking

Modular verification of preemptive OS kernels

Modular verification of collaboration-based software designs

Permissive interfaces

Similar Documents

Permissive interfaces

An automata-theoretic approach to modular model checking

Model checking and modular verification

Foundations of incremental aspect model-checking

Verifying aspect advice modularly

Modular verification of software components in C

Modular Verification of Open Features Using Three-Valued Model Checking

Modular verification of preemptive OS kernels

Modular verification of collaboration-based software designs

Permissive interfaces