Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Forschung / Abgeschlossene Projekte


Inhaltsbereich

Abgeschlossene Projekte


 PolyNI - Verification of polymorphic noninterference for mobile code

Laufzeit: 2010 - 2013
Finanzierung: DFG Sachbeihilfe

This project focusses on technologies to verify information flow security properties that partly depend on the execution environment. Motivated by mobile application scenarios, we plan to develop specification notations for parametric noninterference policies, and to define type systems and program logics to statically certify these policies for Java and bytecode programs.


MLSolver - A Solver for Modal Fixpoint Logics

Laufzeit: ab 2009
Offizielle Website:  http://www.tcs.ifi.lmu.de/mlsolver

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.

 

PGSolver - A Parity Game Solver

Laufzeit: ab 2008
Offizielle Website:  http://www.tcs.ifi.lmu.de/pgsolver

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

 

CFSC - Computational Foundations of Social Choice

Laufzeit: 2008 - 2011
Finanzierung: ESF collaborative research project
Offizielle Website:  http://www.tcs.ifi.lmu.de/~brandtf/cfsc.html

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

Laufzeit: 2005 - 2010
Finanzierung: Nachwuchsgruppe im Emmy-Noether-Programm (Aktionsplan Informatik) der DFG
Offizielle Website:  http://www.tcs.ifi.lmu.de/~pamas/

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

Laufzeit: 2005 - 2009
Finanzierung: DFG Sachbeihilfe
Offizielle Website:  http://www.tcs.ifi.lmu.de/~axelsson/veri_non_reg/vnr.html

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.


Mobius - Mobility, Ubiquity and Security

Laufzeit:  2005 - 2009
Finanzierung: Integriertes Projekt im Rahmen der FET Global Computing Proactive Initiative der Europäischen Kommission
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://mobius.inria.fr/twiki/bin/view/Mobius

Mobius is a European Integrated Project developing novel technologies for trustworthy global computing, using proof-carrying code to give users independent guarantees of the safety and security of Java applications for their mobile phones and PDAs.
Global computing means that applications today may run anywhere, with data and code moving freely between servers, PCs and other devices: this kind of mobility over the ubiquitous internet magnifies the challenge of making sure that such software runs safely and reliably. In this context, the Mobius project focuses on securing applications downloaded to the Java MIDP platform: globally deployed across a host of phones, this is the common runtime environment for a myriad mobile applications.
Techniques of static analysis make it possible to check program behaviour by analysing source code before it ever executes. But mobile code means that this assurance must somehow travel with the application to reach the user. Conventional digital signatures use cryptography to identify who supplied a program; the breakthrough of proof-carrying code is to give mathematical proofs that guarantee the security of the code itself. We can strengthen digital signatures with digital evidence.
Key features of the Mobius security architecture are:

  • Innovative trust management, with digital evidence of program behaviour that can be independently checked by users or any third party.
  • Static enforcement, checking code before it starts; adaptable to manage a range of user security concerns, and configurable to match the real-world mix of mobile platforms.
  • Modularity, allowing developers to build up trusted applications from trusted components.

 

EmBounded - Resource Bounds for Embedded Systems

Laufzeit:  2005 - 2009
Finanzierung: Funded under Framework VI of the EU, as research project IST-510255 (FET-OPEN programme)
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www.embounded.org

The aims of the EmBounded Project are to identify, to quantify and to certify resource-bounded code in Hume, a domain-specific high-level programming language for real-time embedded systems.
Using formal models of resource consumption as a basis, the project will develop static analyses for time and space consumption and assess these against realistic applications for embedded systems. The work is novel in combining analyses of both source and machine code into a single framework.

 

InfoZert - Verification and Certification of Information Flows

Laufzeit:  2007 - 2008
Finanzierung: DFG-Sachbeihilfe
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www.pst.ifi.lmu.de/Research/previous-projects/infozert

The goal of this project is the development of technology enabling the specification of information flow policies in a state-oriented manner as well as the verification of policy conformance of system implementations.
It also aims to allow for generating certificates for policy-compliant system components with little personal effort on the code producer side, which can then producer-independently and automatically be checked by any code consumer prior to code execution.

 

Pro.Platz - Programmiersprachliche Aspekte sublinearer Platzkomplexitätsklassen

Laufzeit:  2005 - 2009
Finanzierung: DFG Sachbeihilfe
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www2.tcs.informatik.uni-muenchen.de/forschung/ProPlatz

In diesem Projekt sollen Komplexitätsklassen, die durch geringen Speicherplatzbedarf gekennzeichnet sind, maschinenunabhängig und ressourcenfrei durch Verwendung von logischen und programmiersprachlichen Konzepten charakterisiert werden.
 Neben theoretischen Einsichten über die Natur dieser Klassen ist dies bei der Entwicklung automatischer Analysen zur Abschätzung von Laufzeit und Platzverbrauch von Programmen nützlich. Eine andere Anwendung ist die Entwicklung spezifischer Optimierungen, die sich aus der komplexitätstheoretischen Analyse ergeben.
 Für polynomielle Rechenzeit (P) und höhere Klassen sind solche Charakterisierungen seit längerer Zeit bekannt; für kleinere Klassen, die durch logarithmischen Speicherplatzbedarf definiert sind, existieren dagegen keine oder nur rudimentäre Ansätze.
 Im Zusammenhang mit den erwähnten Anwendungen sind gerade diese aber von besonderem Interesse bei stark ressourcenbeschränkten Szenarien, wie Peer-to-peer Computing, eingebetteten Systemen, mobilem Code. Obwohl im Projekt die theoretische Grundlagenarbeit im Vordergrund steht, werden solche Anwendungen exemplarisch untersucht.

 

