NDLI: A generic annotation inference algorithm for the safety certification of automatically generated code

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

Staging static analyses for program generation

Creating custom containers with generative techniques

When to use features and aspects?: a case study

Transparent program transformations in the presence of opaque code

Expressing heap-shape contracts in linear logic

A graphical programming system for molecular motif search

Software extension and integration with type classes

Feature refactoring a multi-representation program into a product line

Roadmap for enhanced languages and methods to aid verification

Semantic reasoning about feature composition via multiple aspect-weavings

Debugging C++ template metaprograms

A multi-stage language with intensional analysis

Safe component updates

A dynamic aspect-oriented system for OS kernels

Towards an effective integrated reuse environment

A verified staged interpreter is a verified compiler

Gaigen 2:: a geometric algebra implementation generator

Flexible and efficient measurement of dynamic bytecode metrics

Refactoring product lines

Distributed meta-programming

Stayin' alert:: moulding failure and exceptions to your needs

Assimilating MetaBorg:: embedding language tools in languages

Application-specific foreign-interface generation

Concurrent aspects

A generic annotation inference algorithm for the safety certification of automatically generated code

Determining over- and under-constrained systems of equations using structural constraint delta

Patches as better bug reports

Verifying feature-based model templates against well-formedness OCL constraints

TCS:: a DSL for the specification of textual concrete syntaxes in model engineering

Reflective program generation with patterns

YABS:: a domain-specific language for pervasive computing based on stigmergy

A generic annotation inference algorithm for the safety certification of automatically generated code

Content Provider	ACM Digital Library
Author	Fischer, Bernd Denney, Ewen
Abstract	Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e., pre- and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains difficult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator).Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property-specific abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding definitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.
Starting Page	121
Ending Page	130
Page Count	10
File Format	PDF
ISBN	1595932372
DOI	10.1145/1173706.1173725
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-10-22
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Logical annotations Automated code generation Hoare calculus Automated theorem proving Program verification Software certification
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