SHF:Small:Analysis, Repair, and Synthesis for k-Safety

University Of Texas At Austin, Austin TX

Investigators

Abstract

This project aims to eradicate a broad class of software bugs, called k-safety errors, that arise from multiple inconsistent executions of the same procedure. While there is relatively little work on automated detection of such errors, the investigators have found dozens of such errors in widely-used software projects. This project develops semantic reasoning techniques that help software engineers implement correct programs that do not exhibit k-safety errors. In addition to improving the security and reliability of many kinds of software, these techniques make it easier for software engineers to develop, maintain, and debug their projects. The tools and techniques generated in this project will open-source and incorporated into the educational curriculum whenever possible. The project includes graduate and undergraduate students in this research. The project develops a comprehensive theoretical framework for reasoning about arbitrary k-safety properties, including associativity, determinism, transitivity, and others. Based on preliminary work on Cartesian Hoare Logic (CHL), the investigators explore a wide range of semantic reasoning tools for k-safety, ranging from static and dynamic analysis to automated repair and synthesis. On the analysis side, the project explores precise and scalable static analysis techniques that can automatically prove the absence of k-safety violations using automatically inferred relational program invariants. The project also investigates combined static and dynamic program analysis techniques that can provide witnesses to k-safety violations.