KeY Project: Integrated Deductive Software Design

6th KeY Symposium 2007

Einar Broch Johnsen		Creol: A Formal Model of Distributed Concurrent Objects
Benjamin Weiß		Inferring Invariants by Static Analysis in KeY
Marcus Baum		Debugging by Visualizing Symbolic Execution
Christian Engel		Formal Verification of Performance Contracts
Philipp Rümmer		Integer Arithmetic in KeY
Mattias Ulbrich		Verification of Java 5 Programs
Helga Velroyen		Non-termination Proofs in Dynamic Logic
Christoph Gladisch		White-box Testing
Frank Piessens		Concern-specific Specification and Verification to Improve Software Quality and Security
Vladimir Klebanov		Verifying Library Code for Concurrent Access
Richard Bubel		Verification of the Schorr-Waite Algorithm
Peter H. Schmitt		The Mondex Case Study
Frank Werner		Analysing Probabilistic Network Flooding
Denis Lohner		Specifying the Java Collections Framework in JavaDL
Gerd Beuster		The Verisoft Email Client
Reiner Hähnle		Agile Formal Methods
Thorsten Bormer		Multi-formalism Specification and Verification in Verisoft
Henrik Johansson		Linear Unification Constraints vs. ACU-Unification
Oleg Mürk		Deductive Verification of C Programs with KeY
Joe Kiniry		Recent Advances in Extended Static Checking
Wojciech Mostowski		Fully Verified Java Card API Reference Implementation
André Platzer		Differential Dynamic Logic for Hybrid Systems