Publications

Below you find my publications. Please note that in April 2017, I changed my name from Scheurer to Steinhöfel, and that I have written papers with both names.

A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows

Autor Dominic Steinhöfel, Nathan Wasser
Datum April 2017
Art Techreport
KeywordsProgram Verification, Loop Invariants, Abnormal Termination, Non-Standard Control Flow, Symbolic Execution, Proof Size Reduction
SchlüsselTUD-CS-2017-0057
Forschungsgebiete Software Engineering
Abstrakt Invariants are a standard concept for reasoning about unbounded loops since Floyd-Hoare logic in the late 1960s. For real-world languages like Java, loop invariant rules tend to become extremely complex. The main reason is non-standard control flow induced by return, throw, break, and continue statements, possibly combined and nested inside inner loops and try blocks. We propose the concept of a loop scope which gives rise to a new approach for the design of invariant rules. This permits “sandboxed” deduction-based symbolic execution of loop bodies which in turn allows a modular analysis even of complex loops. Based on the new concept we designed a loop invariant rule for Java that has full language coverage and implemented it in the program verification system KeY. Its main advantages are (1) much increased comprehensibility, which made it considerably easier to argue for its soundness, (2) simpler and easier to understand proof obligations, (3) a substantially decreased number of symbolic execution steps and sizes of resulting proofs in a representative set of experiments. We also show that the new rule, in combination with fully automatic symbolic state merging, realizes even greater proof size reduction and helps to address the state explosion problem of symbolic execution.
Vollständiges Paper (pdf)
[Diesen Eintrag nach BibTeX exportieren]

Important Copyright Notice:

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Raum S2 02 | A223
E-Mail: steinhoefel(a-t)cs.tu-darmstadt.de
Tel.: +49 6151 16-21955

A A A | Drucken Print | Impressum Impressum | Sitemap Sitemap | Suche Search | Kontakt Contact | Webseitenanalyse: Mehr Informationen
zum Seitenanfangzum Seitenanfang