Recent Changes - Search:
FM /

MScThesisProposals

MSc thesis proposals from the Formal Methods group

I (Phillip Rümmer) list a few open research and/or implementation problems that might be suitable for Master's theses.

  • Integration of the infrastructure for program incorrectness proofs [3, 1] with the symbolic debugger front-end for KeY [4, 5].
    • The symbolic debugger is a front-end to KeY that visualises a proof in dynamic logic in terms of the investigated execution paths through a program (by showing the symbolic execution tree of a program). Such a visualisation can detect and help to more easily understand circumstances under which a fault occurs, in the sense that a proof of program correctness fails under such circumstances. Program incorrectness proofs could be used at this point to rule out false positives by actually proving the presence of a bug, and could compute classes of program inputs under which the bug causes a fault.
    • Non-termination checking [1] could be used to extend the realm of symbolic debugging to termination analysis.
    • The existing implementation to conduct incorrectness proofs is rather experimental and would have to be improved. One main issue with the old implementation is the lack of an efficient constraint solver, which might be solved by integrating the Princess theorem prover [2].
  • Non-termination checking for functional programs
    • Adapt the technique developed for imperative while-programs (with a single loop) [1] to programs with recursion and to functional programs. [1] works by synthesising an invariant for the loop in a program at hand, which might correspond to generating pre-conditions (and post-conditions?) for the various functions of a functional program.
    • [1] is implemented on top of KeY. For functional programs, it might be more efficient to write an own symbolic evaluator and directly integrate it into the Princess theorem prover [2].
    • How to handle algebraic datatypes?
    • Relationship to other techniques, like: non-termination proofs for term-rewrite systems; termination criteria in proof assistants like Isabelle, Coq, Agda.
  • Consistency checking for specifications
    • When specifying programs it is often convenient to use model functions, which are functions for which only the signature and some specification (pre/post-conditions) are known, but no implementation. Model functions are, in turn, meant to be used only in the specification of a program (and not in the implementation). An example of such a function might be a method for retrieving the i'th element of a linked list.
    • Due to the lack of an implementation, it is often not immediately clear that the specification of a model function is consistent and can be satisfied by a concrete function (either in the set-theoretic or the computational sense). The consistency of the specification can be necessary, however, to establish the soundness of a verification system. KeY does so far not offer any means to show the consistency of specifications.
    • Semantically, consistency checking means to ensure the existence of a model of the specification, and is thus related to model finding and to testing.
    • Related work: the paper [7]
    • It seems that a similar thesis is announced/proposed at the University of Karlsruhe. This would have to be coordinated
  • Support for generalised quantifiers (e.g. summation, products, counting)

[1] Helga Velroyen, Philipp Rümmer. Non-Termination Checking for Imperative Programs

[2] Philipp Rümmer. A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

[3] Philipp Rümmer, Muhammad Ali Shah. Proving Programs Incorrect using a Sequent Calculus for Java Dynamic Logic

[4] Marcus Baum. Debugging by Visualizing Symbolic Execution

[5] Marcel Rothe. Assisting the Understanding of Program Behavior by Using Symbolic Execution

[6] K. Rustan M. Leino, Rosemary Monahan. Reasoning about Comprehensions with First-Order SMT Solvers

[7] Arsenii Rudich, Ádám Darvas, Peter Müller. Checking Well-Formedness of Pure-Method Specifications