NDLI: Type-based data structure verification

Please wait, while we are loading the content...

Dynamic software updates: a VM-centric approach

Staged information flow for javascript

Lightweight annotations for controlling sharing in concurrent data structures

Progress guarantee for parallel programs via bounded lock-freedom

A decision procedure for subset constraints over regular languages

GC assertions: using the garbage collector to check heap properties

Sharing classes between families

Verified validation of lazy code motion

Automatic generation of library bindings using static analysis

A study of memory management for web-based applications on multicore processors

Programming model for a heterogeneous x86 platform

Safe and timely updates to multi-threaded programs

Laminar: practical fine-grained decentralized information flow control

A randomized dynamic program analysis technique for detecting real deadlocks

Stretching transactional memory

Verifiable composition of deterministic grammars

SoftBound: highly compatible and complete spatial memory safety for c

Typed self-representation

Proving optimizations correct using parameterized program equivalence

Snugglebug: a powerful approach to weakest preconditions

Efficiently and precisely locating memory leaks and bloat

Binary analysis for measurement and attribution of program performance

CEAL: a C-based language for self-adjusting computation

Merlin: specification inference for explicit information flow problems

FastTrack: efficient and precise dynamic race detection

Parallelizing sequential applications on commodity hardware using a low-cost software transactional memory

Analyzing recursive programs using a fixed-point calculus

Implementation of the memory-safe full ANSI-C compiler

Type-based data structure verification

An integrated proof language for imperative programs

Control-flow refinement and progress invariants for bound analysis

Chameleon: adaptive selection of collections

Semantics-aware trace analysis

PetaBricks: a language and compiler for algorithmic choice

TAJ: effective taint analysis of web applications

LiteRace: effective sampling for lightweight data-race detection

Towards a holistic approach to auto-parallelization: integrating profile-driven parallelism detection and machine-learning based mapping

Program verification using templates over predicate abstraction

Error propagation analysis for file systems

Go with the flow: profiling copies to find runtime bloat

Trace-based just-in-time type specialization for dynamic languages

Type-based data structure verification

Content Provider	ACM Digital Library
Author	Kawaguchi, Ming Rondon, Patrick Jhala, Ranjit
Abstract	We present a refinement type-based approach for the static verification of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). We introduce two novel type-based mechanisms targeted towards these elements: recursive refinements and polymorphic refinements. These mechanisms automate the challenging work of generalizing and instantiating rich universal invariants by piggybacking simple refinement predicates on top of types, and carefully dividing the labor of analysis between the type system and an SMT solver. Further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference to automatically synthesize complex invariants from simple logical qualifiers, thereby almost completely automating the verification. We have implemented our approach in dsolve, which uses liquid types to verify ocaml programs. We present experiments that show that our type-based approach reduces the manual annotation required to verify complex properties like sortedness, balancedness, binary-search-ordering, and acyclicity by more than an order of magnitude.
Starting Page	304
Ending Page	315
Page Count	12
File Format	PDF
ISBN	9781605583921
DOI	10.1145/1542476.1542510
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2009-06-15
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Type inference Dependent types Hindley-milner Predicate abstraction
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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