The increasingly widespread use of multicore processors, whose computing power can only be unleashed by concurrent software, makes software defects, or bugs, become more common and labor-intensive to detect and repair. Runtime verification is a novel analysis approach that extracts information from a running system and uses it to detect and possibly react to observed behaviors satisfying or violating certain properties. Runtime verification scales well and avoids the complexity of traditional formal verification techniques. The techniques developed in this project will lead to robust production quality software by providing a scalable alternative to formal verification that provides many of the same guarantees for safety and security.

This project aims to develop a scalable predictive runtime verification framework for concurrent software. A major technical advancement over prior art is that it not only detects errors when they occur at runtime, but is able to predict general security and safety property violations before they actually surface, preventing bad behaviors from happening by taking proper actions defined by the users. This project builds upon a sound and maximal causal model, hereby providing the provably maximum possible prediction power on the observed trace with no false alarms. The core research insight of this work is to explore the maximal causality of concurrency with automated constraint solving, which has been studied for decades and is becoming increasingly powerful.

Project Start
Project End
Budget Start
2014-08-01
Budget End
2018-07-31
Support Year
Fiscal Year
2014
Total Cost
$500,000
Indirect Cost
Name
University of Illinois Urbana-Champaign
Department
Type
DUNS #
City
Champaign
State
IL
Country
United States
Zip Code
61820