Official websites use .gov
A .gov website belongs to an official government organization in the United States.
Secure .gov websites use HTTPS
A lock (
) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.
Runtime verification (RV) is a relatively new software analysis approach, introduced by Klaus Havelund (NASA JPL) and Grigore Rosu in 2001 when they were colleagues at NASA Ames. It combines formal methods with dynamic analysis, the main idea being to formally analyze programs as they execute, observing the results of the execution and using those results to find bugs or violations of specifications. In this talk we will present Runtime Verification technology and products that automatically detect more undefined behaviors in C/C++ applications (e.g., buffer overflows and underflows, stack overflows, data-races, etc.) than the existing commercial static analysis tools, with no false positives. One advantage of RV is that it is based on a formal semantics of the ISO C11 standard, available at https://github.com/kframework/c-semantics
Runtime Verification, Inc. is a University of Illinois startup company aimed at incorporating these ideas into well-engineered and easy to use products. The development of the presented technology and products has been generously supported by a NASA SBIR grant (phases I, II, II-E and currently III) and several Boeing and Toyota contracts.
Grigore Rosu/UIUC and Chris Hathhorn/RV Inc.
Outside attendees need to contact Janet Madison in order to obtain the site badges required to enter NIST grounds and to attend the seminar. 24 hour notice is required for US citizens and 3 days for non-US citizens. Please contact janet.madison@nist.gov to be added to the visitor list. Visitors must check in at the NIST Visitor Center to pick up their badges. A photo ID is required for US citizens and a passport or green card for foreign nationals.