Sequential circuits for program analysis

A number of researchers have proposed the use of Boolean satisfiability solvers for verifying C programs. They encode correctness checks as Boolean formulas using finitization: loops and recursion are bounded, as is the size of the input instances. The SAT approach has been shown to find subtle bugs with reasonable resources. However, it does not scale well; in particular, it lacks the ability to handle larger bounds. We present SEBAC, which can handle the same class of programs as the SAT approach, and scales to bounds that are orders of magnitude higher. The key difference between SEBAC and SAT techniques is SEBAC’s use of imperative Boolean sequential circuits, which are Boolean formulas with memory elements instead of the Boolean formulas which are stateless. Categories and Subject Descriptors D.2.4 [Software Engineering]: Program Verification—formal methods, model checking; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—a...

• Type: Conference
• Year: 2007
• Where: KBSE
• Authors: Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid
• Keywords: Boolean Formulas, Boolean Satisfiability Solvers, KBSE 2007, SAT Approach, Software Engineering