Logo des Repositoriums

Auflistung nach Autor:in "Dangl, Matthias"

1 - 2 von 2
  • Konferenzbeitrag
    Exchanging Verification Witnesses between Verifiers
    (Software Engineering 2017, 2017) Beyer, Dirk; Dangl, Matthias; Dietsch, Daniel; Heizmann, Matthias
    Standard verification tools provide a counterexample to witness a specifica- tion violation. Since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the violation can be shared across verifiers and the user can use standard tools to visualize and explore witnesses. This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, users often struggle to comprehend why a program is correct, and there is no way to independently check the verification result. We recently closed this gap by complementing our earlier work on violation witnesses with correctness witnesses. The overall goal to make proofs avail- able to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago — our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the principle of separation of concerns. At any time, the correctness witness can be used to recon- struct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPACHECKER and ULTIMATEAUTOMIZER, to produce and validate witnesses.
  • Konferenzbeitrag
    Verification Witnesses
    (Software Engineering 2016, 2016) Beyer, Dirk; Dangl, Matthias; Dietsch, Daniel; Heizmann, Matthias; Stahlbauer, Andreas
    It is commonly understood that a verification tool should provide a counterex-ample to witness a specification violation. Until recently, software verifiers dumped error witnesses in proprietary formats, which are often neither humannor machine-readable, and an exchange of witnesses between different verifiers was impossible. We have defined an exchange format for error witnesses that is easy to write and read by verification tools (for further processing, e.g., witness validation). To eliminate manual inspection of false alarms, we develop the notion of stepwise testification: in a first step, a verifier finds a problematic program path and, in addition to the verification result FALSE, constructs a witness for this path; in the next step, another verifier re-verifies that the witness indeed violates the specification. This process can have more than two steps, each reducing the state space around the error path, making it easier to validate the witness in a later step. An obvious application for testification is the setting where we have two verifiers: one that is efficient but imprecise and another one that is precise but expensive. The technique of error-witness-driven program analysis is implemented in two state-of-the-art verification tools, CPACHECKER and ULTIMATE AUTOMIZER.