6th International Verification Workshop – VERIFY-2010

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

Edinburgh, July 20–21, 2010

in connection with IJCAR 2010

Keynote Speakers

V. Cortier (LORIA INRIA-Lorraine, France)
C. Jones (Newcastle University, UK)
A. Platzer (Carnegie Mellon University, USA)

Program & Workshop Chairs

M. Aderhold (TU Darmstadt)
S. Autexier (DFKI Bremen)
H. Mantel (TU Darmstadt)

Program Committee

B. Beckert (Karlsruhe Institute of Technology, Germany)
I. Cervesato (Carnegie Mellon University, Qatar)
C. Fournet (Microsoft Research, Cambridge)
J. Guttman (Worcester Polytechnic Institute, USA)
R. Hähnle (Chalmers University, Sweden)
J. Hurd (Galois, Inc., USA)
D. Hutter (DFKI Bremen, Germany)
P. Jackson (University of Edinburgh, UK)
C. Jones (Newcastle University, UK)
D. Kapur (University of New Mexico, USA)
J.-P. Katoen (RWTH Aachen, Germany)
G. Klein (NICTA, Australia)
G. Lowe (University of Oxford, UK)
F. Martinelli (CNR Pisa, Italy)
C. Meadows (Naval Research Laboratory, USA)
D. Pichardie (INRIA Rennes, France)
G. Schneider (University of Gothenburg, Sweden)
J. Schumann (NASA Ames Research Center, USA)
C. Walther (TU Darmstadt, Germany)

Call for papers



Important dates

Abstract Submission Deadline: April 7, 2010
Paper Submission Deadline: April 11, 2010
Notification of acceptance: April 29, 2010
Final version due: May 17, 2010
Workshop date: July 20–21, 2010

Previous VERIFY workshops


If you need further information, do not hesitate to
contact the workshop chairs by sending an e-mail
to verify2010@mais.informatik.tu-darmstadt.de.


Day 1: Tuesday, July 20, 2010

08:50 Welcome by the Chairs

09:00–10:00 Session 1: Invited Talk

09:00 Cliff Jones
Abstractions Before Proofs

10:00–10:30 Coffee Break

10:30–12:30 Session 2: Verification in Various Domains

10:30 Angelo Brillout, Daniel Kroening, Philipp Rümmer, and Thomas Wahl
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
11:10 Shuling Wang and Xu Wang
Proving Four-Slot Algorithm Using Ownership Transfer (slides)
11:50 Michael von Tessin
Towards High-Assurance Multiprocessor Virtualisation

12:30–14:00 Lunch Break

14:00–15:00 Session 3: Invited Talk

14:00 Véronique Cortier
Verification of Security Protocols (slides)

15:00–15:30 Coffee Break

15:30–17:00 Session 4: Verification of IT-Security

15:30 Mark Bickford
Automated Proof of Authentication Protocols in a Logic of Events
16:10 Bernhard Beckert, Daniel Bruns, and Sarah Grebing
Mind the Gap: Formal Verification and the Common Criteria (slides)

19:00 Workshop Dinner

Day 2: Wednesday, July 21, 2010

09:00–10:00 Session 5: Invited Talk

09:00 André Platzer
Real Analysis for Complex Systems

10:00–10:30 Coffee Break

10:30–12:30 Session 6: Verification Techniques and Tools

10:30 Joe Hurd
Composable Packages for Higher Order Logic Theories (slides)
11:10 Andrei Lapets
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
11:50 Alessandro Carioni, Silvio Ghilardi, and Silvio Ranise
MCMT in the Land of Parametrized Timed Automata

12:30–13:50 Lunch Break — ATTENTION: The next session already starts at 13:50.

13:50–15:10 Session 7: Software Security and Software Testing

13:50 Daniel Wasserrab and Denis Lohner
Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing (slides)
14:30 Enrico Giunchiglia, Massimo Narizzano, Gabriele Palma, and Alessandra Puddu
Automatic generation of high quality test sets via CBMC

15:10–15:30 Coffee Break

15:30–17:00 Session 8: Panel Discussion (joint with ASA-4)

15:30 Riccardo Focardi, Jon Geater, Andrew Gordon, Cliff Jones, Mark Ryan, Johann Schumann
Panel Discussion: Formal Methods for/in/as Industry

Markus Aderhold, Serge Autexier, Heiko Mantel
Last modified: August 6, 2010