Programme of KeY Symposium 2017

Wednesday

StartEndTitle
11:30 12:00 Arrival and Registration
12:00 13:30 Lunch
13:30 14:45 Session I: Verification of Automated Production Systems
  1. Opening Ceremony
    Alexander Weigl, Sarah Grebing (13:30-13:45)
  2. Generalised Test Tables: A Practical Specification Language for Reactive Systems
    Alexander Weigl (13:45-14:15)
  3. Structured Verification Studio
    Carsten Csiky (14:15-14:30)
  4. Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software
    Anja Blechinger (14:30-14:45)
14:45 15:15 Coffee Break
15:15 17:15 Session II: Usability for Program Verification
  1. Proof Scripting Language Concept
    Sarah Grebing (15:15-15:35)
  2. Seamless Interaction Concept for Program Verification
    Sarah Grebing, Philip Krüger (15:35-16:15)
  3. Specifying and Verifying Real-World Java Code with KeY – Case Study java.math.BigInteger
    Wolfram Pfeifer (16:15-16:45)
  4. Discussion: JML object invariants after exceptions in constructors
    Wolfram Pfeifer, Mattias Ulbrich (16:45-17:15)

Thursday

StartEndTitle
09:00 10:00 Invited Talk: Why3 ‐ where programs meet provers.
Jean-Christophe Filliâtre
10:00 10:30 Break
10:30 12:00 Session III: Deductive Verification with KeY
  1. A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
    Dominic Steinhöfel (10:30-11:00)
  2. Assessing the Coverage of Formal Specifications
    Dominic Steinhöfel (11:00-11:30)
  3. Update on the On-Going KeY Refactoring
    Eduard Kamburjan (11:30-12:00)
12:00 13:30 Lunch
13:30 15:00 Session IV: ABS
  1. Update on KeY-ABS
    Eduard Kamburjan (13:30-14:00)
  2. Implementing Domain-Specific Languages with Xtext
    Igor Lunev, Paul Thieme (14:00-14:30)
  3. Measuring the Abstractness of Statemachines
    Thomas Baar (14:30-15:00)
15:00 15:30 Break
15:30 17:30 Session V
  1. Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
    Moritz Kiefer (15:30-16:00)
  2. Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages
    Reiner Hähnle (16:00-17:00)
  3. Relational Verification for Floating Points
    Jonas Klamroth (17:00-17:30)
17:45 18:45 Dinner
19:00 21:00 Social Event: Guide through Raststatt with a night guard

Friday

StartEndTitle
09:00 09:15 Check out until 09:00!
09:15 10:15 Session VI: Security in Component-based Systems
  1. Support for Distributed Systems in KeY – Specification and Verification of JavaEE Remote Mehods
    Karsten Diekhoff (09:15-09:45)
  2. Specification and Verification of Information Flow Properties for Components in Distributed Systems
    Jonas Krämer (09:45-10:15)
10:15 10:45 Break
10:45 12:00 Session VII
  1. Modelling of Autosar Libraries for Large Scale Testing
    Wojciech Mostowski (10:45-11:15)
  2. Combining Graph-Based and Deduction-Based Information-Flow Analysis
    Mihai Herda (11:15-11:45)
  3. Tales from the Trenches – One Year in Industry
    Vladimir Klebanov (11:45-12:00)
12:00 13:30 Lunch
13:30 14:15 Session VIII: Social Choice Theory
  1. Formal Fairness Properties in Network Routing Based on a Resource Allocation Model
    Michael Kirsten (13:30-14:00)
  2. BEAST – automated election verification via bounded model checking
    Lukas Stapelbroek (14:00-14:15)
14:15 16:00 Session IX
  1. Computing Exact Loop Bounds for Bounded Program Verification
    Tianhai Liu (14:15-14:45)
  2. Closing Discussion
    tba (14:45-15:45)
  3. Closing Cerenomy
    Sarah Grebing, Alexander Weigl (15:45-16:00)
[row] [column md=”6″]

Opening Ceremony

Alexander Weigl, Sarah Grebing

Schedule: 13:30 – 13:45


Opening!

[/column] [column md=”6″]

Generalised Test Tables: A Practical Specification Language for Reactive Systems

Alexander Weigl

Schedule: 13:45 – 14:15


In industrial practice today, correctness of software is rarely verified using formal techniques. One reason is the lack of specification languages for this application area that are both comprehensible and sufficiently expressive. We present the concepts and logical foundations of generalised test tables — a specification language for reactive systems accessible for practitioners. Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. The semantics of generalised test tables is based on a two-party game over infinite words.

We show how generalised test tables can be encoded into verification conditions for state-of-the-art model checkers. And we demonstrate the applicability of the language by an example in which a function block in a programmable logic controller as used in automation industry is specified and verified.

[/column] [/row] [row] [column md=”6″]

Structured Verification Studio

Carsten Csiky

Schedule: 14:15 – 14:30


https://formal.iti.kit.edu/stvs

[/column] [column md=”6″]

Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software

Anja Blechinger

Schedule: 14:30 – 14:45


No abstract given.

[/column] [/row] [row] [column md=”6″]

