NDLI: Fissile type analysis:modular checking of almost everywhere invariants

Content Provider	ACM Digital Library
Author	Coughlin, Devin Chang, Bor-Yuh Evan
Abstract	We present a generic analysis approach to the imperative relationship update problem, in which destructive updates temporarily violate a global invariant of interest. Such invariants can be conveniently and concisely specified with dependent refinement types, which are efficient to check flow-insensitively. Unfortunately, while traditional flow-insensitive type checking is fast, it is inapplicable when the desired invariants can be temporarily broken. To overcome this limitation, past works have directly ratcheted up the complexity of the type analysis and associated type invariants, leading to inefficient analysis and verbose specifications. In contrast, we propose a generic lifting of modular refinement type analyses with a symbolic analysis to efficiently and effectively check concise invariants that hold almost everywhere. The result is an efficient, highly modular flow-insensitive type analysis to optimistically check the preservation of global relationship invariants that can fall back to a precise, disjunctive symbolic analysis when the optimistic assumption is violated. This technique permits programmers to temporarily break and then re-establish relationship invariants--a flexibility that is crucial for checking relationships in real-world, imperative languages. A significant challenge is selectively violating the global type consistency invariant over heap locations, which we achieve via almost type-consistent heaps. To evaluate our approach, we have encoded the problem of verifying the safety of reflective method calls in dynamic languages as a refinement type checking problem. Our analysis is capable of validating reflective call safety at interactive speeds on commonly-used Objective-C libraries and applications.
Starting Page	73
Ending Page	85
Page Count	13
File Format	PDF MP4
ISSN	03621340 15581160
DOI	10.1145/2578855.2535855
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	49
Issue Number	1
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	Dependent refinement types Almost everywhere invariants Almost type-consistent heaps Objective-c Reflection
Content Type	Audio 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

Fissile type analysis: modular checking of almost everywhere invariants

A type-directed abstraction refinement approach to higher-order model checking

Secure distributed programming with value-dependent types

Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants

Self-certification:bootstrapping certified typecheckers in F* with Coq

Static and user-extensible proof checking

Refinement types for TypeScript

Low-level liquid types

Linear dependent types for differential privacy

Fissile type analysis:modular checking of almost everywhere invariants

Similar Documents

Fissile type analysis: modular checking of almost everywhere invariants

A type-directed abstraction refinement approach to higher-order model checking

Secure distributed programming with value-dependent types

Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants

Self-certification:bootstrapping certified typecheckers in F* with Coq

Static and user-extensible proof checking

Refinement types for TypeScript

Low-level liquid types

Linear dependent types for differential privacy

Fissile type analysis:modular checking of almost everywhere invariants