Logo des Repositoriums

Auflistung nach Autor:in "Stahlbauer, Andreas"

1 - 3 von 3
  • Konferenzbeitrag
    Precision reuse in CPAchecker
    (Software Engineering 2014, 2014) Beyer, Dirk; Löwe, Stefan; Novikov, Evgeny; Stahlbauer, Andreas; Wendler, Philipp
  • Konferenzbeitrag
    Testing Scratch Programs Automatically
    (Software Engineering 2020, 2020) Stahlbauer, Andreas; Kreis, Marvin; Fraser, Gordon
    Block-based programming environments like Scratch foster engagement with computer programming and are used by millions of young learners. Scratch allows learners to quickly create entertaining programs and games, while eliminating syntactical program errors that could interfere with progress. However, functional programming errors may still lead to incorrect programs, and learners and their teachers need to identify and understand these errors. This is currently an entirely manual process. We introduce a formal testing framework that describes the problem of Scratch testing in detail, and instantiate this formal framework with the Whisker tool, which provides automated and property-based testing functionality for Scratch programs. Empirical evaluation on real student and teacher programs demonstrates that Whisker can successfully test Scratch programs, and automatically achieves an average of 95.25 % code coverage. This opens up new possibilities to support learners of programming in their struggles. This summary refers to the article \"Testing Scratch Programs Automatically\" published at the 27th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2019.
  • 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.