Automating Program Verification and Repair Using Invariant Analysis and Test Input Generation

Software bugs are a persistent feature of daily life---crashing web browsers, allowing cyberattacks, and distorting the results of scientific computations. One approach to improving software uses program invariants---mathematical descriptions of program behaviors---to verify code and detect bugs. Current invariant generation techniques lack support for complex yet important forms of invariants, such as general polynomial relations and properties of arrays. As a result, we lack the ability to conduct precise analysis of programs that use this common data structure. This dissertation presents DIG, a static and dynamic analysis framework for discovering several useful classes of program invariants, including (i) nonlinear polynomial relations, which are fundamental to many scientific applications; disjunctive invariants, (ii) which express branching behaviors in programs; and (iii) properties about multidimensional arrays, which appear in many practical applications. We describe theoretical and empirical results showing that DIG can efficiently and accurately find many important invariants in real-world uses, e.g., polynomial properties in numerical algorithms and array relations in a full AES encryption implementation. Automatic program verification and synthesis are long-standing problems in computer science. However, there has been a lot of work on program verification and less so on program synthesis. Consequently, important synthesis tasks, e.g., generating program repairs, remain difficult and time-consuming. This dissertation proves that certain formulations of verification and synthesis are equivalent, allowing for direct applications of techniques and tools between these two research areas. Based on these ideas, we develop CETI, a tool that leverages existing verification techniques and tools for automatic program repair. Experimental results show that CETI can have higher success rates than many other standard program repair methods.

Name thesis:degree_name

Computer Science

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Department of Computer Science

Year

2010

Author dc:creator

• Nguyen, Thanh V

Contributors dc:contributor

• Forrest, Stephanie
• Kapur, Deepak
• Stefanovic, Darko
• Weimer, Westley

• dynamic analysis
• invariant generation
• program repair
• program synthesis
• program verification
• theorem proving

Language dc:language

English

Identifier

https://digitalrepository.unm.edu/cs_etds/44

OAI identifier oai:identifier

oai:digitalrepository.unm.edu:cs_etds-1043