Ludwig-Maximilians-University, Munich, Institute of Computer Science
Department for Programming and Software Engineering
Compositional Specification and Verification Parallel Programs
The aim of this project is twofold: on one hand, we want to apply formal
methods to the design and analysis of object-oriented distributed software.
On the other hand, we want to use object-oriented principles of
software construction in the application of formal methods. We try to
achieve reuse of both specifications and proofs in the design of complex
systems by subdividing such systems into agents of manageable complexity.
This requires a more fundamental understanding of different concepts of
composition, including parallel composition and "vertical"
composition of components that is motivated from the application of
object-oriented techniques.
Specifically, we study the following questions:
- assumption-commitment rules for compositional reasoning
- different logics for concurrent systems
- abstraction techniques that aim at reducing the state space
of complex systems
- computer-assisted analysis of systems such as model checking,
interactive theorem proving, and their combination
This Project has been partly supported by the DAAD as part of the PROCOPE program.
Project partner:
Applied Logics Group, Institut de recherche en informatique de Toulouse
Contact person:
Dr. Stephan Merz
Publications:
list of all projects
Institute
University
(16.12.1996)