4th International Verification Workshop - VERIFY'07

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

Bremen, July 15-16, 2007

in connection with CADE-21

Keynote Speakers

A. Cimatti (IRST Trento)
T. Nipkow (TU Munich)
A. Stump (Washington U in St. Louis)
C. Tinelli (U of Iowa)

Program & Workshop Chair

B. Beckert (U of Koblenz)

Program Committee

S. Autexier (DFKI & U Saarbrücken)
Y. Bertot (INRIA Sophia Antipolis)
B. Dutertre (SRI International)
R. Hähnle (Chalmers U, Gothenburg)
D. Hutter (DFKI Saarbrücken)
A. Ireland (Heriot-Watt U, Edinburgh)
D. Kapur (U of New Mexico)
J.-P. Katoen (RWTH Aachen)
J. Kiniry (U Dublin)
H. Mantel (RWTH Aachen)
F. Massacci (U of Trento)
S. Merz (INRIA Lorraine)
T. Mossakowski (U of Bremen)
L. Paulson (U of Cambridge)
W. Reif (U of Augsburg)
J. Richardson (Powerset Inc.)
L. Viganò (U of Verona)
C. Walther (TU Darmstadt)

Steering Committee

S. Autexier (DFKI & U Saarbrücken)
H. Mantel (RWTH Aachen)

Call for papers

PDF - ASCII



CADE-21 

Important dates

Extended Abstract Submission Deadline: May 21, 2007

Extended Paper Submission Deadline: May 25, 2007

Notification of acceptance: June 8, 2007

Early registration deadline: June 10, 2007 (tentative)

Final version due: June 21th, 2007

Workshop date: July 15-16, 2007

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

Workshop Schedule and Programme (Tentative)

Day 1: Sunday, July 15

09:15 - 09:30
 Welcome
09:30 - 10:30
 Invited Talk
Tobias Nipkow
Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic
10:30 - 11:00
 Break
11:00 - 11:30
 Jia Meng, Lawrence Paulson and Gerwin Klein
A Termination Checker for Isabelle Hoare Logic
11:30 - 12:00 Mamoun Filali
A Mechanization of Phylogenetic Trees
12:00 - 12:30 Peter H. Schmitt and Benjamin Weiss
Inferring Invariants by Symbolic Execution
12:30 - 14:00 Lunch
14:00 - 14:30
 Andre Platzer
Combining Deduction and Algebraic Constraints for Hybrid System Analysis
14:30 - 15:00 Wojciech Mostowski
Fully Verified Java Card API Reference Implementation
15:00 - 15:30 Olivera Pavlovic, Ralf Pinger and Maik Kollmann
Automation of Formal Verification of PLC Programs Written in IL
15:30 - 16:00 Break
16:00 - 16:30 Daniel Larsson and Reiner Hähnle
Symbolic Fault Injection
16:30 - 17:00 Till Mossakowski, Christian Maeder and Klaus Lüttich
The Heterogeneous Tool Set (Hets)
17:00 - 17:30 Borislav Gajanovic and Bernhard Rumpe
ALICE: An Advanced Logic for Interactive Component Engineering

Day 2: Monday, July 16

11:30 - 12:00

 Special Invited Talks Session on Satisfiability Modulo Theories (joint with DISPROVING and CFV)
09:00 - 10:00
 Invited Talk
Cesare Tinelli
Trends and Challenges in Satisfiability Modulo Theories
10:00 - 11:00
 Invited Talk
Alessandro Cimatti
Satisfiability Modulo the Theory of Bit Vectors
11:00 - 11:30
 Break

Joint Session with DISPROVING
Alan Bundy
Where's My Stuff? An Ontology Repair Plan
(DISPROVING Talk)
12:00 - 12:30
 Philipp Rümmer
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
(VERIFY Talk)
12:30 - 14:00 Lunch
14:00 - 15:00
 Invited Talk
Aaron Stump
Lightweight Verification with Dependent Types
15:00 - 15:30 Eyad Alkassar, Mark Hillebrand, Steffen Knapp, Rostislav Rusev and Sergey Tverdyshev
Formal Device and Programming Model for a Serial Interface
15:30 - 16:00 Break
16:00 - 16:30 Pascal Fontaine
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class
16:30 - 17:00 Bruno Langenstein, Andreas Nonnengart, Georg Rock, and Werner Stephan
A History-based Verification of Distributed Applications
17:00 - 17:30 Discussion and Closing Session
Bernhard Beckert