Wednesday
| Start | End | Title |
|---|---|---|
| 11:30 | 12:00 | Arrival and Registration |
| 12:00 | 13:30 | Lunch |
| 13:30 | 14:45 | Session I: Verification of Automated Production Systems
|
| 14:45 | 15:15 | Coffee Break |
| 15:15 | 17:15 | Session II: Usability for Program Verification
|
Thursday
Friday
[row]
[column md=”6″]
Opening!
[/column]
[column md=”6″]
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″]
https://formal.kastel.kit.edu/stvs
[/column]
[column md=”6″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[column md=”6″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[column md=”6″]
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″]
[/column]
[column md=”6″]
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″]
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″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[column md=”6″]
Create IDE / Editor / Parser for DSLs. Use those tools with KeY-ABS. Reference project
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[column md=”6″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
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″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[column md=”6″]
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″]
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″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
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″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
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″]
No abstract given.
[/column]
[/row]
[row]
[column md=”6″]
No abstract given.
[/column]
[/row]
Opening Ceremony
Alexander Weigl, Sarah Grebing
Schedule: 13:30 – 13:45Opening!
Generalised Test Tables: A Practical Specification Language for Reactive Systems
Alexander Weigl
Schedule: 13:45 – 14:15In 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.
Structured Verification Studio
Carsten Csiky
Schedule: 14:15 – 14:30https://formal.kastel.kit.edu/stvs
Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software
Anja Blechinger
Schedule: 14:30 – 14:45No abstract given.
Proof Scripting Language Concept
Sarah Grebing
Schedule: 15:15 – 15:35No abstract given.
Seamless Interaction Concept for Program Verification
Sarah Grebing, Philip Krüger
Schedule: 15:35 – 16:15No abstract given.
Specifying and Verifying Real-World Java Code with KeY – Case Study java.math.BigInteger
Wolfram Pfeifer
Schedule: 16:15 – 16:45No abstract given.
Discussion: JML object invariants after exceptions in constructors
Wolfram Pfeifer, Mattias Ulbrich
Schedule: 16:45 – 17:15In 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.
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.A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
Dominic Steinhöfel
Schedule: 10:30 – 11:00Abstract. 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.
Assessing the Coverage of Formal Specifications
Dominic Steinhöfel
Schedule: 11:00 – 11:30Deductive 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.
Update on the On-Going KeY Refactoring
Eduard Kamburjan
Schedule: 11:30 – 12:00No abstract given.
Update on KeY-ABS
Eduard Kamburjan
Schedule: 13:30 – 14:00No abstract given.
Implementing Domain-Specific Languages with Xtext
Igor Lunev, Paul Thieme
Schedule: 14:00 – 14:30Create IDE / Editor / Parser for DSLs. Use those tools with KeY-ABS. Reference project
Measuring the Abstractness of Statemachines
Thomas Baar
Schedule: 14:30 – 15:00No abstract given.
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Moritz Kiefer
Schedule: 15:30 – 16:00No abstract given.
Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages
Reiner Hähnle
Schedule: 16:00 – 17:00A 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.
Relational Verification for Floating Points
Jonas Klamroth
Schedule: 17:00 – 17:30No abstract given.
We meet at entrance of the hotel ca. 19:00.
The guidance start at 19:30 in front of the tourist information.
[/column]
[column md=”6″]
Touristinformation am Schloss Herrenstraße 18The south-side of the Rastatt’s castle.
Support for Distributed Systems in KeY – Specification and Verification of JavaEE Remote Mehods
Karsten Diekhoff
Schedule: 09:15 – 09:45No abstract given.
Specification and Verification of Information Flow Properties for Components in Distributed Systems
Jonas Krämer
Schedule: 09:45 – 10:15No abstract given.
Modelling of Autosar Libraries for Large Scale Testing
Wojciech Mostowski
Schedule: 10:45 – 11:15We 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.
Combining Graph-Based and Deduction-Based Information-Flow Analysis
Mihai Herda
Schedule: 11:15 – 11:45Information 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.
Tales from the Trenches – One Year in Industry
Vladimir Klebanov
Schedule: 11:45 – 12:00No abstract given.
Formal Fairness Properties in Network Routing Based on a Resource Allocation Model
Michael Kirsten
Schedule: 13:30 – 14:00Network 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.
BEAST – automated election verification via bounded model checking
Lukas Stapelbroek
Schedule: 14:00 – 14:15No abstract given.
Computing Exact Loop Bounds for Bounded Program Verification
Tianhai Liu
Schedule: 14:15 – 14:45Bounded 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.
Closing Discussion
tba
Schedule: 14:45 – 15:45No abstract given.
Closing Cerenomy
Sarah Grebing, Alexander Weigl
Schedule: 15:45 – 16:00No abstract given.
</div Generated: 2017-10-30 18:19:54.212605