
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Lucas Cordeiro, Bernd Fischer, Joao MarquesSilva, "SMTBased Bounded Model Checking for Embedded ANSIC Software," IEEE Transactions on Software Engineering, vol. 38, no. 4, pp. 957974, JulyAug., 2012.  
BibTex  x  
@article{ 10.1109/TSE.2011.59, author = {Lucas Cordeiro and Bernd Fischer and Joao MarquesSilva}, title = {SMTBased Bounded Model Checking for Embedded ANSIC Software}, journal ={IEEE Transactions on Software Engineering}, volume = {38}, number = {4}, issn = {00985589}, year = {2012}, pages = {957974}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2011.59}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  SMTBased Bounded Model Checking for Embedded ANSIC Software IS  4 SN  00985589 SP957 EP974 EPD  957974 A1  Lucas Cordeiro, A1  Bernd Fischer, A1  Joao MarquesSilva, PY  2012 KW  Software engineering KW  formal methods KW  verification KW  model checking VL  38 JA  IEEE Transactions on Software Engineering ER   
[1] A. Biere, "Bounded Model Checking," Handbook of Satisfiability, pp. 457481, 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. 146162, 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. 6983, 2009.
[4] M.K. Ganai and A. Gupta, "Accelerating HighLevel Bounded Model Checking," Proc. Int'l Conf. ComputerAided Design, pp. 794801, 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. MarquesSilva, "SMTBased Bounded Model Checking for Embedded ANSIC Software," Proc. Int'l Conf. Automated Software Eng., pp. 137148, 2009.
[8] L. Cordeiro, B. Fischer, and J. MarquesSilva, "Continuous Verification of Large Embedded Software Using SMTBased Bounded Model Checking," Proc. Int'l Conf. and Workshops Eng. ComputerBased Systems, pp. 160169, 2010.
[9] SMTLIB, 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 ANSIC Programs," Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 168176, 2004.
[12] C. Wintersteiger, Compiling GOTOPrograms, http://www. cprover.orggotocc/, 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. 314, 2006.
[16] C. Barrett and C. Tinelli, "CVC3," Proc. Int'l Conf. Computer Aided Verification, pp. 298302, 2007.
[17] R. Brummayer and A. Biere, "Boolector: An Efficient SMT Solver for BitVectors and Arrays," Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 174177, 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. 337340, 2008.
[19] J. Mccarthy, "Towards a Mathematical Science of Computation," Proc. Int'l Federation of Information Processing Congress, pp. 2128, 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. 174183, 2005.
[22] L.M. de Moura and N. Bjørner, "Satisfiability Modulo Theories: An Appetizer," Proc. Brazilian Symp. Formal Methods, pp. 2336, 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. 8596, 2004.
[24] M.K. Ganai and A. Gupta, "Completeness in SMTBased BMC for Software Programs," Proc. Conf. Design, Automation and Test in Europe, pp. 831836, 2008.
[25] A.S. Tanenbaum, Computer Networks, fourth ed. PrenticeHall, Inc., 2002.
[26] E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, "Predicate Abstraction of ANSIC Programs Using SAT," Formal Methods in System Design, vol. 25, pp. 105127, 2004.
[27] S.S. Lim, Seoul Nat'l Univ. RealTime 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. 564579, 1980.
[30] D. Kroening, E. Clarke, and K. Yorav, "Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking," technical report, CMUCS03126, 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. 515524, 2010.
[32] D. Kroening and S.A. Seshia, "Formal Verification at Higher Levels of Abstraction," Proc. Int'l Conf. ComputerAided Design, pp. 572578, 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. 389392, 2007.
[35] L. Platania, Eureka Benchmark Suite, http://www.ailab.it/eurekabmc.html, 2009.
[36] S. Sankaranarayanan, NECLA Static Analysis Benchmarks, http://www.neclabs.com/researchsystem/, 2009.
[37] J. Scott, L.H. Lee, A. Chin, J. Arends, and B. Moyer, "Designing the LowPower m∗Core Architecture," Proc. Int'l Symp. Computer Architecture Power Driven Microarchitecture Workshop, pp. 145150, 1998.
[38] A. Ermedahl and J. Gustafsson, WorstCase 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 SetTop 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. 24, pp. 7597, 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, "SMTBased Bounded Model Checking for RealTime Systems," Proc. Int'l Conf. Quality Software, pp. 120125, 2008.
[49] A. Donaldson, D. Kroening, and P. Rümmer, "Automatic Analysis of ScratchPad Memory Code for Heterogeneous Multicore Processors," Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 280295, 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. 438455, 2002.
[51] P.B. Jackson, B.J. Ellis, and K. Sharp, "Using SMT Solvers to Verify HighIntegrity Programs," Proc. Second Workshop Automated Formal Methods, pp. 6068, 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 vctdec09draft.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. 211220, 2008.
[54] Y. Xie and A. Aiken, "Scalable Error Detection Using Boolean Satisfiability," SIGPLAN Notices, vol. 40, pp. 351363, 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. 234245, 2002.
[56] D. Detlefs, G. Nelson, and J.B. Saxe, "Simplify: A Theorem Prover for Program Checking," J. ACM, vol. 52, no. 3, pp. 365473, 2005.
[57] L. Cordeiro, "SMTBased Bounded Model Checking for MultiThreaded Software in Embedded Systems," Proc. ACM/IEEE 32nd Int'l Conf. Software Eng., pp. 373376, 2010.
[58] L. Cordeiro and B. Fischer, "Verifying MultiThreaded Software Using SMTBased ContextBounded Model Checking," Proc. ACM/IEEE 33rd Int'l Conf. Software Eng., pp. 331340, 2011.
[59] R.C. Andreas, B. Cook, A. Podelski, and A. Rybalchenko, "Terminator: Beyond Safety," Proc. Int'l Conf. Computer Aided Verification, pp. 415418, 2006.
[60] R. Jhala and R. Majumdar, "Software Model Checking," ACM Computing Surveys, vol. 41, no. 4, pp. 154, 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. 245259, 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. 505525, 2007.
[63] K. McMillan, "Interpolation and SatBased Model Checking," Proc. Int'l Conf. Computer Aided Verification, pp. 113, 2003.
[64] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "CounterexampleGuided Abstraction Refinement," Proc. Int'l Conf. Computer Aided Verification, pp. 154169, 2000.