Sequential circuits for program analysis

ABSTRACT

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

REFERENCES

• 1: Peter J. Ashenden, The Designer's Guide to VHDL, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1999
• 2: A. Aziz, F. Balarin, R. Brayton, and A. Sangiovanni-Vincentelli. Sequential Synthesis Using S1S. IEEE Trans. Comput.-Aided Design Integrated Circuits, Oct. 2000.
• 3: Adnan Aziz , Thomas Shiple , Vigyan Singhal , Robert Brayton , Alberto Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking, Formal Methods in System Design, v.21 n.2, p.193-224, September 2002 [doi>10.1023/A:1016043502772]
• 4: Adam Barr, Find the Bug: A Book of Incorrect Programs, Addison-Wesley Professional, 2004
• 5: Jason Baumgartner , Andreas Kuehlmann , Jacob A. Abraham, Property Checking via Structural Analysis, Proceedings of the 14th International Conference on Computer Aided Verification, p.151-165, July 27-31, 2002
• 6: R. J. Bayardo Jr. and R. C. Schrag. Using CSP look-back techniques to solve real world SAT instances. In National Conference on Artificial Intelligence, 1997.
• 7: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 8: R. K. Brayton and C. McMullen. The Decomposition and Factorization of Boolean Expressions. May 1982.
• 9: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, March 2004.
• 10: Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775928]
• 11: Giovanni De Micheli, Hardware synthesis from C/C++ models, Proceedings of the conference on Design, automation and test in Europe, p.80-es, January 1999, Munich, Germany [doi>10.1145/307418.307527]
• 12: Stephen A. Edwards, The Challenges of Hardware Synthesis from C-Like Languages, Proceedings of the conference on Design, Automation and Test in Europe, p.66-67, March 07-11, 2005 [doi>10.1109/DATE.2005.307]
• 13: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 14: Sumit Gupta , Rajesh Kumar Gupta , Nikil D. Dutt , Alexandru Nicolau, Coordinated parallelizing compiler optimizations and high-level synthesis, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.9 n.4, p.441-470, October 2004 [doi>10.1145/1027084.1027087]
• 15: Steven Paul Haynal , Forrest D. Brewer, Automata-based symbolic scheduling, 2000
• 16: Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 17: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 18: John E. Hopcroft , Rajeev Motwani , Rotwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages and Computability, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 19: International Organization for Standardization. ISO/IEC 9899:1999: Programming languages-C. 1999.
• 20: Andreas Kuehlmann , Jason Baumgartner, Transformation-Based Verification Using Generalized Retiming, Proceedings of the 13th International Conference on Computer Aided Verification, p.104-117, July 18-22, 2001
• 21: A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design, (12), 2002.
• 22: R. P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, 1993.
• 23: H. Mony et al. Scalable automated verification via expert-system guided transformations. In Formal Methods in Computer-Aided Design, Nov. 04.
• 24: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 25: In-Ho Moon , Gary D. Hachtel , Fabio Somenzi, Border-Block Triangular Form and Conjunction Schedule in Image Computation, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.73-90, November 01-03, 2000
• 26: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 27: Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation, Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, p.459, September 17-20, 2000
• 28: A. Saldanha , A. R. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, Multi-level logic simplification using don't cares and filters, Proceedings of the 26th ACM/IEEE conference on Design automation, p.277-282, June 25-28, 1989, Las Vegas, Nevada, United States [doi>10.1145/74382.74429]
• 29: E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis. Technical report, Electronics Research Lab, Univ. of California, Berkeley, May 1992.
• 30: Thomas R. Shiple , James H. Kukula , Rajeev K. Ranjan, A Comparison of Presburger Engines for EFSM Reachability, Proceedings of the 10th International Conference on Computer Aided Verification, p.280-292, June 28-July 02, 1998
• 31: E. Torlak and D. Jackson. Kodkod: A relational model finder. In Tools and Algorithms for Construction and Analysis of Systems, March 2007.
• 32: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 33: Fadi Zaraket , Adnan Aziz , Sarfraz Khurshid, Sequential Circuits for Relational Analysis, Proceedings of the 29th international conference on Software Engineering, p.13-22, May 20-26, 2007 [doi>10.1109/ICSE.2007.75]
• 34: F. Zaraket , J. Baumgartner , A. Aziz, Scalable compositional minimization via static analysis, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1060-1067, November 06-10, 2005, San Jose, CA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Mechanical verification; Assertions

General Terms:
Verification

Keywords:
model checking, program analysis, static analysis, verification