NDLI: Natural proofs for data structure manipulation in C using separation logic

Content Provider	ACM Digital Library
Author	Madhusudan, P. Qiu, Xiaokang Pek, Edgar
Abstract	The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32]. In this work, we develop a framework called VCDryad that extends the Vcc framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing Vcc framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing Vcc to find natural proofs using primarily decidable theories. We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, well-known open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without any user-provided proof tactics. VCDryad is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
Starting Page	440
Ending Page	451
Page Count	12
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2666356.2594325
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	49
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	Program verifiers Separation logic Data structures Natural proofs
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

Natural proofs for data structure manipulation in C using separation logic

Natural proofs for structure, data, and separation

Automatic induction proofs of data-structures in imperative programs

Cyclic proofs of program termination in separation logic

Semantics-based program verifiers for all languages

Relaxed separation logic:a program logic for C11 concurrency

GPS:navigating weak memory with ghosts, protocols, and separation

Automatic safety proofs for asynchronous memory operations

Verifying read-copy-update in a logic for weak memory

Natural proofs for data structure manipulation in C using separation logic

Similar Documents

Natural proofs for data structure manipulation in C using separation logic

Natural proofs for structure, data, and separation

Automatic induction proofs of data-structures in imperative programs

Cyclic proofs of program termination in separation logic

Semantics-based program verifiers for all languages

Relaxed separation logic:a program logic for C11 concurrency

GPS:navigating weak memory with ghosts, protocols, and separation

Automatic safety proofs for asynchronous memory operations

Verifying read-copy-update in a logic for weak memory

Natural proofs for data structure manipulation in C using separation logic