DocumentCode :
3144623
Title :
Towards a Framework for Scalable Model Checking of Concurrent C Programs
Author :
Wang, Ji ; Yi, Xiaodong ; Yang, Xuejun
Author_Institution :
Nat. Lab. for Parallel & Distributed Process., Changsha
fYear :
2006
fDate :
15-19 Nov. 2006
Firstpage :
355
Lastpage :
362
Abstract :
The paper presents a novel framework for scalable model checking of concurrent C programs. With the idea of verification reuse, it shows an integrated approach to efficient reduction of state space by abstraction, symbolic representation and dynamic partial-order reduction (DPOR) techniques. The framework is founded on an over-approximated model of the concurrent program by variable abstraction, and combines DPOR with lightweight symbolic execution to generate the symbolic conditions for all locations, called -conditions, which are intended for verification reuse. The -conditions of a location are weak approximation of the conditions that must be satisfied at that location so as to guarantee the temporal safety properties to be verified. These conditions will be checked for reusing the previous exploration in verification, and will be iteratively refined under the guidance of spurious counterexamples. The presented framework is demonstrated by several experiments including a concurrent software system whose server and client processes are derived from openssl-0.9.6c C source codes implementing the SSL protocol.
Keywords :
multiprocessing programs; program verification; concurrent C program; dynamic partial-order reduction; scalable model checking; state space reduction; symbolic representation; Distributed processing; Interleaved codes; Java; Laboratories; Open source software; Safety; Scalability; Software systems; Space exploration; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006. Second International Symposium on
Conference_Location :
Paphos
Print_ISBN :
978-0-7695-3071-0
Type :
conf
DOI :
10.1109/ISoLA.2006.69
Filename :
4463736
Link To Document :
بازگشت