This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modular Verification of Software Components in C
June 2004 (vol. 30 no. 6)
pp. 388-402
ASCII Text
x 
 
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith, "Modular Verification of Software Components in C," IEEE Transactions on Software Engineering, vol. 30, no. 6, pp. 388-402, June, 2004.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2004.22,
author = {Sagar Chaki and Edmund M. Clarke and Alex Groce and Somesh Jha and Helmut Veith},
title = {Modular Verification of Software Components in C},
journal ={IEEE Transactions on Software Engineering},
volume = {30},
number = {6},
issn = {0098-5589},
year = {2004},
pages = {388-402},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2004.22},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Modular Verification of Software Components in C
IS - 6
SN - 0098-5589
SP388
EP402
EPD - 388-402
A1 - Sagar Chaki,
A1 - Edmund M. Clarke,
A1 - Alex Groce,
A1 - Somesh Jha,
A1 - Helmut Veith,
PY - 2004
KW - Software engineering
KW - formal methods
KW - verification.
VL - 30
JA - IEEE Transactions on Software Engineering
ER -
 

Abstract—We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the CounterExample Guided Abstraction Refinement (CEGAR) paradigm, our tool magic first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, weak simulation is checked via a reduction to Boolean satisfiability. magic has been interfaced with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel, the OpenSSL toolkit, and several industrial strength benchmarks.

