Click on a theme or a project in the table below for more information.
Project leader:
Prof.dr. Herman Geuvers (RUN)
Consortium:
RUN
Total FTE: 2.4 (heads: 3 faculty: assoc. prof.: 1, PD: 2)
Key BRICKS publications:
| • |
H. Geuvers, M. Niqui, B. Spitters, F. Wiedijk - Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science, vol. 17 (1), pp. 3-36, 2007
|
| • |
P. Corbineau and C. Kaliszyk -- Cooperative Repositories for Formal Proofs -- A Wiki-Based Solution, in Towards Mechanized Mathematical Assistants, LNCS 4573, 2007, pp 221-234
|
|
Project AFM4: Advancing the Real Use of Proof Assistants
Proof Assistants are computer tools that help the user in
developing a theory, modeling systems and verifying properties
about these systems (giving proofs). So, Proof Assistants are very
generic tools to support Formal Methods. Their genericness makes
them less efficient than tools that are especially geared towards a
specific formal method. On the other hand they have a very precise
semantics, which makes the certainty of a result that is verified
by a Proof Assistant (PA) very high. In this project we want to
advance the use of PAs in several ways: (1) by developing a
mathematical input mode for PAs, making them more easy to use, (2)
developing a certified library for real number computation in Coq,
(3) verifying hybrid systems in Coq, using the library of (2) to
model and verify system properties.
Mathematical documents and proof language
We develop a more system independent declarative input mode for the
PA Coq, which will relax the learning curve and make the PA more
interesting and easy to use for average (mathematical) users. We
also develop tools for integrating formal proofs and mathematical
documents and we study the fine structure of proofs.
Certified library for real numbers
We have further developed our repository of constructive real
numbers C-CoRN. We plan to cooperate with researchers from INRIA to
apply our repository to large mathematical formalizations.
Verifying hybrid systems
This project has only just started. We cooperate with researchers
from the ITA group in Nijmegen to model hybrid systems and verify
their properties using predicate abstraction.
International cooperation
In the context of BRICKS we actively collaborate with a wide
variety of internationally well-renowned research institutes,
including for example INRIA Sophia Antipolis, INRIA-Microsoft
Research laboratory, University Paris XI, INTEL Research Labs
Portland, Chalmers University Gothenburg, University of Bologna,
Italy.
Highlights 2005-2006
As this project is part of the second phase of the BRICKS program
(financed through the first open round July 2005), the project is
currently in full swing and not all research positions have been
fulfilled. Likewise, the number of BRICKS key publications is
limited.
Research highlights
- The project leader Herman Geuvers has become a full professor at Radboud University Nijmegen on August 1 2006.
- We have developed a first version of the declarative input mode for Coq, which can be downloaded.
- We have developed a TexMacs plugin for Coq, enabling an integration of mathematical documents and a repository of formalized proofs.
Research challenges
- Optimal delay-based scheduling in communication networks.
- Identification of the SLA negotiation space for realizing end-to-end QoS for Web-based services in multi-provider environments.
- Exact asymptotics for Discriminatory Process Sharing models.
- Identification of a pricing structure to provide incentives to enforce a suitable prioritization.
Future work 2007-2009
We plan to focus our research on the formalization of hybrid
systems and the further development of our formal library and our
interfaces. To this end we will hire a scientific programmer in the
coming year, which is the one vacancy left on the project. The
formalization of Hybrid systems will require a close collaboration
with researchers from the ITA group in Nijmegen and possibly with
research groups at the TU Eindhoven. For the development of our
library we will be in close collaboration with researchers from
INRIA.
AFM4 Researchers funded by BRICKS
- Herman Geuvers (RUN)
- Pierre Corbineau (RUN)
- Henk Barendregt (RUN)
- Frits Vaandrager (RUN)
- Freek Wiedijk (RUN)
- Bas Spitters (RUN)
- Milad Niqui (RUN)
- Tonny Hurkens (RUN)
- Iris Loeb (RUN)
- Lionel Mamane (RUN)
- Russell O'Connor (RUN)
- Cezary Kaliszyk (RUN)
- Dan Synek (RUN)
- O. Tveretina (RUN)
For more information, please refer to the publications and posters of this project.
|
