Current Projects

PyJIT

PyPy ist ein Open-Source-Projekt welches einen sehr flexible Python-Interpreter in Python selbst implementiert. Mit nur wenigen Zeilen Code ist es in PyPy möglich, zum Beispiel modernste Sicherheitsmechanismen oder alternative Nebenläufigkeitsmodelle einzubauen. Um PyPy ausgiebiger in der Praxis zu verwerten, wollen wir die Flexibilität von PyPy mit einer guten Performanz verbinden. Innerhalb des PYJIT Projektes werden wir deshalb ein "Just-In-Time"-Compiler-Toolkit entwickeln. Wir hoffen damit nicht nur flexibler sondern auch schneller als die Referenz-Implementierungvon Python zu werden. Das Projekt erschliesst uns damit eine grosse Reihe von neuen Anwendungen,zum Beispiel die Portierung von Python auf neue spezialisierte Hardware (eingebettete Systeme).Wir werden diese Techniken auch auf andere Programmiersprachen anwenden. Partner: merlinux (Deutschland), OpenEnd (Schweden), HHU

---

GEPAVAS

A DFG-funded project on directed and parallel model checking of high-level specifications. To start in 2008.

Referenzen:

• Gepavas Project Website

---

DEPLOY

An EU-funded Framework 7 IP; has started in February 2008.

Referenzen:

• Deploy Website

---

ProCSB

Extension of ProB to be able to animate CSP-M specifications in FDR syntax and link them with B machines. Funded by AWE.

---

Finished Projects

ASAP
The overall aim of this project is to develop techniques which enable the development of sophisticated and reliable software systems that are easy to maintain, and can be deployed on new generation, pervasive computing platforms.

Referenzen:

• ASAP - Publikationen
• ASAP - Website
• ASAP - Tools
• ASAP - Tools (Mirror)

PyPy
PyPy is a reimplementation of Python written in Python itself, flexible and easy to experiment with. Our long-term goals are to target a large variety of platforms, small and large, by providing a compiler toolsuite that can produce custom Python versions. Platform, Memory and Threading models are to become aspects of the translation process - as opposed to encoding low level details into a language implementation itself. Eventually, dynamic optimization techniques - implemented as another translation aspect - should become robust against language changes. The EU-funded period of the project is finished, but development continues and we have requested funding for a follow-up project.

Referenzen:

• PyPy - Website

Rodin
Our overall objective is the creation of a methodology and supporting open tool platform for the cost effective rigorous development of dependable complex software systems and services.

Referenzen:

• Rodin - Website

TSAS
The Trusted Software Agents and Services (TSAS) project is investigating and demonstrating the Trust issues that arise from accessing software services and utilising agent technology in PervasiveComputing environments. The project is developing software/hardware demonstrators with which to explore and highlight trust matters in the context of applications such as home finance or tele-medicine. The project is also examining the appropriate validation techniques that can help to achieve assurance of trustworthiness in such technologies.

Referenzen:

• TSAS - Website

ABCD
Automated Validation of Business Critical Systems with Component Based DesignsThe objective of this project is:

• to increase the uptake of formal modelling in the business critical systems industry.
We plan to achieve this by:
• lowering the cost of entry and
• increasing the benefits of using formal modelling.
We will be able to:
• lower the cost by building a repository of generic models of systems and components;
• increase the benefits by making verification and validation of critical systems available to real system architects;
• lower the cost and increase the benefits by providing automated tool support.

The focus is on support of system definition and architectural design so that the systems integrator can more easily model systems and validate proposed system architectures.

Referenzen:

• ABCD - Website

iMoc
The main objective of the project is to study the potential of automatically deriving abstractions for infinite model checking through a combination of existing technology for the automatic control of partial evaluation and abstract interpretation. First successful experiments of this idea have been conducted using the ECCE and LOGEN tools. The project consists of a theoretical study coupled with the implementation of a combined partial evaluation and abstract interpretation system (based upon ECCE). The practicality of the approach will be gauged on realistic examples, some of them coming from the EPSRC funded ABCD project for the validation of business-critical systems.

Referenzen:

• iMoc - Website

IOPS
Improving Offline Program Specialization
This is a DAAD funded project in collaboration with the group of Germán Vidal from the University of Valencia. Scheduled to run from January 2007 to December 2008.

Referenzen:

JASP
Demonstrably correct compilation of Java Byte Code. Three month industrially sponsored project.

Referenzen:

Impressum