[1] D. Harel, Statecharts: A Visual Formalism for Complex Systems Science of Computer Programming, vol. 8, no. 3, pp. 231-274, June 1987.
[2] Unified Modeling Language http:/www.uml.org, 2002.
[3] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
[4] E. Clarke, S. Jha, and W. Marrero, Verifying Security Protocols with Brutus ACM Trans. Software Eng. Methodology (TOSEM), vol. 9, no. 4, 2000.
[5] G. Lowe, S.A. Schneider, B. Roscoe, M.H. Goldsmith, P.Y.A. Ryan, and A. Roscoe, Modelling and Analysis of Security Protocols. Addison-Wesley, Dec. 2000.
[6] Business Process Execution Language for Web Services http://www.oasis-open.org/coverbpel4ws.html , 2002.
[7] M.B. Dwyer and L.A. Clarke, Data Flow Analysis for Verifying Properties of Concurrent Programs Proc. Foundations of Software Eng. Symp. (FSE), 1994.
[8] K.M. Olender and L.J. Osterweil, Interprocedural Static Analysis of Sequencing Constraints ACM Trans. Software Eng. Methodology (TOSEM), vol. 1, no. 1, pp. 21-52, 1992.
[9] R.L. Smith, G.S. Avrunin, L.A. Clarke, and L.J. Osterweil, PROPEL: An Approach Supporting Property Elucidation Proc. Int'l Conf. Software Eng. (ICSE), 2002.
[10] MAGIC http://www.cs.cmu.edu/~chakimagic, 2002.
[11] R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
[12] C.A.R. Hoare, Communicating Sequential Processes Comm. ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.
[13] R. Milner, Communicating and Mobile Systems: The -Calculus. Cambridge Univ. Press, 1999.
[14] T. Ball and S.K. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces Lecture Notes in Computer Science, vol. 2057, 2001.
[15] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement Computer Aided Verification, pp. 154-169, 2000.
[16] M.B. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, and H. Zheng, “Tool-Supported Program Abstraction for Finite-State Verification,” Proc. 23rd Int'l Conf. Software Eng., pp. 177–187, May 2001.
[17] T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy Abstraction Proc. Symp. Principles of Programming Languages, pp. 58-70, 2002.
[18] S. Das, D.L. Dill, and S. Park, Experience with Predicate Abstraction Computer Aided Verification, pp. 160-171, 1999.
[19] S. Graf and H. Saidi, Construction of Abstract State Graphs with PVS Computer Aided Verification, O. Grumberg, ed., vol. 1254, pp. 72-83, 1997.
[20] G. Nelson, Techniques for Program Verification PhD dissertation, Stanford Univ., 1980.
[21] A. Stump, C. Barrett, and D. Dill, CVC: A Cooperating Validity Checker Proc. Conf. Computer-Aided Verification, 2002.
[22] J.-C. Filliatre, S. Owre, H. Ruess, and N. Shankar, ICS: Integrated Canonizer and Solver Computer-Aided Verification, 2001.
[23] CVC Lite http://chicory.stanford.eduCVCL, 2002.
[24] D. Kroening, Application Specific Higher Order Logic Theorem Proving Proc. Verification Workshop (VERIFY '02), pp. 5-15, July 2002.
[25] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver Proc. 38th Design Automation Conf., pp. 530-535, 2001.
[26] J.P. Marques-Silva and K.A. Sakallah, GRASP A New Search Algorithm for Satisfiability Proc. IEEE/ACM Int'l Conf. Computer-Aided Design, Nov. 1996.
[27] H. Zhang, SATO: An Efficient Propositional Prover Proc. Conf. Automated Deduction, 1997.
[28] S. Chaki, E. Clarke, S. Jha, and H. Veith, Strategy Guided Abstraction Refinement Technical Report CMU-CS-03-188, Carnegie Mellon Univ., 2003.
[29] Bandera http://www.cis.ksu.edu/santosbandera, 2002.
[30] Java PathFinder http://ase.arc.nasa.gov/visserjpf, 2002.
[31] K. Havelund and T. Pressburger, Model Checking JAVA Programs Using JAVA Pathfinder Proc. Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366 381, 2000.
[32] ESC-Java http://www.research.compaq.com/SRCesc, 2002.
[33] SLAM http://research.microsoft.comslam, 2002.
[34] BLAST http://www-cad.eecs.berkeley.edu/~rupakblast , 2002.
[35] D. Engler, B. Chelf, A. Chou, and S. Hallem, Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions Proc. Symp. Operating Systems Design and Implementation, 2000.
[36] S. Hallem, B. Chelf, Y. Xie, and D. Engler, A System and Language for Building System-Specific, Static Analyses Proc. SIGPLAN Conf. Programming Language Design and Implementation, 2002.
[37] E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications ACM Trans. Programming Languages and System (TOPLAS), vol. 8, no. 2, pp. 244-263, Apr. 1986.
[38] E.M. Clarke, O. Grumberg, and D.E. Long, Model Checking and Abstraction ACM Trans. Programming Languages and System (TOPLAS), vol. 16, no. 5, pp. 1512-1542, Sept. 1994.
[39] T. Ball, A. Podelski, and S.K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs Lecture Notes in Computer Science, vol. 2031, pp. 268-283, 2001.
[40] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking Without BDDs Lecture Notes in Computer Science, vol. 1579, pp. 193-207, 1999.
[41] D. Jackson, Automating Relational Logic Proc. ACM SIGSOFT Conf. Foundations of Software Eng. (FSE), Nov. 2000.
[42] D. Jackson and K. Sullivan, COM Revisited: Tool-Assisted Modelling and Analysis of Complex Software Structures Proc. ACM SIGSOFT Conf. Foundations of Software Eng., Nov. 2000.
[43] S. Khurshid and D. Jackson, Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer Proc. 15th IEEE Int'l Conf. Automated Software Eng. (ASE), Sept. 2000.
[44] S.K. Shukla, Uniform Approaches to the Verification of Finite State Systems PhD dissertation, State Univ. of New York, Albany, 1997.
[45] W.F. Dowling and J.H. Gallier, Linear Time Algorithms for Testing the Satisfiability of Propositional Horn Formula J. Logic Programming, vol. 3, pp. 267-284, 1984.
[46] G. Ausiello and G.F. Italiano, On-Line Algorithms for Polynomially Solvable Satisfiability Problems J. Logic Programming, vol. 10, nos. 1-4, pp. 69-90, Jan. 1991.
[47] CIL http://manju.cs.berkeley.educil, 2002.
[48] J. Magee and J. Kramer, Concurrency: State Models&Java Programs. Wiley, 2000.
[49] E.W. Dijkstra, A Simple Axiomatic Basis for Programming Language Constructs lecture notes from the Int'l Summer School on Structured Programming and Programmed Structures, 1973, http://www.cs.utexas.edu/users/EWD/ewd03xx EWD372. PDF.
[50] C.A.R. Hoare, An Axiomatic Basis for Computer Programming Comm. ACM, vol. 12, no. 10, pp. 576-580, 1969.
[51] D. Dams and K.S. Namjoshi, Shape Analysis through Predicate Abstraction and Model Checking Proc. Conf. Verification, Model Checking and Abstract Interpretation, 2003.
[52] L. Anderson, Program Analysis and Specialization for the C Programming Language PhD dissertation, Datalogisk Intitut, Univ. of Copenhagen, Denmark, 1994.
[53] S.K. Shukla, H.B.H. III, and D.J. Rosenkrantz, HORNSAT, Model Checking, Verification and Games Technical Report TR-95-8, State Univ. of New York, Albany, 1995.
[54] OpenSSL http:/www.openssl.org, 2002.
[55] SSL 3.0 Specification http://wp.netscape.com/engssl3, 2002.
[56] A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzé, Using Symbolic Execution for Verifying Safety-Critical Systems Proc. Eighth European Software Eng. Conf., pp. 142-151, 2001.
[57] C. Livadas, J. Lygeros, and N.A. Lynch, High-Level Modeling and Analysis of the Traffic Alert and Collision Avoidance System (TCAS) Proc. IEEE, special issue on hybrid systems: theory and applications, vol. 88, no. 7, pp. 926-948, July 2000.
[58] S. Chaki, E. Clarke, A. Groce, and O. Strichman, Predicate Abstraction with Minimum Predicates Proc. 12th Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME), Oct. 2003.
[59] S. Chaki, J. Ouaknine, K. Yorav, and E. Clarke, Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach Electronic Notes in Theoretical Computer Science, B. Cook et al., eds., vol. 89, 2003.
[60] S. Chaki, E. Clarke, J. Ouaknine, N. Sinha, and N. Sharygina, State/Event-Based Software Model Checking Proc. Fourth Int'l Conf. Integrated Formal Methods (IFM), to appear.

Index Terms:
Software engineering, formal methods, verification.
Citation:
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith, "Modular Verification of Software Components in C," IEEE Transactions on Software Engineering, vol. 30, no. 6, pp. 388-402, June 2004, doi:10.1109/TSE.2004.22
Usage of this product signifies your acceptance of the Terms of Use.