KeY-Symposium 2008 - Program
Program:
Wednesday,
Thursday,
Friday
Attention: Presentations written in
italic font have changed date and time.
Time |
Topic |
| 14.00 - 14.15 |
Welcome |
| 14.15 - 14.45 |
Peter H. Schmitt: Formal Methods in Avionics |
| 14:45 - 15:00 |
Hendrik Post: Applications of Software Bounded Model Checking |
| 15:00 - 15:30 |
Angela Wallenburg: Induction Formula Generalisation |
| 15:30 - 16:00 |
Fika (Coffee Break) |
| 16:00 - 16:30 |
Benjamin Weiß: Loop Invariant Inference in JavaDL |
| 16:30 - 17:00 |
Volker Klasen: Stable Saving and Loading of Proofs |
| 17:00 - 17:45 |
New Feature Session
- Benjamin Weiß: New Specification Language Front-Ends
- Jochen Seidel: Query Treatment in Modalities
- Christian Engel: Treatment of Inner Classes
- Mattias Ulbrich: KeY Treck - The \classpath Directive
|
Time |
Topic |
| 9:00 - 9:30 |
Wojciech Mostowski: Malicious Code on Java Card Smartcards: Attacks and Countermeasures |
| 9:30 - 9:45 |
Frank Werner: Applying Verification Techniques in Sensor Networks |
| 9:45 - 10:15 |
Christoph Scheben: Verification of Sun Spot's Network Library |
| 10:15 - 10:45
| Fika (Coffee Break) |
| 10:45 - 11:15 |
Vladimir Klebanov: Proving Java Memory Model Safety of Java Programs |
| 11:15 - 11:45 |
Christian Engel: Verification of Real-Time Specification for
Java (RTSJ) Programs |
| 11:45 - 12:15 |
Richard Bubel: Predicates With Explicit Dependencies |
| 12:15 - 14:00 | Lunch |
| 14:00 - 14:30 |
Christoph Gladisch: Test Generation with Loop Invariants and Method Specifications |
| 14:30 - 15:00 |
Markus Bender: Generating Efficient Test Oracles From Specifications |
| 15:00 - 15:30 |
Marcel Rothe: Extending the Visual Debugger |
| 15:30 - 16:00 | Fika (Coffee Break) |
| 16:00 - 18:00 |
Discussions
- Reiner Hähnle: Efficient and more versatile symbolic execution (intermediate/core language)
- Reiner Hähnle and Vladimir Klebanov: Alternative/additional user views
- Push-button Mode for KeY
- Interaction Mode for KeY
- Cleaner sequent view (invisible formulas, preconditions on the left, etc.)
- Peter H. Schmitt: Semantics of anonymous and anonymising updates
|
19:00 |
Social Event (Restaurant Yamato) |
Time |
Topic |
| 9.00 - 9.30 |
Thorsten Bormer + Markus Wagner: The Verisoft XT Project |
| 9.30 - 10.00 |
Ongoing and Planned Projects: DIANA, HATS, MOBIUS, ZEUS |
| 10.00 - 10.30 |
Fika (Coffee Break) |
| 10:30 - 11:00 |
Denis Lohner: Verification of Java Floating-Point Arithmetic |
| 11:00 - 11:15 |
Richard Bubel: Classes of Non-Rigid Symbols in KeY |
| 11.15 - 12.00 |
Discussions
- Richard Bubel: Suggestion and road-map for a nearly
complete rewrite of our term data structures
- Richard Bubel: Git-Repository layout (what to do with side-branches,
squash commits etc.)
|
| 12:00 - | Lunch |
