Refinement of Trace Abstraction | Zendy

Matthias Heizmann | Zendy; Jochen Hoenicke | Zendy; Andreas Podelski | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Refinement of Trace Abstraction

Author(s) -

Matthias Heizmann,

Jochen Hoenicke,

Andreas Podelski

Publication year - 2009

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/978-3-642-03237-0_7

Subject(s) - computer science , trace (psycholinguistics) , counterexample , automaton , theoretical computer science , abstraction , set (abstract data type) , büchi automaton , reuse , scheme (mathematics) , programming language , algorithm , construct (python library) , discrete mathematics , mathematics , deterministic automaton , philosophy , ecology , mathematical analysis , linguistics , epistemology , biology

We present a new counterexample-guided abstraction rene- ment scheme. The scheme renes an over-approximation of the set of possible traces. Each renement step introduces a nite automaton that recognizes a set of infeasible traces. A central idea enabling our approach is to use interpolants (assertions generated, e.g., by the infeasibility proof for an error trace) in order to automatically construct such an automa- ton. A data base of interpolant automata has an interesting potential for reuse of theorem proving work (from one program to another).

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research