MSR - Verifikation von effektbasierten Programmtransformationen

Hier fehlt noch eine Beschreibung des Projekts.

 PUMA - Graduiertenkolleg Programm- Und Modell-Analyse

The doctorate program (Graduiertenkolleg) PUMA brings together the four fundamental approaches of program and model analysis, namely, type systems, theorem proving, model-checking, and abstract interpretation. Its goal is to develop new analysis techniques through cross-fertilization. The new methods should prototypically be implemented and be evaluated on selected analysis problems of software-intensive systems.

 CFSC - Computational Foundations of Social Choice

This collaborative research project will address some of the key issues in computational social choice, an interdisciplinary field of study at the interface of social choice theory and computer science. It aims at deepening our understanding of algorithmic and complexity-theoretic issues in social choice, at developing logic-based languages for modeling and reasoning about choice problems and preference structures, and at applying established techniques from AI, such as preference elicitation and learning, to problems of collective decision making.

 PAMAS - Preference Aggregation in Multiagent Systems

The PAMAS research group is devoted to studying distributed protocols that allow autonomous entities to aggregate their conflicting preferences. Well-known examples of conventional preference aggregation among humans are auctions and voting. Scientific fields that traditionally deal with preference aggregation, such as social choice theory, game theory, mechanism design, and implementation theory reside somewhere on the boundaries of economics, mathematics, and political science. During the last years, preference aggregation has experienced a dramatic increase of attention from computer scientists coming from various fields such as artificial intelligence, theory, or networking. Computer science extends existing research by introducing computational and communication efficiency, decentralized mechanism execution, correctness, privacy, or new applications like scheduling, file-sharing, or knowledge transfer. The lab is hosted by the chair for theoretical computer science at the University of Munich and is funded by the DFG (German Research Foundation) within the Emmy Noether Program.

 VeriNonReg - Verifikation nicht-regulärer Eigenschaften

The verification of non-regular program properties involves the investigation of program models which are structurally more complex than usually assumed in this context. Non-regularity is here to be understood in the sense of formal language theory, i.e. regarding the more expressive segments of the Chomsky hierarchy such as the context-free or context-sensitive languages. In order to capture these languages, a similarly increasing expressivity is needed on the specification side.
Several different logics capable of expressing context-free and context-sensitive properties have been proposed in the literature (follow the links to see a list of publications/ information):

• Fixed Point Logic with Chop (FLC)
• Higher Order Fixpoint Logic (HFL)
• Propositional Dynamic Logic of non-regular grammars (PDL[CFG], PDL[IG])
• Modal Iteration Calculus (MIC)

Example properties are unlimited counting, absence of buffer underflows (for unlimited buffer sizes) or bisimilarity to a balanced tree, just to name a few. The project aims at comparing these logics regarding expressivity and to develop model checking algorithms for them. As expressivity increases, the meaning of "model checking" is less restricted to "method used in program verification" but must be viewed as a general logic problem in which various important and general problems can be encoded. It is for example possible to solve universality of nondeterministic finite automata, satisfiability of modal logic K and evaluation of quantified boolean formulas as instances of the model checking problem for the first-order fragment of HFL (HFL1).
Taking a model checking algorithm as a template to analyze problem structures bears a high potential for optimizations, in particular, if we take into account that the formulas for these logics are typically fixed regardless of the input size.
Formulas of the above logics tend to be difficult to read. Simplifications of the logical syntax (maybe at the cost of lesser expressivity) are desirable with regard to the development of verification tools that can be used by engineers without a formal background. The goal here is to extract fragments of these logics for which intuitive specification languages can be provided.

Aim of this project is to develop an efficient parity game solver.

MLSolver - A Solver for Modal Fixpoint Logics

Aim of this project is to develop a satisfiability and validity solver for various modal fixpoint logics like the modal and linear-time mu-calculus, CTL*, PDL, etc. It is based on PGSolver.

Abgeschlossene Projekte