9.00 10.00 |
ESOP Invited Talk Greg Morrisett (Cornell University, USA) Type Checking Systems Code Session chair: Daniel Le Métayer |
|||
10.00 10.45 |
Coffee | |||
10.45 12.45 |
TACAS Software verification Session chair: Wang Yi Relative Completeness of Abstraction Refinement for Software Model Checking Towards the Automated Verification of Multithreaded Java Programs CLPS-B - A Constraint Solver for B Formal Verification of Functional Properties of an SCR-style Software Requirements Specification using PVS |
FASE Tool Demos Session chair: Peter Mosses The Coordination Development Environment The KeY System: Integrating Object-Oriented Design and Formal Methods ObjectCheck: A Model Checking Tool for Executable Object-oriented Software System Designs Demonstration of an Operational Procedure for the Model-Based Testing of CTI Systems |
ESOP Program analysis : applications Session chair: Julia Lawall Tool Support for Improving Test Coverage Data Space-Oriented Tiling Propagation of Roundoff Errors in Finite Precision Computations: a Semantics Approach Asserting the Precision of Floating-Point Computations: a Simple Abstract Interpreter (demo paper) |
ACL |
12.45 14.15 |
Lunch | |||
14.15 15.15 |
TACAS Invited Talk Michael Lowry (NASA Ames Research Center) Software Construction and Analysis Tools for Future Space Missions Session chair: Perdita Stevens |
|||
15.15 16.00 |
Coffee | |||
16.00 17.30 |
TACAS Infinite-state and parametric systems Session chair: Bernard Steffen Beyond Parameterized Verification Resource-Constrained Model Checking of Recursive Programs Model Checking Large-scale and Parameterized Resource Allocation Systems |
FASE Meta-models Session chair: Ralf-D. Kutsche (Berlin, Germany) Engineering Modelling Languages: A Precise Meta-Modelling Approach ATOM3: A Tool for Multi-formalism Modelling and Meta-modelling A Toolbox for Automating Visual Software Engineering |
ESOP Program analysis : principles Session chair: David Sands A Modular, Extensible Proof Method for Small-step Flow Analyses A Prototype Dependency Calculus Automatic Complexity Analysis |
ACL |
17.30 17.45 |
Short Break | |||
17.45 18.45 |
TACAS Tool demo Session chair: Joost-Pieter Katoen Compositional Verification using SVL Scripts |
FASE Formal Approaches towards UML Session chair: Martin Grosse-Rhode (Berlin, Germany) Enriching OCL using observational mu-calculus Formal Verification of UML Statecharts with Real-time Extensions |
empty | ACL |
18:45 19:30 |
EASST General Assembly Session chair: |
|||
20.00 |