NDLI: Automatic synthesis of optimal invariant assertions: Mathematical foundations

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

Automatic synthesis of optimal invariant assertions: Mathematical foundations

Abstractions, instantiations, and proofs of marking algorithms

Program synthesis by analogy

The automatic synthesis of recursive programs

Control requirements for the design of production system architectures

Generalized procedure calling and content-directed invocation

The incremental garbage collection of processes

Macaroni is better than spaghetti

Design rationale for TELOS, a PASCAL-based AI language

Automated derivation of program control structure from natural language program descriptions

What the nature of natural language tells us about how to make natural-language-like programming languages more natural

Language facilities for programmable backtracking

CSSA: Language concepts and programming methodology

Prolog - the language and its implementation compared with Lisp

AMORD explicit control of reasoning

A knowledge-based code generator generator

The PSI Program Model Builder - synthesis of very high-level programs

The selection of efficient implementations for a high-level language

Selection of representations for data structures

A normal form for compiler testing

Program manipulation via an efficient production system

Self-redefinition as a program manipulation strategy

Automatic synthesis of optimal invariant assertions: Mathematical foundations

Content Provider	ACM Digital Library
Author	Cousot, Radhia Cousot, Patrick
Abstract	The problem of discovering invariant assertions of programs is explored in light of the fixpoint approach in the static analysis of programs, Cousot [1977a], Cousot[1977b]. In section 2 we establish the lattice theoric foundations upon which the synthesis of invariant assertions is based. We study the resolution of a fixpoint system of equations by Jacobi's successive approximations method. Under continuity hypothesis we show that any chaotic iterative method converges to the optimal solution. In section 3 we study the deductive semantics of programs. We show that a system of logical forward equations can be associated with a program using the predicate transformer rules which define the semantics of elementary instructions. The resolution of this system of semantic equations by chaotic iterations leads to the optimal invariants which exactly define the semantics of this program. Therefore these optimal invariants can be used for total correctness proofs (section 4). Next we show that usually a system of inequations is used as a substitute for the system of equations. Hence the solutions to this system of inequations are approximate invariants which can only be used for proofs of partial correctness (section 5). In section 6 we show that symbolic execution of programs consists in fact in solving the semantic equations associated with this program. The construction of the symbolic execution tree corresponds to the chaotic successive approximations method. Therefore symbolic execution permits optimal invariant assertions to be discovered provided that one can pass to the limit, that is consider infinite paths in the symbolic execution tree. Induction nrinciDles can be used for that purpose. In section 7 we show how difference equations can be utilized to discover the general term of the sequence of successive approximations so that optimal invariants are obtained by a mere passage to the limit. In section 8 we show that an approximation of the optimal solution to a fixpoint system of equations can be obtained by strengthening the term of a chaotic iteration sequence. This formalizes the synthesis of approximate invariants by heuristic methods. Various examples provide a helpful intuitive support to the technical sections.
Starting Page	1
Ending Page	12
Page Count	12
File Format	PDF
DOI	10.1145/800228.806926
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1977-08-15
Publisher Place	New York
Access Restriction	Subscribed
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