Using 3-valued memory representation for state space reduction in embedded assembly code model checking

2009 ◽  
Author(s):  
Thomas Reinbacher ◽  
Martin Horauer ◽  
Bastian Schlich
Keyword(s):  
Model Checking ◽  
State Space ◽  
Memory Representation ◽  
Assembly Code ◽  
Space Reduction ◽  
Code Model ◽  
State Space Reduction

State Space Reduction for Model Checking Agent Programs

2012 ◽  
pp. 133-151
Author(s):  
Sung-Shik T. Q. Jongmans ◽  
Koen V. Hindriks ◽  
M. Birna van Riemsdijk
Keyword(s):  
Model Checking ◽  
State Space ◽  
Space Reduction ◽  
State Space Reduction

SLICING EXECUTION FOR MODEL CHECKING C PROGRAMS

2006 ◽  
Vol 16 (05) ◽  
pp. 747-768 ◽  
Author(s):  
XIAODONG YI ◽  
JI WANG ◽  
XUEJUN YANG
Keyword(s):  
Model Checking ◽  
State Space ◽  
Considerable Improvement ◽  
Safety Properties ◽  
C Programs ◽  
Space Reduction ◽  
Efficient Reduction ◽  
Ssl Protocol ◽  
Novel Method ◽  
State Space Reduction

This paper presents a novel method, namely slicing execution, for model checking C programs with respect to temporal safety properties. The distinguished feature is that it shows a nice approach to the efficient reduction of state space by abstraction and symbolic representation. Slicing execution is founded on an over-approximated semantics of C programs by variable abstraction, and executes symbolically only the relevant statements under abstraction criteria to construct over-approximated finite models of programs, which may be model checked. The variable abstraction criterion begins with a proper initial set of program variables and may be iteratively refined according to spurious counterexamples generated during model checking. In general, the properties to be verified often involve only a few variables in practical programs. In these cases, significant state space reduction, as well as considerable improvement of the scalability, may be achieved. The presented method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c. The experiment results confirm that slicing execution is not only practical but also effective.

Sign in / Sign up

Export Citation Format

Share Document