Paper Info
Title
Counterexample-Guided Prefix Refinement Analysis for Program Verification
Abstract
Counterexample-guided abstraction refinement (cegar) has become a successful approach to the automatic verification of program properties. Starting from a coarse abstract model, cegar incrementally refines the model based on spurious counterexamples that are retrieved from model checking attempts. In addition to purely symbolic representations of program states, recent work shows that a combination of an explicit-value and an abstract domain can be beneficial for cegar approaches. This paper introduces the counterexample-guided prefix refinement analysis (cegpra) that is based on the cegar idea and features a purely path-based model refinement. A first evaluation based on benchmarks from the rigorous examination of reactive systems (RERS) challenge indicates that cegpra is useful for analyzing a subset of temporal properties on large-scale reactive systems.
Year
DOI
Venue
2014
10.1007/978-3-319-51641-7_9
Communications in Computer and Information Science
Field
DocType
Volume
Kripke structure,Model checking,Programming language,Computer science,Model refinement,Theoretical computer science,Prefix,Abstraction refinement,Counterexample,Reactive system,Spurious relationship
Conference
683
ISSN
Citations 
PageRank 
1865-0929
0
0.34
References 
Authors
0
1
Name
Order
Citations
PageRank
Marc Jasper132.77