Property Checking Without Inductive Invariants
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2016
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917693614981120 |
|---|---|
| author | Goldberg, Eugene |
| author_facet | Goldberg, Eugene |
| contents | We introduce a procedure for proving safety properties. This procedure 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 our procedure is twofold. First, it can prove a property without generating an inductive invariant. Second, it employs depth-first search and so can be used to find deep bugs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1602_05829 |
| institution | arXiv |
| publishDate | 2016 |
| record_format | arxiv |
| spellingShingle | Property Checking Without Inductive Invariants Goldberg, Eugene Logic in Computer Science We introduce a procedure for proving safety properties. This procedure 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 our procedure is twofold. First, it can prove a property without generating an inductive invariant. Second, it employs depth-first search and so can be used to find deep bugs. |
| title | Property Checking Without Inductive Invariants |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/1602.05829 |