APPSEM II - Applied Semantics II

Laufzeit:  2003 - 2008
Finanzierung: Projekt im IST-Programm des EU 5th Framework Programme
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www.tcs.informatik.uni-muenchen.de/~mhofmann/appsem2

APPSEM is a thematic network funded by the IST programme of the European Union.
 Its objective is to promote research into application-oriented semantics of programming languages.
 APPSEM does this by organising and sponsoring workshops, summer schools, and individual visits.
 APPSEM does not fund researchers or PhD students.
 The APPSEM research programme is structured into nine themes.
 More details can be found in the  Technical Annex and the Annual Report.

 

SIGNAL

Laufzeit:  2002 - 2006
Finanzierung: Projekt des Bayerischen Kultusministeriums zur Nachqualifikation von Gymnasiallehrern bis 2005
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www2.tcs.informatik.uni-muenchen.de/lehre/lehrerausbildung

Die Neueinführung des Pflichtfaches Informatik an den bayerischen Gymnasien erfordert die Nachqualifizierung von ca. 400 Lehrkräften bis zum Jahr 2007. Auf Initiative des Bayerischen Staatsministeriums für Unterricht und Kultus wurde im September 2001 mit Pilotkursen begonnen, Lehrerinnen und Lehrer auf das Staatsexamen Informatik vorzubereiten.
 Im September 2002 startete das bayernweite Projekt SIGNAL (Sofortprogramm Informatik am Gymnasium - Nachqualifikation von Lehrkräften), welches bis zum Sommer 2006 Lehrkräfte in Form von jeweils zweijährigen Kursen in Informatik nachqualifiziert.
 Die Zielsetzung dieser Nachqualifizierungskurse ist in erster Linie ein fundiertes Fachwissen in Informatik mit dem Abschluss 1. Staatsexamen. Weiterhin wird auf didaktische Aspekte des ab Schuljahr 04/05 am Gymnasium neuen Faches Informatik eingegangen.

 

MRG - Mobile Resource Guarantees

Laufzeit:  2002 - 2006
Finanzierung: Projekt im IST Programm des EU 5th Framework Programme
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://groups.inf.ed.ac.uk/mrg/

The Mobile Resource Guarantees (MRG) project has developed the infrastructure needed to endow mobile code with independently verifiable certificates describing its resource behaviour (space, time, etc.).
An article on MRG, explaining the results in general terms, has appeared in the IST Results website, and in EVCA Barometer.

 

Komplexität monotoner Schaltkreise und aussagenlogischer Beweissysteme

Laufzeit:  2001 - 2006
Finanzierung: Nachwuchsgruppe im Emmy-Noether-Programm der DFG
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www.tcs.informatik.uni-muenchen.de/~jjohanns/projekt.html

Es sollen Probleme aus der Komplexitätstheorie monotoner Schaltkreise und ihre Anwendung auf Probleme aus der Theorie der Komplexität aussagenlogischer Beweissysteme untersucht werden. Insbesondere sollen untere Schranken an die Tiefe und Größe boolescher Schaltkreise verbessert und auf weitere Klassen monotoner Schaltkreise (boolesche Schaltkreise mit unbeschränktem Eingangsgrad, monotone reelle Schaltkreise) verallgemeinert werden. Als Anwendung folgen neue und verbesserte untere Schranken für aussagenlogische Beweissysteme, etwa Varianten des Cutting-Planes Systems, mittels der Methode der effektiven monotonen Interpolation. Weiterhin soll untersucht werden, inwieweit diese Interpolationsmethode auf verschiedene, in der Literatur vorgeschlagene und neue, Erweiterungen von Cutting-Planes-Beweissystemen verallgemeinert werden kann.
 Außerdem soll die relative Komplexität von eingeschränkten Formen des Resolutionskalküls untersucht werden. Dabei sollen insbesondere solche Einschränkungen betrachtet werden, die in Anwendungen, etwa in automatischen Theorembeweisern oder in Erfüllbarkeitsalgorithmen, verwendet werden, beispielsweise negative/positive Resolution, reguläre und Davis-Putnam-Resolution oder lineare Resolution.

 

Type Systems for Resource-Bounded Computation

Laufzeit:  2000 - 2002
Finanzierung: EPSRC Projekt                                             
Teilprojekte:  
Projektpartner: -
Offizielle Website:  http://www.dcs.ed.ac.uk/home/resbnd/

This project draws on ideas of Martin Hofmann, see his papers on the subject area.

 

 

 Laufende Projekte

 

 

 

 

Artikelaktionen


Funktionsleiste