Efficient SAT-Based Software Analysis: From Automated Testing to Automated Verification and Repair

摘要

Formal approaches to software development have traditionally aimed at guaranteeing software correctness, through the use of notations, analysis mechanisms and other elements founded on solid mathematical grounds. Since the seminal works of Hoare, Floyd and others, formal methods have used logical notations to capture intended software behavior, and proposed techniques for reasoning about software correctness, originally mainly through deductive approaches. Formal methods for software development have been presented as a stronger correctness guarantee compared to informal, widely employed techniques such as testing. While advantages of formal methods make them appealing, the above-described original composition of formal methods implied two main difficulties for their effective use, namely, the need to dominate the logical notations used to specify intended software behavior, and mastering the associated deductive techniques necessary for analysis, i.e., for verifying software correctness.