Proof Scripting Language Concept

Sarah Grebing

Schedule: 15:15 – 15:35


No abstract given.

[/column] [column md=”6″]

Seamless Interaction Concept for Program Verification

Sarah Grebing, Philip Krüger

Schedule: 15:35 – 16:15


No abstract given.

[/column] [/row] [row] [column md=”6″]

Specifying and Verifying Real-World Java Code with KeY – Case Study java.math.BigInteger

Wolfram Pfeifer

Schedule: 16:15 – 16:45


No abstract given.

[/column] [column md=”6″]

Discussion: JML object invariants after exceptions in constructors

Wolfram Pfeifer, Mattias Ulbrich

Schedule: 16:45 – 17:15


In Java a constructor may throw an exception. Has the object invariant to hold after the exceptional termination of the constructor? JML says yes, but there are examples that suggest the opposite. We will briefly discuss which understanding fits KeY’s invariant semantics best.

[/column] [/row] [row] [column md=”6″]

Invited Talk


Jean-Christophe Filliatre

Slides

Regarding the demo, here is a pointer to the example in our gallery:

http://toccata.lri.fr/gallery/maximum_subarray.en.html

It contains several solutions, the last of which is the one used in my demo. This is in the syntax of the current, distributed version of Why3 (while I used the development version of Why3 during my demo).

I may have to rush to the station soon (it looks my return train has disappeared as well) without saying good bye properly. Thanks for everything, I had a very nice time in Rastatt.

[/column] [column md=”6″]

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

Dominic Steinhöfel

Schedule: 10:30 – 11:00


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 a new approach for the design of invariant rules based on the concept of a loop scope. This permits “sandboxed” 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.

[/column] [/row] [row] [column md=”6″]

Assessing the Coverage of Formal Specifications

Dominic Steinhöfel

Schedule: 11:00 – 11:30


Deductive program verification is an intricate and time-consuming task, in spite of significant advances in state-of-the-art program provers. While proving the correctness of programs with respect to existing specifications can already be difficult, it can be even more demanding to come up with sensible specifications for methods and especially for loops. Another issue is related to programs heavily making use of software libraries: Their verification can be considered almost infeasible due to the lack of formal specifications of the libraries. We propose a method for assessing the coverage/strength of formal specifications based on “facts” extracted using heavyweight symbolic execution. We envision that this method can be employed for (1) assisting verification engineers in the incremental specification of programs, (2) comparing different specifications for the same program, and (3) obtaining information for specification generation tools. Our approach has been implemented as a prototype for Java which uses the heavyweight symbolic execution system KeY as a backend. We studied its practicability with several small examples and plan to conduct a more extensive case study in the near future.

[/column] [column md=”6″]

Update on the On-Going KeY Refactoring

Eduard Kamburjan

Schedule: 11:30 – 12:00


No abstract given.

[/column] [/row] [row] [column md=”6″]

Update on KeY-ABS

Eduard Kamburjan

Schedule: 13:30 – 14:00


No abstract given.

[/column] [column md=”6″]

Implementing Domain-Specific Languages with Xtext

Igor Lunev, Paul Thieme

Schedule: 14:00 – 14:30


Create IDE / Editor / Parser for DSLs. Use those tools with KeY-ABS.

Reference project

[/column] [/row] [row] [column md=”6″]

Measuring the Abstractness of Statemachines

Thomas Baar

Schedule: 14:30 – 15:00


No abstract given.

[/column] [column md=”6″]

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

Moritz Kiefer

Schedule: 15:30 – 16:00


No abstract given.

[/column] [/row] [row] [column md=”6″]

Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages

Reiner Hähnle

Schedule: 16:00 – 17:00


A formal, mathematically precise semantics for a programming language is the essential prerequisite for the design of logics and calculi that permit automated reasoning about programs. The most popular approach to programming language semantics — small step operational semantics (SOS) — is not modular in the sense that it does not separate conceptual layers in the target language. SOS is also hard to relate formally to program logics and calculi. Low-level semantic formalisms, such as automata, Petri nets, or π-calculus are inadequate for rich programming languages. We propose a new formal semantics for a concurrent, active objects language. It is designed with the explicit aim of being compatible with a sequent calculus for a program logic and has a strong model theoretic flavor. Our semantics separates sequential and object-local from concurrent computation: the former yields abstract traces which in a second stage are combined into global system behavior.

[/column] [column md=”6″]

Relational Verification for Floating Points

Jonas Klamroth

Schedule: 17:00 – 17:30


No abstract given.

[/column] [/row] [row] [column md=”6″]

We meet at entrance of the hotel ca. 19:00.

The guidance start at 19:30 in front of the tourist information.

Touristinformation am Schloss Herrenstraße 18

The south-side of the Rastatt’s castle.

[/column] [column md=”6″]

Support for Distributed Systems in KeY – Specification and Verification of JavaEE Remote Mehods

Karsten Diekhoff

Schedule: 09:15 – 09:45


No abstract given.

[/column] [/row] [row] [column md=”6″]

Specification and Verification of Information Flow Properties for Components in Distributed Systems

