NDLI: On inter-procedural analysis of programs with lists and data

Content Provider	ACM Digital Library
Author	Enea, Constantin Bouajjani, Ahmed Drăgoi, Cezara Sighireanu, Mihaela
Abstract	We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program configurations are represented by graphs where nodes represent list segments without sharing. The data in these list segments are characterized by constraints in abstract domains. We consider a domain where constraints are in a universally quantified fragment of the first-order logic over sequences, as well as a domain constraining the multisets of data in sequences. Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain. The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking.
Starting Page	578
Ending Page	589
Page Count	12
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1993316.1993566
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	46
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Assertion synthesis Dynamic data structures Interprocedural analysis
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design 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

On inter-procedural analysis of programs with lists and data

Interprocedural analysis of asynchronous programs

Dataflow analysis for concurrent programs using datarace detection

Data representation synthesis

Escape analysis on lists

Pointer analysis for programs with structures and casting

Parallelizing top-down interprocedural analyses

Interprocedural modification side effect analysis with pointer aliasing

Dynamic optimistic interprocedural analysis:a framework and an application

On inter-procedural analysis of programs with lists and data

Similar Documents

On inter-procedural analysis of programs with lists and data

Interprocedural analysis of asynchronous programs

Dataflow analysis for concurrent programs using datarace detection

Data representation synthesis

Escape analysis on lists

Pointer analysis for programs with structures and casting

Parallelizing top-down interprocedural analyses

Interprocedural modification side effect analysis with pointer aliasing

Dynamic optimistic interprocedural analysis:a framework and an application

On inter-procedural analysis of programs with lists and data