Paper Info
Title
Property Checking Without Invariant Generation.
Abstract
We introduce ProveProp, a procedure for proving safety properties. ProveProp is based on a technique called Partial Quantifier Elimination (PQE). In contrast to complete quantifier elimination, in PQE, only a part of the formula is taken out of the scope of quantifiers. So PQE can be dramatically more efficient than complete quantifier elimination. The appeal of ProveProp is twofold. First, it can prove a property without generating an inductive invariant. This is an implication of the fact that computing the reachability diameter of a system reduces to PQE. Second, PQE enables depth-first search, so ProveProp can be used to find very deep bugs. To prove property true, ProveProp has to consider traces of length up to the reachability diameter. This may slow down property checking for systems with a large diameter. We describe a variation of ProveProp that can prove a property without generation of long traces.
Year
Venue
Field
2016
arXiv: Logic in Computer Science
Quantifier elimination,Discrete mathematics,Model checking,Algorithm,Reachability,Invariant (mathematics),Mathematics
DocType
Volume
Citations 
Journal
abs/1602.05829
1
PageRank 
References 
Authors
0.48
6
1
Name
Order
Citations
PageRank
Eugene Goldberg1258.01