NDLI: Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Content Provider	ACM Digital Library
Author	Dillig, Thomas Dillig, Isil Aiken, Alex
Abstract	Many relational static analysis techniques for precise reasoning about heap contents perform an explicit case analysis of all possible heaps that can arise. We argue that such precise relational reasoning can be obtained in a more scalable and economical way by enforcing the memory invariant that every concrete memory location stores one unique value directly on the heap abstraction. Our technique combines the strengths of analyses for precise reasoning about heap contents with approaches that prioritize axiomatization of memory invariants, such as the theory of arrays. Furthermore, by avoiding an explicit case analysis, our technique is scalable and powerful enough to analyze real-world programs with intricate use of arrays and pointers; in particular, we verify the absence of buffer overruns, incorrect casts, and null pointer dereferences in OpenSSH (over 26,000 lines of code) after fixing 4 previously undiscovered bugs found by our system. Our experiments also show that the combination of reasoning about heap contents and enforcing existence and uniqueness invariants is crucial for this level of precision.
Starting Page	397
Ending Page	410
Page Count	14
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1932682.1869493
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	45
Issue Number	10
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	Array analysis Heap analysis Relational static analysis Memory invariants
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

Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Symbolic heap abstraction with demand-driven axiomatization of memory invariants (2010)

Scaling abstraction refinement via pruning

A demand-driven adaptive type analysis

Relational inductive shape analysis

Precise reasoning for programs using containers

Thresher:precise refutations for heap reachability

Selective control-flow abstraction via jumping

Symbolic bounds analysis of pointers, array indices, and accessed memory regions

Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Similar Documents

Symbolic heap abstraction with demand-driven axiomatization of memory invariants

Symbolic heap abstraction with demand-driven axiomatization of memory invariants (2010)

Scaling abstraction refinement via pruning

A demand-driven adaptive type analysis

Relational inductive shape analysis

Precise reasoning for programs using containers

Thresher:precise refutations for heap reachability

Selective control-flow abstraction via jumping

Symbolic bounds analysis of pointers, array indices, and accessed memory regions

Symbolic heap abstraction with demand-driven axiomatization of memory invariants