Skip Navigation Links

Project Information

CAREER: SEMANTICS, ABSTRACTIONS, AND TOOLS FOR A PRAGMATIC VERIFIED LLVM COMPILER

Agency:
NSF

National Science Foundation

Project Number:
1453086
Contact PI / Project Leader:
NAGARAKATTE, SANTOSH
Awardee Organization:
RUTGERS THE ST UNIV OF NJ NEW BRUNSWICK

Description

Abstract Text:
Title: : CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM Compiler

Compilers are crucial components of the computing ecosystem. They can transform source programs written in multiple languages (e.g, C/C++/Java) into multiple target architectures (e.g, x86/ARM). Compiler bugs, however, break properties enforced at the level of source programs and can lead to unintended application behavior and disasters in safety-critical domains. This project aims to develop pragmatic and lightweight formal techniques for making mainstream compilers robust, in a manner that can be easily adopted by compiler developers. The intellectual merit of this project is the development of real-world compiler verification environments drawing influence from multiple areas like programming languages, architecture, and concurrency. The project's broader significance and importance are: (1) improving the quality of a large number of software projects by improving the robustness of the compiler, (2) inculcating formal reasoning for building large systems (compilers in particular) that are correct by construction, and (3) educating high school students, undergraduates, and graduate students for developing software with lightweight formal methods.

This project aims to build new techniques and tools that can check the correctness of optimizations with the help of the developer. The project achieves this by (1) designing mathematically-precise semantics for various components of the mainstream LLVM compiler, (2) designing domain specific languages for writing and specifying LLVM optimizations, which not only check optimizations for correctness but also generate efficient C++ implementations, (3) designing techniques to build precise translation validators, which compare the source and the target code with assistance from the compiler developer. Technology developed by this research will not only improve the reliability of compilers but also the reliability of other large software systems which depend on correct compilation.
Project Terms:
Adopted; Architecture; Area; Behavior; career; Code; Computer software; design; Development; Disasters; Ecosystem; Environment; graduate student; High School Student; improved; Java; Language; Lead; Methods; Programming Languages; programs; Property; Research; Safety; Semantics; software development; software systems; Source; Specific qualifier value; System; Techniques; Technology; tool; Translations; Writing

Details

Contact PI / Project Leader Information:
Name:  NAGARAKATTE, SANTOSH
Other PI Information:
Not Applicable
Awardee Organization:
Name:  RUTGERS THE ST UNIV OF NJ NEW BRUNSWICK
City:  NEW BRUNSWICK    
Country:  UNITED STATES
Congressional District:
State Code:  NJ
District:  06
Other Information:
Fiscal Year: 2015
Award Notice Date: 15-Jan-2015
DUNS Number: 001912864
Project Start Date: 15-Jan-2015
Budget Start Date:
CFDA Code: 47.070
Project End Date: 31-Dec-2019
Budget End Date:
Agency: ?

Agency: The entity responsible for the administering of a research grant, project, or contract. This may represent a federal department, agency, or sub-agency (institute or center). Details on agencies in Federal RePORTER can be found in the FAQ page.

National Science Foundation
Project Funding Information for 2015:
Year Agency

Agency: The entity responsible for the administering of a research grant, project, or contract. This may represent a federal department, agency, or sub-agency (institute or center). Details on agencies in Federal RePORTER can be found in the FAQ page.

FY Total Cost
2015 NSF

National Science Foundation

$209,045

Results

i

It is important to recognize, and consider in any interpretation of Federal RePORTER data, that the publication and patent information cannot be associated with any particular year of a research project. The lag between research being conducted and the availability of its results in a publication or patent award varies substantially. For that reason, it's difficult, if not impossible, to associate a publication or patent with any specific year of the project. Likewise, it is not possible to associate a publication or patent with any particular supplement to a research project or a particular subproject of a multi-project grant.

ABOUT FEDERAL REPORTER RESULTS

Publications: i

Click on the column header to sort the results

PubMed = PubMed PubMed Central = PubMed Central Google Scholar = Google Scholar

Patents: i

Click on the column header to sort the results

Similar Projects

Download Adobe Acrobat Reader:Adobe Acrobat VERSION: 3.41.0 Release Notes
Back to Top