Skip to main content

and
  1. No Access

    Chapter and Conference Paper

    The Gradual Verifier

    Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress o...

    Stephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf in NASA Formal Methods (2014)

  2. No Access

    Chapter and Conference Paper

    A Theory for Control-Flow Graph Exploration

    Detection of infeasible code has recently been identified as a scalable and automated technique to locate likely defects in software programs. Given the (acyclic) control-flow graph of a procedure, infeasible ...

    Stephan Arlt, Philipp Rümmer, Martin Schäf in Automated Technology for Verification and … (2013)

  3. No Access

    Chapter and Conference Paper

    Reconstructing Paths for Reachable Code

    Infeasible code has proved to be an interesting target for static analysis. It allows modular and scalable analysis, and at the same time, can be implemented with a close-to-zero rate of false warnings. The ch...

    Stephan Arlt, Zhiming Liu, Martin Schäf in Formal Methods and Software Engineering (2013)