Jonas Krämer

Schedule: 09:45 – 10:15


No abstract given.

[/column] [column md=”6″]

Modelling of Autosar Libraries for Large Scale Testing

Wojciech Mostowski

Schedule: 10:45 – 11:15


We demonstrate a specific method and technology for model-based testing of large software projects with the QuickCheck tool using property-based specifications. Our specifications are very precise, state-full models of the software under test (SUT). In our approach we define (a) formal descriptions of valid function call sequences (public API), (b) postconditions that check the validity of each call, and (c) call-out specifications that define and validate external system interactions (SUT calling external API). The QuickCheck tool automatically generates and executes tests from these specifications. Commercially, this method and tool have been used to test large parts of the industrially developed automotive libraries based on the Autosar standard. In this paper, we exemplify our approach with a circular buffer specified by Autosar, to demonstrate the capabilities of the model-based testing method of QuickCheck. Our example is small compared to the commercial QuickCheck models, but faithfully addresses many of the same challenges.

[/column] [/row] [row] [column md=”6″]

Combining Graph-Based and Deduction-Based Information-Flow Analysis

Mihai Herda

Schedule: 11:15 – 11:45


Information flow control (IFC) is a category of techniques for ensuring system security by enforcing information flow properties such as non-interference. Established IFC techniques range from fully automatic approaches with much over-approximation to approaches with high precision but potentially laborious user interaction. A noteworthy approach mitigating the weaknesses of both automatic and interactive IFC techniques is the hybrid approach, developed by Küsters et al., which – however – is based on program modifications and still requires a significant amount of user interaction.

In this paper, we present a combined approach that works without any program modifications. It minimizes potential user interactions by applying a dependency-graph-based information-flow analysis first. Based on over-approximations, this step potentially generates false positives. Precise non-interference proofs are achieved by applying a deductive theorem prover with a specialized information-flow calculus for checking that no path from a secret input to a public output exists. Both tools are fully integrated into a combined approach, which is evaluated on a case study, demonstrating the feasibility of automatic and precise non-interference proofs for complex programs.

[/column] [column md=”6″]

Tales from the Trenches – One Year in Industry

Vladimir Klebanov

Schedule: 11:45 – 12:00


No abstract given.

[/column] [/row] [row] [column md=”6″]

Formal Fairness Properties in Network Routing Based on a Resource Allocation Model

Michael Kirsten

Schedule: 13:30 – 14:00


Network routing –being a central part of our everyday life, which increasingly depends on internet services– is highly distributed. It must provide for a variety of different services, each accommodating different requirements. Thereby, the access to network services is often very different between multiple users or agents, who are nonetheless expecting the same quality, e.g., regarding speed or availability. This work establishes a formal model of network routing, stepping into fair allocation theory, in order to develop formal fairness properties within this model. We furthermore derive possible fairness criteria from established notions in fair allocation theory.

[/column] [column md=”6″]

BEAST – automated election verification via bounded model checking

Lukas Stapelbroek

Schedule: 14:00 – 14:15


No abstract given.

[/column] [/row] [row] [column md=”6″]

Computing Exact Loop Bounds for Bounded Program Verification

Tianhai Liu

Schedule: 14:15 – 14:45


Bounded program verification techniques verify functional properties of programs by analyzing the program for user-provided bounds on the number of objects and loop iterations. Whereas those two kinds of bounds are related, existing bounded program verification tools treat them as independent parameters and require the user to provide them. We present a new approach for automatically calculating exact loop bounds based on the number of objects; i.e. when a bound is found, it is always the precise one, thus ensuring that the verification is complete with respect to all the configurations of objects on the heap, enhancing the confidence in the correctness of the analyzed program. We compute the loop bounds by encoding the program and its specification as a logical formula and solve it using an SMT solver. We have performed experiments to evaluate the precision of our approach in loop bounds computation.

[/column] [column md=”6″]

Closing Discussion

tba

Schedule: 14:45 – 15:45


No abstract given.

[/column] [/row] [row] [column md=”6″]

Closing Cerenomy

Sarah Grebing, Alexander Weigl

Schedule: 15:45 – 16:00


No abstract given.

[/column] [/row]
table { width: 100%; border-collapse:collapse; } .type-B { background: lavender; } .type-S { background: linen; } .type-SE { background: indigo; color: white; } .type-IT { background: khaki; } .type-D, .type-L { background: lavender; } .type-NT { background: #cfb; } .type-error {background:red;} tr { border-top: 1px solid black; border-bottom: 1px solid black; } tr:first-child { border-top: none; } tr:last-child { border-bottom: none; } td {padding:0.2em;} li { margin-bottom:0.5em; } a[onclick] { text-decoration: underline; color: blue; cursor: pointer; } th.start { width:5em; text-align:center; } th.end{ width:5em; text-align:center; } th.title{ width:auto; text-align:center; visibility:hidden; } td.start {vertical-align:top;} td.end {vertical-align:bottom;} div.abstract { border: dotted 1px black; padding: 2em; } .speaker { font-style: italic; } .session-name { font-size:120%; font-weight: bold; }