5th International Verification Workshop - VERIFY'08

What are the verification problems? What are the deduction techniques?

Sydney, August 10-11, 2008

in connection with IJCAR 2008

Keynote Speakers

G. Barthe* (IMDEA Software, Madrid)
G. Heiser (National ICT Australia)
A. Groce* (NASA JPL)
P. Kalla* (U of Utah)

* invited jointly with the CFV Workshop

Program & Workshop Chairs

B. Beckert (U of Koblenz)
G. Klein (National ICT Australia)

Program Committee

S. Autexier (DFKI & U Saarbrücken)
G. Barthe (IMDEA Software, Madrid)
P. Baumgartner (National ICT Australia)
B. Dutertre (SRI International)
R. Hähnle (Chalmers U, Gothenburg)
A. Ireland (Heriot-Watt U, Edinburgh)
J. Kiniry (U Dublin)
H. Mantel (TU Darmstadt)
S. Merz (INRIA Lorraine)
C. Morgan (U of New South Wales)
P. Müller (Microsoft Research)
M. Norrish (National ICT Australia)
W. Paul (U Saarbrücken)
L. Paulson (U of Cambridge)
W. Reif (U of Augsburg)
W. Schulte (Microsoft Research)
J. Schumann (NASA Ames Research Center)
L. Viganò (U of Verona)
T. Walsh (National ICT Australia)
C. Walther (TU Darmstadt)

Steering Committee

S. Autexier (DFKI & U Saarbrücken)
H. Mantel (TU Darmstadt)

Call for papers

PDF - ASCII



IJCAR 

Important dates

Extended Abstract Submission Deadline: May 29, 2008

Extended Paper Submission Deadline: June 5, 2008

Notification of acceptance: June 30, 2008

Final version due: July 15th, 2008

Workshop date: Aug 10-11, 2008

Previous VERIFY workshops

Contact

If you need further information do not hesitate
to contact us by sending an e-mail to beckert@uni-koblenz.de and/or gerwin.klein@nicta.com.au

Workshop Schedule and Programme (PDF)

Day 1: Sunday, August 10

14:00 - 15:00 Invited Talk
Gernot Heiser
Operating System Verification for Real Use
Abstract
15:00 - 15:30 Niusha Hakimipour, Paul Strooper, Roger Duke
Exploring Model-Based Development for the Verification of Real-Time Java Code
15:30 - 16:00 Break
16:00 - 16:30 Simon Bäumler, Florian Nafz, Michael Balser, Wolfgang Reif
Compositional Proofs with Symbolic Execution
16:30 - 17:00 Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Specification Predicates with Explicit Dependency Information
17:00 - 18:00 Discussion
  • Verification of Operating Systems vs. Verification of Application Software
  • Verification and Software Certification
19:30 - Workshop Dinner

Day 2: Monday, August 11


 Joint Session with CFV
09:00 - 10:00
 Invited Talk
Alex Groce
Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving
10:00 - 10:30
 Break

Joint Session with CFV
10:30 - 11:30 Invited Talk
Priyank Kalla
Verification of Bit-Vector Arithmetic
11:30 - 12:00
 Matthias Daum, Jan Dörrenbächer, Sebastian Bogan
Model Stack for the Pervasive Verification of a Microkernel-based Operating System
12:00 - 12:30
 Masahiro Fujita et al.
Modular-HED: A Canonical Decision Diagram for Modular Equivalence Verification of Polynomial Functions
(CFV Talk)
12:30 - 14:00 Lunch

Joint Session with CFV
14:00 - 15:00
 Invited Talk
Gilles Barthe
Certificate Translation
Abstract
15:00 - 15:30 Nikolaj Bjørner, Leonardo de Moura, Nikolai Tillmann
Satisfiability Modulo Bit-precise Theories for Program Exploration
(CFV Talk)
15:30 - 16:00 Break
16:00 - 16:30 Hasan Amjad, Richard Bornat
Model Checking for Stability Analysis in Rely-Guarantee Proofs
16:30 - 17:00 David Cock
Bitfields and Tagged Unions in C: Verification through Automatic Generation
17:00 - 17:30 Gurvan Le Guernic
Precise Dynamic Verification of Confidentiality
17:30 - 17:45 Closing
18:00 -
 IJCAR Welcome Reception
Bernhard Beckert, Gerwin Klein