| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 3, 2012 |
| Latest Amendment Date: | July 3, 2012 |
| Award Number: | 1218605 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Nina Amla
namla@nsf.gov (703)292-7991 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | August 15, 2012 |
| End Date: | July 31, 2015 (Estimated) |
| Total Intended Award Amount: | $400,000.00 |
| Total Awarded Amount to Date: | $400,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
506 S WRIGHT ST URBANA IL US 61801-3620 (217)333-2187 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
IL US 61820-7473 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Computers, and implicitly programming languages, are used in many
critical applications these days, where correct behavior is necessary.
Rigorous, formal semantic definitions of the employed programming
languages are therefore necessary in order to verify computing systems.
Unfortunately, in spite of more than forty years of research in
programming language semantics, most program verifiers are not directly
based on a formal semantics, but rather on complex and ad-hoc hardwired
models of their target programming languages. This has at least two
negative consequences: first, it makes the development and maintenance
of program verifiers hard and uneconomical, particularly for new
programming languages or languages which evolve fast; second, it allows
room for subtle bugs in program verifiers themselves. This research
project aims at developing a generic program verification framework
that takes a programming language given through its formal semantics as
input, and yields a program verifier for that language as output.
Moreover, the language semantics will be executable, so testable,
and public, so will serve as a reference implementation for the language
and as a formal basis for language understanding.
Specifically, this projects builds upon recent advances in matching logic
and its use for verifying reachability properties. A language-independent
sound and relatively complete proof system takes a programming language
operational semantics as a set of axioms, and can be used to derive
any reachability property about any program in the given language. This
is in sharp contrast to the existing verification approaches based on
Hoare logic and on dynamic logic, since these approaches are
language-specific. This research will therefore lead to the development
of semantic and verification techniques and algorithms that will work for
any language, provided a formal semantics of the language is given.
Consequently, the broader impact of this research is that it will increase
the quality and robustness of software systems, and will narrow the gap
between the specification and the implementation of computer systems.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
The main outcome of this project is a program verification infrastructure, which provides a fast way to build a correct-by-construction program verifier from a formal K (kframework.org) semantics of a progamming language. This gives researchers in the program verification areas an easy way of deploying new verification techniques for real-world languages. It also gives language designers a cost-effective way to build verifiers for their languages, regardless of how unconventional they are.
The K formal semantics of three major languages were defined and used with the verification infrastructure: JavaScript (ES5), C (ISO C11), and Java (1.4). These are largest known formal semantics of real-world programming languages known. Besides providing referfence models for these language that can be used by other researchers to validate their program analysis tools, these semantics have also been used to detect errors in all the major web browsers (Chrome, Safari, Firefox, IE), errors that can yield safety and security leaks.
The K framework makes it easy for researchers to design and develop not only new programming langugaes, but also effective formal analysis tools for them that can find errors in realistic applications. Researchers in other disciplines should now be more likely to design their own domain-specific languages, which should increase their productivity and confidence in their work.
The K framework has been adopted as infrastructure for the commercial RV-Match tool (https://runtimeverification.com/match/) in PI's startup Runtime Verification, Inc. (https://runtimeverification.com). Currently, three large customers use the RV-Match tool: NASA, Boeing, Toyota ITC & Denso. Negotiations with other customers will hopefully spread more widely the use of this tool, and thus the results of this NSF project.
The results of the project in the areas of building programs verifiers and operational semantics should make the use of certified software systems more widespread, which in turn should decrease the likelihood of major bugs, like Heartbleed.
Last Modified: 04/12/2016
Modified by: Grigore Rosu
Please report errors in award information by writing to: awardsearch@nsf.gov.
