What are the verification problems? What are the deduction techniques?
Edinburgh, July 20–21, 2010
in connection with IJCAR 2010
Keynote SpeakersV. Cortier (LORIA INRIA-Lorraine, France)
C. Jones (Newcastle University, UK)
A. Platzer (Carnegie Mellon University, USA)
Program & Workshop ChairsM. Aderhold (TU Darmstadt)
S. Autexier (DFKI Bremen)
H. Mantel (TU Darmstadt)
Program CommitteeB. 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 papersPDF – ASCII
ContactIf you need further information, do not hesitate to
contact the workshop chairs by sending an e-mail
Véronique Cortier (LORIA INRIA-Lorraine, France): Verification of Security Protocols
Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed and are used to efficiently detect flaws.
In this talk, we will first review results and techniques that allow automatic analysis of security protocols. In a second part, we will present recent results that demonstrate that formal abstract models used for verification are actually sound with respect to much richer models that considers issues of complexity and probability. As a consequence, it is possible to derive strong, clear security guarantees still keeping the simplicity of reasoning in symbolic models.
Cliff Jones (Newcastle University, UK): Abstractions Before Proofs
Proving that programs satisfy their specifications can benefit enormously from tool support but theorem proving tools can also constrain a user's thinking. This talk argues that, for large or complex programs, it is layers of abstraction that make or break the comprehensibility of developments.
However powerful a theorem proving tool is, it will make little long-term contribution to the understanding of programs if the user is forced to bend their steps of development to fit the tool. Abstraction is essential to achieve separation of issues and to help in the understanding of complex systems. The formalism chosen governs the difficulty of completing detailed proofs that can be verified with mechanically checkable rules.
This talk will emphasise abstractions and techniques for reasoning about the development of concurrent programs. In conclusion, the argument will turn to positive recommendations for tool developers.
André Platzer (Carnegie Mellon University, USA): Real Analysis for Complex Systems
Formal verification techniques are used routinely in finite-state digital circuits. Theorem proving is also used successfully for infinite-state discrete systems. But many safety-critical computers are actually embedded in physical systems. Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. There is a well-understood theory for proving programs. But what about complex physical systems? How can we prove that a hybrid system works as expected, e.g., an aircraft does not crash into another one?
This talk illustrates the complexities and pitfalls of hybrid systems verification. It describes a theoretical and practical foundation for deductive verification of hybrid systems called differential dynamic logic. The proof calculus for this logic is interesting from a theoretical perspective, because it is a complete axiomatization of hybrid systems relative to differential equations. The approach is of considerable practical interest too. Its implementation in the theorem prover KeYmaera has been used successfully to verify collision avoidance properties in the European Train Control System and air traffic control systems. The number of dimensions and nonlinearities in they hybrid dynamics of these systems is surprisingly tricky such that they are still out of scope for other verification tools.