TU Darmstadt / ULB / TUbiblio

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

Steinhöfel, Dominic and Wasser, Nathan
Polikarpova, Nadia and Schneider, Steve (eds.) (2017):
A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows.
In: Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, Springer, In: Lecture Notes in Computer Science, ISBN 978-3-319-66844-4,
DOI: 10.1007/978-3-319-66845-1, [Conference or Workshop Item]

Abstract

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.

Item Type: Conference or Workshop Item
Erschienen: 2017
Editors: Polikarpova, Nadia and Schneider, Steve
Creators: Steinhöfel, Dominic and Wasser, Nathan
Title: A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
Language: German
Abstract:

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.

Title of Book: Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
Series Name: Lecture Notes in Computer Science
Volume: 10510
Publisher: Springer
ISBN: 978-3-319-66844-4
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 25 Sep 2017 15:56
DOI: 10.1007/978-3-319-66845-1
Identification Number: TUD-CS-2017-0251
Export:

Optionen (nur für Redakteure)

View Item View Item