Counterexample-guided precondition inference
The precondition for an assertion inside a procedure is useful for understanding, verifying and debugging programs. As the procedure might be used in multiple calling-contexts within a program, the precondition should be sufficiently general to enable re-use. We present an extension of counterexampl...
| Main Authors: | , |
|---|---|
| Outros autores: | |
| Formato: | Conference item |
| Publicado: |
Springer
2013
|
| _version_ | 1826288726288891904 |
|---|---|
| author | Seghir, M Kroening, D |
| author2 | Felleisen, M |
| author_facet | Felleisen, M Seghir, M Kroening, D |
| author_sort | Seghir, M |
| collection | OXFORD |
| description | The precondition for an assertion inside a procedure is useful for understanding, verifying and debugging programs. As the procedure might be used in multiple calling-contexts within a program, the precondition should be sufficiently general to enable re-use. We present an extension of counterexample-guided abstraction refinement (CEGAR) for automated precondition inference. Starting with an over-approximation of both the set of safe and unsafe states, we iteratively refine them until they become disjoint. The resulting precondition is then necessary and sufficient for the validity of the assertion, which prevents false alarms. We have implemented our approach in a tool called P-Gen. We present experimental results on string and array-manipulating programs. |
| first_indexed | 2024-03-07T02:18:03Z |
| format | Conference item |
| id | oxford-uuid:a2f40b2c-a914-424a-bf63-f2004a402a88 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:18:03Z |
| publishDate | 2013 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:a2f40b2c-a914-424a-bf63-f2004a402a882022-03-27T02:23:28ZCounterexample-guided precondition inferenceConference itemhttp://purl.org/coar/resource_type/c_5794uuid:a2f40b2c-a914-424a-bf63-f2004a402a88Symplectic Elements at OxfordSpringer2013Seghir, MKroening, DFelleisen, MGardner, PThe precondition for an assertion inside a procedure is useful for understanding, verifying and debugging programs. As the procedure might be used in multiple calling-contexts within a program, the precondition should be sufficiently general to enable re-use. We present an extension of counterexample-guided abstraction refinement (CEGAR) for automated precondition inference. Starting with an over-approximation of both the set of safe and unsafe states, we iteratively refine them until they become disjoint. The resulting precondition is then necessary and sufficient for the validity of the assertion, which prevents false alarms. We have implemented our approach in a tool called P-Gen. We present experimental results on string and array-manipulating programs. |
| spellingShingle | Seghir, M Kroening, D Counterexample-guided precondition inference |
| title | Counterexample-guided precondition inference |
| title_full | Counterexample-guided precondition inference |
| title_fullStr | Counterexample-guided precondition inference |
| title_full_unstemmed | Counterexample-guided precondition inference |
| title_short | Counterexample-guided precondition inference |
| title_sort | counterexample guided precondition inference |
| work_keys_str_mv | AT seghirm counterexampleguidedpreconditioninference AT kroeningd counterexampleguidedpreconditioninference |