Title :
PuMoC: a CTL model-checker for sequential programs
Author :
Fu Song ; Touili, Tayssir
Author_Institution :
LIAFA, Univ. Paris Diderot, Paris, France
Abstract :
In this paper, we present PuMoC, a CTL model checker for Pushdown systems (PDSs) and sequential C/C++ and Java programs. PuMoC allows to do CTL model-checking w.r.t simple valuations, where the atomic propositions depend on the control locations of the PDSs, and w.r.t. regular valuations, where atomic propositions are regular predicates over the stack content. Our tool allowed to (1) check 500 randomly generated PDSs against several CTL formulas; (2) check around 1461 versions of 30 Windows drivers taken from SLAM benchmarks; (3) check several C and Java programs; and (4) perform data flow analysis of real-world Java programs. Our results show the efficiency and the applicability of our tool.
Keywords :
C++ language; Java; formal verification; C-C++ language; CTL model checker; Java program; PuMoC model checker; Windows driver; atomic proposition; data flow analysis; pushdown system; Branching-time Temporal Logic; Model-Checking; Pushdown Systems; Software Model-Checking;
Conference_Titel :
Automated Software Engineering (ASE), 2012 Proceedings of the 27th IEEE/ACM International Conference on
Print_ISBN :
978-1-4503-1204-2
DOI :
10.1145/2351676.2351743
