Subscribe

Issue No.04 - July-Aug. (2012 vol.38)

pp: 957-974

Lucas Cordeiro , Federal University of Amazonas, Brazil

Bernd Fischer , University of Southampton, Southampton

Joao Marques-Silva , University College Dublin, Dublin

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2011.59

ABSTRACT

Propositional bounded model checking has been applied successfully to verify embedded software, but remains limited by increasing propositional formula sizes and the loss of high-level information during the translation preventing potential optimizations to reduce the state space to be explored. These limitations can be overcome by encoding high-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we propose the application of different background theories and SMT solvers to the verification of embedded software written in ANSI-C in order to improve scalability and precision in a completely automatic way. We have modified and extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions, and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded software applications from telecommunications, control systems, and medical devices. The experiments show that our ESBMC model checker can analyze larger problems than existing tools and substantially reduce the verification time.

INDEX TERMS

Software engineering, formal methods, verification, model checking

CITATION

Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva, "SMT-Based Bounded Model Checking for Embedded ANSI-C Software",

*IEEE Transactions on Software Engineering*, vol.38, no. 4, pp. 957-974, July-Aug. 2012, doi:10.1109/TSE.2011.59REFERENCES

- [1] A. Biere, "Bounded Model Checking,"
Handbook of Satisfiability, pp. 457-481, IOS Press, 2009.- [2] A. Armando, J. Mantovani, and L. Platania, "Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers,"
Proc. SPIN, pp. 146-162, 2006.- [3] A. Armando, J. Mantovani, and L. Platania, "Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers,"
Int'l J. Software Tools Technology Transfer, vol. 11, no. 1, pp. 69-83, 2009.- [4] M.K. Ganai and A. Gupta, "Accelerating High-Level Bounded Model Checking,"
Proc. Int'l Conf. Computer-Aided Design, pp. 794-801, 2006.- [5]
ISO/IEC 9899:1999: Programming Languages C. Int'l Organization for Standardization, 1999.- [6] D. Kroening,
CBMC 3.3 Released—Preliminary Support for SMT QF_AUFBV, http://groups.google.co.uk/groupcprover, The CProver Group, 2009.- [7] L. Cordeiro, B. Fischer, and J. Marques-Silva, "SMT-Based Bounded Model Checking for Embedded ANSI-C Software,"
Proc. Int'l Conf. Automated Software Eng., pp. 137-148, 2009.- [8] L. Cordeiro, B. Fischer, and J. Marques-Silva, "Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking,"
Proc. Int'l Conf. and Workshops Eng. Computer-Based Systems, pp. 160-169, 2010.- [9] SMT-LIB,
The Satisfiability Modulo Theories Library, http:// combination.cs.uiowa.edusmtlib, 2009.- [10] A. Stump and M. Deters,
Satisfiability Modulo Theories Competition, http:/www.smtcomp.org/, 2010.- [11] E. Clarke, D. Kroening, and F. Lerda, "A Tool for Checking ANSI-C Programs,"
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 168-176, 2004.- [12] C. Wintersteiger,
Compiling GOTO-Programs, http://www. cprover.orggoto-cc/, 2009.- [13] R.L. Sites, "Some Thoughts on Proving Clean Termination of Programs," technical report, Stanford, Calif., 1974.
- [14] A.R. Bradley and Z. Manna,
The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.- [15] M. Bozzano et al., "Encoding RTL Constructs for MathSAT: A Preliminary Report,"
Electrical Notes in Theoretical Computer Science, vol. 144, no. 2, pp. 3-14, 2006.- [16] C. Barrett and C. Tinelli, "CVC3,"
Proc. Int'l Conf. Computer Aided Verification, pp. 298-302, 2007.- [17] R. Brummayer and A. Biere, "Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays,"
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 174-177, 2009.- [18] L.M. de Moura and N. Bjørner, "Z3: An Efficient SMT Solver,"
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, 2008.- [19] J. Mccarthy, "Towards a Mathematical Science of Computation,"
Proc. Int'l Federation of Information Processing Congress, pp. 21-28, 1962.- [20] S.S. Muchnick,
Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, Inc., 1997.- [21] E. Clarke, D. Kroening, J. Ouaknine, and O. Strichman, "Computational Challenges in Bounded Model Checking,"
Software Tools for Technology Transfer, vol. 7, no. 2, pp. 174-183, 2005.- [22] L.M. de Moura and N. Bjørner, "Satisfiability Modulo Theories: An Appetizer,"
Proc. Brazilian Symp. Formal Methods, pp. 23-36, 2009.- [23] E. Clarke, D. Kroening, O. Strichman, and J. Ouaknine, "Completeness and Complexity of Bounded Model Checking,"
Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 85-96, 2004.- [24] M.K. Ganai and A. Gupta, "Completeness in SMT-Based BMC for Software Programs,"
Proc. Conf. Design, Automation and Test in Europe, pp. 831-836, 2008.- [25] A.S. Tanenbaum,
Computer Networks, fourth ed. Prentice-Hall, Inc., 2002.- [26] E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, "Predicate Abstraction of ANSI-C Programs Using SAT,"
Formal Methods in System Design, vol. 25, pp. 105-127, 2004.- [27] S.-S. Lim,
Seoul Nat'l Univ. Real-Time Benchmarks Suite, http://archi.snu.ac.kr/realtimebenchmark /, 2009.- [28] D. Kroening and O. Strichman,
Decision Procedures: An Algorithmic Point of View. Springer, 2008.- [29] D. Gries and G. Levin, "Assignment and Procedure Call Proof Rules,"
ACM Trans. Programming Languages and Systems, vol. 2, no. 4, pp. 564-579, 1980.- [30] D. Kroening, E. Clarke, and K. Yorav, "Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking," technical report, CMU-CS-03-126, Carnegie Mellon Univ., 2003.
- [31] J.A. Clause and A. Orso, "Leakpoint: Pinpointing the Causes of Memory Leaks,"
Proc. IEEE/ACM 32nd Int'l Conf. Software Eng., vol. 1, pp. 515-524, 2010.- [32] D. Kroening and S.A. Seshia, "Formal Verification at Higher Levels of Abstraction,"
Proc. Int'l Conf. Computer-Aided Design, pp. 572-578, 2007.- [33] S. Gupta,
High Level Synthesis Benchmarks Suite, http://mesl. ucsd.edu/sparkbenchmarks.shtml , 2009.- [34] K. Ku, T.E. Hart, M. Chechik, and D. Lie, "A Buffer Overflow Benchmark for Software Model Checkers,"
Proc. Int'l Conf. Automated Software Eng., pp. 389-392, 2007.- [35] L. Platania,
Eureka Benchmark Suite, http://www.ai-lab.it/eurekabmc.html, 2009.- [36] S. Sankaranarayanan,
NECLA Static Analysis Benchmarks, http://www.nec-labs.com/researchsystem/, 2009.- [37] J. Scott, L.H. Lee, A. Chin, J. Arends, and B. Moyer, "Designing the Low-Power m∗Core Architecture,"
Proc. Int'l Symp. Computer Architecture Power Driven Microarchitecture Workshop, pp. 145-150, 1998.- [38] A. Ermedahl and J. Gustafsson,
Worst-Case Execution Time Project/Benchmarks, http://www.mrtc.mdh.se/projectswcet/, 2009.- [39] T. Ostrand,
Siemens Corporate Research, http://sir.unl.eduportal/, 2010.- [40] NXP,
High Definition IP and Hybrid DTV Set-Top Box STB225, http:/www.nxp.com/, 2009.- [41]
MiBench Version 1.0, http://www.eecs.umich.edumibench/, 2009.- [42] A. Biere, "Picosat Essentials,"
J. Satisfiability, Boolean Modeling and Computation, vol. 4, nos. 2-4, pp. 75-97, 2008.- [43] M. Ramanathan,
Flex, http://sir.unl.eduportal/, 2010.- [44] J. Morse,
Kerberos Git, https://www.studentrobotics.org/trac/wiki/ KerberosGit, 2011.- [45] N.L. Vinh,
The Flasher Manager Application, http://users.polytech. unice.fr/rueher/Benchs FM/, 2010.- [46] F. Ivancic, personal communication, 2011.
- [47] M. Chechik, personal communication, 2011.
- [48] L. Xu, "SMT-Based Bounded Model Checking for Real-Time Systems,"
Proc. Int'l Conf. Quality Software, pp. 120-125, 2008.- [49] A. Donaldson, D. Kroening, and P. Rümmer, "Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors,"
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 280-295, 2010.- [50] L.M. de Moura, H. Rueß, and M. Sorea, "Lazy Theorem Proving for Bounded Model Checking over Infinite Domains,"
Proc. Int'l Conf. Automated Deduction, pp. 438-455, 2002.- [51] P.B. Jackson, B.J. Ellis, and K. Sharp, "Using SMT Solvers to Verify High-Integrity Programs,"
Proc. Second Workshop Automated Formal Methods, pp. 60-68, 2007.- [52] P.B. Jackson and G.O. Passmore,
Proving SPARK Verification Conditions with SMT Solvers, technical report, Univ. of Edinburgh, http://homepages.inf.ed.ac.uk/pbj/papers vct-dec09-draft.pdf, 2009.- [53] D. Babić and A.J. Hu, "Calysto: Scalable and Precise Extended Static Checking,"
Proc. IEEE/ACM Int'l Conf. Software Eng., pp. 211-220, 2008.- [54] Y. Xie and A. Aiken, "Scalable Error Detection Using Boolean Satisfiability,"
SIGPLAN Notices, vol. 40, pp. 351-363, 2005.- [55] C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, "Extended Static Checking for Java,"
Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 234-245, 2002.- [56] D. Detlefs, G. Nelson, and J.B. Saxe, "Simplify: A Theorem Prover for Program Checking,"
J. ACM, vol. 52, no. 3, pp. 365-473, 2005.- [57] L. Cordeiro, "SMT-Based Bounded Model Checking for Multi-Threaded Software in Embedded Systems,"
Proc. ACM/IEEE 32nd Int'l Conf. Software Eng., pp. 373-376, 2010.- [58] L. Cordeiro and B. Fischer, "Verifying Multi-Threaded Software Using SMT-Based Context-Bounded Model Checking,"
Proc. ACM/IEEE 33rd Int'l Conf. Software Eng., pp. 331-340, 2011.- [59] R.C. Andreas, B. Cook, A. Podelski, and A. Rybalchenko, "Terminator: Beyond Safety,"
Proc. Int'l Conf. Computer Aided Verification, pp. 415-418, 2006.- [60] R. Jhala and R. Majumdar, "Software Model Checking,"
ACM Computing Surveys, vol. 41, no. 4, pp. 1-54, 2009.- [61] A. Podelski and A. Rybalchenko, "ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement,"
Proc. Ninth Int'l Symp. Practical Aspects of Declarative Languages, pp. 245-259, 2007.- [62] D. Beyer, T. Henzinger, R. Jhala, and R. Majumdar, "The Software Model Checker Blast,"
Int'l J. Software Tools Technology Transfer, vol. 9, nos. 5/6, pp. 505-525, 2007.- [63] K. McMillan, "Interpolation and Sat-Based Model Checking,"
Proc. Int'l Conf. Computer Aided Verification, pp. 1-13, 2003.- [64] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement,"
Proc. Int'l Conf. Computer Aided Verification, pp. 154-169, 2000. |