NDLI: The design and implementation of a certifying compiler

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

Complete removal of redundant expressions

A new algorithm for scalar register promotion based on SSA form

Data transformations for eliminating conflict misses

The implementation and evaluation of fusion and contraction in array languages

Simplification of array access patterns for compiler optimizations

Improving data-flow analysis with path profiles

Partial online cycle elimination in inclusion constraint graphs

Using static single assignment form to improve flow-insensitive pointer analysis

Type-based alias analysis

Exploiting idle floating-point resources for integer execution

Improving performance by branch reordering

Quality and speed in linear-scan register allocation

An implementation of complete, asynchronous, distributed garbage collection

Generational stack collection and profile-driven pretenuring

Proper tail recursion and space efficiency

Using integer sets for data-parallel program analysis and optimization

Communication optimizations for parallel C programs

The implementation of the Cilk-5 multithreaded language

Run-time code generation and modal-ML

Units: cool modules for HOT languages

Eliminating array bound checking through dependent types

Thin locks: featherweight synchronization for Java

Garbage collection and local variable type-precision and liveness in Java virtual machines

Fast, effective code generation in a just-in-time Java compiler

Optimizing direct threaded code by selective inlining

Scalable cross-module optimization

Memory management with explicit regions

A study of dead data members in C++ applications

The design and implementation of a certifying compiler

Automatically closing open reactive programs

The design and implementation of a certifying compiler

Content Provider	ACM Digital Library
Author	Necula, George C. Lee, Peter
Abstract	This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programming language into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the target program. The ensemble of the compiler and the certifier is called a certifying compiler.Several advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code.
Starting Page	333
Ending Page	344
Page Count	12
File Format	PDF
ISBN	0897919874
DOI	10.1145/277650.277752
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1998-05-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

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

The design and implementation of a certifying compiler

RETROSPECTIVE: The Design and Implementation of a Certifying Compiler

The design and implementation of a certifying compiler (SIGP, Vol. 33, Issue. 5)

The design and implementation of a certifying compiler (SIGP, Vol. 39, Issue. 4)

The Design and Implementation of a Certifying Compiler (1998)

The Design and Implementation of a Certifying Compiler (1998)

A certifying compiler for Java

A verifying core for a cryptographic language compiler

A pointer logic and certifying compiler

The design and implementation of a certifying compiler

Similar Documents

The design and implementation of a certifying compiler

RETROSPECTIVE: The Design and Implementation of a Certifying Compiler

The design and implementation of a certifying compiler (SIGP, Vol. 33, Issue. 5)

The design and implementation of a certifying compiler (SIGP, Vol. 39, Issue. 4)

The Design and Implementation of a Certifying Compiler (1998)

The Design and Implementation of a Certifying Compiler (1998)

A certifying compiler for Java

A verifying core for a cryptographic language compiler

A pointer logic and certifying compiler

The design and implementation of a certifying compiler