Projekt

Lax Logic in Formal System Design

Project Objectives:

to develop a general theory of abstraction and refinement at multiple abstraction levels and to specialise it to provide a logical and coherent account of how to handle behavioural constraints during formal hardware and software synthesis.
to improve the technology of formal system design by building a system centred on a generic mechanism for constraint-handling, together with concrete constraint packages for timing, data and structure.
to demonstrate the adequacy of the theory and the usefulness of the implementation by means of a substantial case study of formal synthesis.

Projektleitung:
Dr. Matt Fairtlough

Beteiligte:
Prof. Michael Mendler, Ph.D., Dr. Xiaochun Cheng, The University of Reading, UK

Stichwörter:
System Design and Formal Verification, Abstraction and Refinement, Intuitionistic Modal Logic

Laufzeit: 1.7.1998 - 5.2.2002

Förderer:
British EPSRC

Publikationen

Fairtlough, M. ; Mendler, Michael ; Cheng, X.: Abstraction and refinement in higher-order logic . In: Boulton, R. J. ; Jackson, P. B. (Hrsg.) : International Conference on Theorem Proving in Higher-order Logic (TPHOLs`2001 Edinburgh September 2001). 2001, S. 201-216. (LNCS Bd. 2152)

Fairtlough, M. ; Mendler, Michael ; Moggi, E. (Hrsg.): Modalities in Type Theory . Cambridge : Cambridge University Press, 2001 (Special Issue of Mathematical Structures in Computer Science Bd. 11, Nr. 4) . - 90 Seiten.

Cheng, X. ; Fairtlough, M. ; Mendler, Michael: Proofs as constraints for abstraction and refinement. . In: Egly, U. ; Fiedler, A. ; Horacek, H. ; Schmitt, S. (Hrsg.) : Workshop on Proof Transformations, Proof Presentations and Complexities of Proof (PTP '01 Siena, Universitá degli Studi di Siena, Dipartimento di Ingegneria dell'Informatione June 2001). 2001, S. 1-11.

Gore, R. ; Mendler, Michael ; De Paiva, V. (Hrsg.): Intuitionistic Modal Logic and Applications . (IMLA'02 Copenhagen, DK July 2002) 2002. - 100 Seiten.

Fairtlough, M. ; Mendler, Michael: On the logical content of computational type theory: A solution to Curry`s problem . In: Callaghan, P. ; Luo, Z. ; McKinna, J. ; Pollack, R. (Hrsg.) : Types for Proofs and Programs. Berlin u.a. : Springer, 2002, (LNCS Bd. 2277), S. 63-78.

Fairtlough, M. ; Mendler, Michael: Intensional completeness in an extension of Goedel-Dummett logic . In: Studia Logica 73 (2003), S. 51-80

De Paiva, V. ; Gore, R. ; Mendler, Michael (Hrsg.): Modalities in Constructive Modal Logics and Type Theories . Oxford : Oxford University Press, 2004 (Special Issue of Journal of Logic and Computation Bd. to appear)

Mendler, Michael: Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification . In: Jones, G. ; Sheeran, M. (Hrsg.) : Workshop on Designing Correct Circuits. Berlin u.a. : Springer, 1991, S. 1-28.

Mendler, Michael: A modal logic for handling behavioural constraints in formal hardware verification . Edinburgh : Dept. of Computer Science, University of Edinburgh. 1993 (ECS-LFCS-93-255, March). - Forschungsbericht. 236 Seiten

Mendler, Michael: Dealing with Hardware Constraints - A modal logical approach . In: Kloos, C., D. (Hrsg.) : 1st Euroform Workshop (1st Euroform Workshop Las Navas del Marques, Spain January 1994). 1994, S. 7 Seiten.

Fairtlough, M. ; Mendler, Michael: An intuitionistic modal logic with applications to the formal verification of hardware . In: Pacholski, L. ; Tiuryn, J. (Hrsg.) : Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic. Berlin u. a. : Springer, 1995, S. 354-368. (LNCS Bd. 933)

Fairtlough, M. ; Mendler, Michael ; Walton, M.: First-order Lax Logic as a Framework for Constraint Logic Programming . Passau : Universität Passau. 1997 (MIP-9714). - Forschungsbericht. 51 Seiten