Program Verification

@article{deGouw2017,
title = {Verifying OpenJDK's Sort Method for Generic Collections},
author = {Stijn de Gouw and Frank S de Boer and Richard Bubel and Reiner H\"{a}hnle and Jurriaan Rot and Dominic Steinh\"{o}fel},
url = {https://doi.org/10.1007/s10817-017-9426-4},
doi = {10.1007/s10817-017-9426-4},
issn = {1573-0670},
year = {2017},
date = {2017-01-01},
journal = {Journal of Automated Reasoning},
abstract = {TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}

@inproceedings{HentschelHB16ASE16a,
title = {An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {403-413},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@inproceedings{ HentschelHB16ASE16b,
title = {The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {846--851},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@phdthesis{ TUD-CS-2016-0099,
title = {Integrating Symbolic Execution, Debugging and Verification},
author = {Martin Hentschel},
year = {2016},
date = {2016-01-01},
school = {Technische Universit\"{a}t Darmstadt},
abstract = {In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}

@inproceedings{scheurer.hahnle.ea_general-lattice-model_16,
title = {A General Lattice Model for Merging Symbolic Execution Branches},
author = {Dominic Scheurer and Reiner H\"{a}hnle and Richard Bubel},
editor = {Kazuhiro Ogata and Mark Lawford and Shaoying Liu},
url = {http://link.springer.com/chapter/10.1007/978-3-319-47846-3_5
/wp-content/uploads/2016/12/SHB-General_Lattice_Model-2016.pdf},
doi = {10.1007/978-3-319-47846-3_5},
year = {2016},
date = {2016-01-01},
booktitle = {Formal Methods and Software Engineering - 18th International Conference
on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November
14-18, 2016, Proceedings},
volume = {10009},
pages = {57--73},
publisher = {Springer International Publishing},
series = {LNCS},
abstract = {Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@article{MostowskiU16,
title = {Dynamic Dispatch for Method Contracts Through Abstract Predicates},
author = {Wojciech Mostowski and Mattias Ulbrich},
url = {http://dx.doi.org/10.1007/978-3-319-46969-0_7},
doi = {10.1007/978-3-319-46969-0_7},
year = {2016},
date = {2016-01-01},
journal = {Trans. Modularity and Composition},
volume = {1},
pages = {238--267},
crossref = {DBLP:journals/taosd/2016-1},
keywords = {},
pubstate = {published},
tppubtype = {article}
}

@inproceedings{MostowskiU15,
title = {Dynamic Dispatch for Method Contracts through Abstract Predicates},
author = {Wojciech Mostowski and Mattias Ulbrich},
url = {http://doi.acm.org/10.1145/2724525.2724574},
doi = {10.1145/2724525.2724574},
year = {2015},
date = {2015-01-01},
booktitle = {Proceedings of the 14th International Conference on Modularity, MODULARITY
2015, Fort Collins, CO, USA, March 16 - 19, 2015},
pages = {109--116},
publisher = {ACM},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@article{bruns.mostowski.ea:implementation-level,
title = {Implementation-level Verification of Algorithms with KeY},
author = {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
url = {http://link.springer.com/article/10.1007/s10009-013-0293-y},
doi = {10.1007/s10009-013-0293-y},
issn = {1433-2779},
year = {2015},
date = {2015-01-01},
journal = {Software Tools for Technology Transfer},
volume = {17},
number = {6},
pages = {729--744},
publisher = {Springer},
abstract = {We give an account on the authors' experience and results from the software verification competition held at the Formal Methods~2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}

@inproceedings{KuestersTruderungBeckertEA2015,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
editor = {C'{e}dric Fournet and Michael Hicks},
doi = {10.1109/CSF.2015.28},
year = {2015},
date = {2015-01-01},
booktitle = {28th IEEE Computer Security Foundations Symposium (CSF 2015)},
pages = {305-319},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.


In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.


To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@article{KuestersTruderungBeckertEA2015b,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
url = {http://eprint.iacr.org/2015/438},
year = {2015},
date = {2015-01-01},
journal = {IACR Cryptology ePrint Archive},
volume = {2015},
pages = {438},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist.
Some of them have a high degree of automation or are even fully automatic, but overapproximate
the actual information flow, and hence, may produce false positives.
Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence,
analysis is time-consuming.


In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches:
We want to use fully automatic analysis as much as possible and only at places in a program where,
due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification of specific functional properties in certain
parts of the program, rather than checking more intricate noninterference properties for the whole
program.


To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully
automatic tool Joana for checking noninterference properties for Java programs and the theorem prover
KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung,
and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an
e-voting system.
The CVJ framework allows one to establish cryptographic indistinguishability properties for Java
programs by checking (standard) noninterference properties for such programs.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}