Home
Consortium
Project Structure
Goals and Results
SP1: Methods and Tools
SP2: Academic System
SP3: Correct Industrial Hardware/SoftwareSystem
SP4: Biometric Identification System
SP5: Project Management
SP6: Automotive
Verisoft Repository
Publications
Press
Contact
Internal
Auf Deutsch, Bitte!

The work that is done in Subproject 1 aims at the integration of different deduction techniques in order to have a continuous verification.
We consider interactive as well as automatic deduction techniques.
The administration of the logical artefacts is managed by a repository that is developed in SP 1.
Furthermore, we develop a verification environment for cryptographie and security, which is used for the formalisation and verification of cryptographic primitives.
The tools and techniques that are developed within SP 1 are all evaluated directly with the help of the applications that are examined in SP2, SP3, SP4, and SP6.
An overview of the structure of SP 1 is given in the following figure.
For the verification of C0 programs, we develop a BigStep and a corresponding SmallStep semantics.
Based on both semantics a Hoare Logic and a C0 calculus for dynamic logic have been developed.
The verification tools are all based on the mentioned semantics.
In SP 1 we divide automatic methods into automatic theorem proves and special procedures for
 proving temporal properties,
 analysing C0 programs,
 analysing cryptographic protocols, and
 execution time analysis.
The integration of different automatic deduction techniques and the corresponding tools is illustrated in the following figure:
The integration of automatic theorem provers into interactive systems is shown in the following figure.
In addition to these generic techniques there are special procedure for the verification of temporal properties and for the analysis of programs, especially of programs working on pointer structures.
This part of the project handles cryptographic primitives, for example encryption, signatures, or hashing, in a formal way.
Furthermore, we develop and improve methods and techniques for the verification of cryptographic protocols.
The developed methods are evaluated at the early stages of the project with the help of the applications taken from SP 4.
Finally we will implement a verified system consisting of a host, a chipcard terminal, biosensors that are communicating with the help of a cryptographic protocol.
Further work is done with respect to the connection of the symbolic level of protocol verification and
the level of probabilistic protocol models.
The complete picture is given in the following figure.
 BigStep semantics and SmallStep semantics for C0, which form the semantic basis for the developed verification tools
 There is substantial progress in the correspondence proof between BigStep semantics und SmallStep semantics
 Hoare Logics for partial and total correctness
 C0calculus in dynamic logic
 Development method for state based systems working on pointer structures
 Tools for modelchecking and termination analysis
 Symbolic shape analysis tool
 Refinement tool for the verification of temporal properties
 Integration of automatic procedures and methods in VSE and Isabelle
 Procedure for the (automatic) analysis of cryptographic protocols
 Implementation of a strategy for the inductive verification of protocols in VSE (SP 4 protocol is verified)
 Refinement of cryptographic protocols has just started
 Formalisation of the mathematical basics of cryptography in Isabelle
 Basic functionality of the repository for the management of developments
 Andreas Podelski, Andrey Rybalchenko: Transition Invariants. Proc. 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland. July 1317, 2004.
 Amir Pnueli, Andreas Podelski, Andrey Rybalchenko: Separating Fairness and WellFoundedness for the Analysis of Fair Discrete Systems. Proc. of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, U.K. April 48, 2005.
 Andreas Podelski, Andrey Rybalchenko: Transition Predicate Abstraction and Fair Termination. Proc. of the 32nd ACM SIGPLAN  SIGACT Symposium on Principles of Programming Languages (POPL 2005), Long Beach, California, USA. January 1214, 2005.
 Bernd Finkbeiner, Henny Sipma: Checking Finite Traces using Alternating Automata. Formal Methods in System Design, vol 24, pages 101127. March 2004.
 Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma: Collecting Statistics over Runtime Executions. Formal Methods in System Design. To appear.
 Andreas Podelski, Ina Sch~fer, Silke Wagner: Summaries for While Programs with Recursion. Proc. of the European Symposium on Programming (ESOP 2005), Edinburgh, U.K., April 48, 2005.
 Jan Jürjens: Secure Systems Development with UML, SpringerVerlag, 2004.
 Jan Jürjens and Pasha Shabalin: Automated Verification of UMLsec Models for Security Requirements, UML 2004, Lisabon, Portugal Oct. 1115, 2004, LNCS, SpringerVerlag.
 Jan Jürjens and Pasha Shabalin: Tools for Critical Systems Development with UML, ETAPS 2005, Edinburgh, 210 April 2005, LNCS, SpringerVerlag
 Jan Jürjens: Sound Methods and Effective Tools for Modelbased Security Engineering with UML, 27th International Conference on Software Engineering, St. Louis, Missouri, USA; May 1521, 2005, IEEE Computer Society
11. Dieter Hutter, Axel Schairer: Possibilistic Information Flow Control in the Presence of Encrypted Communication. In Proceedings of
the 6th European Symposium on Research in Computer Security (ESORICS 2004), Springer, LNCS 3193, pp. 209224, 2004
 Dieter Hutter: Towards a generic management of change. In Proceedings of the Workshop on ComputerSupported Mathematical Theory
Development, International Joint Conference on Automated Reasoning, IJCAR2004, Cork, Ireland, 2004
 Till Mossakowksi, Piotr Hoffman, Serge Autexier, Dieter Hutter: CASL Logic. Part 4 of the CASL Reference Manual, P.D. Mosses (Ed.)
Springer, LNCS 2960, pp. 275324, 2004
 Till Mossakowski, Serge Autexier, Dieter Hutter: Extending development graphs with hiding. Journal of Logic and Algebraic Programming,
Special Issue on Algebraic Specification and Development Techniques. 2004
 Andreas Nonnengart, Georg Rock, Werner Stephan: Verification Support Environment (VSE), Fourth International Workshop on Planning and
Scheduling for Space  IWPSS '04, WPP228
 Dieter Hutter: A Management of Change. Ausarbeitung für Dagstuhl Seminar 03451 ``Applied Deductive Verification'', www.dagstuhl.de, 2003
