Forschungsgebiete
Forschungsgebiet Formal Methods
Publikationen:| Year | Title | Author | Journal/Proceedings | Publisher | |
|---|---|---|---|---|---|
| 2012 | Pattern- and Component-based Development of Dependable Systems | Hatebur, D. | School: University of Duisburg-Essen | Deutscher Wissenschafts-Verlag (DWV) Baden-Baden | |
BibTeX:
@phdthesis{Hatebur2012,
year = {2012},
title = {Pattern- and Component-based Development of Dependable Systems},
author = {Hatebur, Denis},
publisher = {Deutscher Wissenschafts-Verlag (DWV) Baden-Baden},
school = {University of Duisburg-Essen},
url = {http://www.dwverlag.de/index.php?art=Pattern-+and+Component-based+Development+of+Dependable+Systems&mod=Onlineshop&view=Artikel&abid=166}
}
|
|||||
| 2011 | 11th School on Formal Methods (SFM) [BibTeX] |
Jürjens, J., Ochoa, M., Schmidt, H., Marchal, L., Houmb, S. H. & Shareeful, I. | Springer | ||
BibTeX:
@inbook{sfm2011,
year = {2011},
title = {11th School on Formal Methods ({SFM})},
author = {J{\"{u}}rjens, Jan and Ochoa, Mart{\'{\i}}n and Schmidt, Holger and Marchal, Lo{\"{\i}}c and Houmb, Siv Hilde and Shareeful, Islam},
publisher = {Springer},
series = {LNCS 6659},
pages = {504--526},
url = {https://link.springer.com/}
}
|
|||||
| 2008 | A Formal Metamodel for Problem Frames | Hatebur, D., Heisel, M. & Schmidt, H. | Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS) | ||
| Abstract: Problem frames are patterns for analyzing, structuring, and characterizing software development problems. This paper presents a formal metamodel for problem frames expressed in UML class diagrams and using the formal specification notation OCL. That metamodel clarifies the nature of the different syntactical elements of problem frames, as well as the relations between them. It provides a framework for syntactical analysis and semantic validation of newly defined problem frames, and it prepares the ground for tool support for the problem frame approach. |
|||||
BibTeX:
@techreport{HHS2008,
year = {2008},
title = {A Formal Metamodel for Problem Frames},
booktitle = {Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS)},
author = {Hatebur, Denis and Heisel, Maritta and Schmidt, Holger},
series = {LNCS 5301},
pages = {68--82},
url = {https://link.springer.com/}
}
|
|||||
| 2007 | Enhancing Dependability of Component-Based Systems | Lanoix, A., Hatebur, D., Heisel, M. & Souquières, J. | Reliable Software Technologies -- Ada Europe 2007 | Springer | |
| Abstract: We present an approach for enhancing dependability of component- based software. Functionality related to security, safety and reliability is encapsulated in specific components, allowing the method to be applied to off-the-shelf components. Any set of components can be extended with dependability features by wrapping them with special components, which monitor and filter input and outputs. This approach is supported by a rigorous development methodology based on UML and the B method and is introduced on the level of software architecture. |
|||||
BibTeX:
@inproceedings{LHH+2007,
year = {2007},
title = {Enhancing Dependability of Component-Based Systems},
booktitle = {Reliable Software Technologies -- Ada Europe 2007},
author = {Lanoix, Arnaud and Hatebur, Denis and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
publisher = {Springer},
series = {LNCS 4498},
pages = {41--54},
url = {https://link.springer.com/}
}
|
|||||
| 2006 | Proving Component Interoperability with B Refinement [BibTeX] |
Chouali, S., Heisel, M. & Souquières, J. | Electronic Notes in Theoretical Computer Science | ||
BibTeX:
@article{CHS2006,
year = {2006},
title = {Proving Component Interoperability with B Refinement},
author = {Chouali, Samir and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {160},
pages = {157--172}
}
|
|||||
| 2005 | Proving Component Interoperability with B Refinement | Chouali, S., Heisel, M. & Souquières, J. | International Workshop on Formal Aspects on Component Software | ||
| Abstract: We use the formal method B for specifying interfaces of software components. Each component interface is equipped with a suitable data model defining all types occurring in the signature of interface operations. Moreover, pre- and postconditions have to be given for all interface operations. The interoperability between two components is proved by using a refinement relation between an adaption of the interface specifications. | |||||
BibTeX:
@inproceedings{ChoualiHeiselSouquieres05,
year = {2005},
title = {Proving Component Interoperability with {B} Refinement},
booktitle = {{International Workshop on Formal Aspects on Component Software}},
author = {Chouali, Samir and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
publisher = {CSREA Press},
pages = {915-920}
}
|
|||||
| 2003 | Use of Patterns in Formal Development: Systematic Transition From Problems to Architectural Designs | Choppy, C. & Heisel, M. | Recent Trends in Algebraic Development Techniques, 16th WADT, Selected Papers | Springer | |
| Abstract: We present a pattern-based software lifecycle and a method that supports the systematic execution of that lifecycle. First, problem frames are used to develop a formal specification of the problem to be solved. In a second phase, architectural styles are used to construct an architectural specification of the software system to be developed. That specification forms the basis for fine-grained design and implementation. | |||||
BibTeX:
@inproceedings{CH2003,
year = {2003},
title = {Use of Patterns in Formal Development: Systematic Transition From Problems to Architectural Designs},
booktitle = {Recent Trends in Algebraic Development Techniques, 16th WADT, Selected Papers},
author = {Choppy, Christine and Heisel, Maritta},
publisher = {Springer},
series = {LNCS 2755},
pages = {205--220},
url = {https://link.springer.com/}
}
|
|||||
| 2003 | Formalisation des besoins à l`aide de schémas LSCs | Souquières, J. & Heisel, M. | Proceedings Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'2003 | ||
| Abstract: Dans notre approche pour l'expression des besoins, nous proposons d'intégrer une étape de formalisation très tôt dans le développement an d'analyser de manière détaillée les besoins des utilisateurs et de découvrir les inconsistances et les problèmes à partir des difcultés rencontrées lors de la formalisation. An d'améliorer la lisibilité et l'écriture des besoins formalis és, nous proposons d'utiliser les LSCs, Life Sequence Charts, au lieu des formules pour la formalisation des besoins décomposés sous forme de fragments. Nous proposons, en particulier, des schémas graphiques pour exprimer différents types de besoins. Ces schémas constituent un guide à la formalisation. |
|||||
BibTeX:
@inproceedings{SH2003,
year = {2003},
title = {Formalisation des besoins {\`{a}} l`aide de sch{\'{e}}mas {LSCs}},
booktitle = {Proceedings Approches Formelles dans l'Assistance au D{\'{e}}veloppement de Logiciels - AFADL'2003},
author = {Souqui{\`{e}}res, Jeanine and Heisel, Maritta},
pages = {53--63},
note = {ISBN 2-7261-1236-6}
}
|
|||||
| 2002 | Logische Modellierung von Anwendungswelten aus Benutzersicht | Heisel, M. & Krömker, H. | Workshop Proceedings "Multimediale Informations- und Kommunikationssysteme, NET.OBJECT Days 2002" | ||
| Abstract: Der Softwareentwicklung fehlt oft eine detaillierte methodische Unterstützung von technischen Softwareentwicklungsaktivitäten. Eine Autorin dieses Papiers hat das Konzept der Agenda entwickelt, das zum Ziel hat, Softwareentwicklungswissen als "methodische Essenzen" von Softwareentwicklungsaktivitäten explizit zu repräsentieren. Zur logischen Modellierung von Anwendungswelten aus Benutzersicht wird eine Agenda entwickelt, die es erlaubt diese Anwendungswelt methodisch in Konzepten der Handlungspsychologie zu erheben. | |||||
BibTeX:
@inproceedings{Heisel2002,
year = {2002},
title = {Logische Modellierung von Anwendungswelten aus Benutzersicht},
booktitle = {Workshop Proceedings "Multimediale Informations- und Kommunikationssysteme, NET.OBJECT Days 2002"},
author = {Heisel, Maritta and Kr{\"{o}}mker, Heidi},
publisher = {tranSIT GmbH, Ilmenau},
pages = {649--656},
note = {ISBN 3-9808628-1-X}
}
|
|||||
| 2002 | Toward a formal model of software components | Heisel, M., Santen, T. & Souquières, J. | Proc. 4th International Conference on Formal Engineering Methods | Springer | |
| Abstract: We are interested in specifying component models in a way that allows us to analyze the interplay of components in general, and to concisely specify individual components. As a starting point for coming up with a technique of specifying component models, we consider JavaBeans. We capture the JavaBean component model using UML class diagrams, Object-Z, and life sequence charts. |
|||||
BibTeX:
@inproceedings{HSS2002,
year = {2002},
title = {Toward a formal model of software components},
booktitle = {Proc.\ 4th International Conference on Formal Engineering Methods},
author = {Heisel, Maritta and Santen, Thomas and Souqui{\`{e}}res, Jeanine},
publisher = {Springer},
series = {LNCS 2495},
pages = {57--68},
url = {https://link.springer.com/}
}
|
|||||
| 2002 | Confidentiality-Preserving Refinement is Compositional -- Sometimes | Santen, T., Heisel, M. & Pfitzmann, A. | Proc. Computer Security -- ESORICS 2002 | Springer | |
| Abstract: Confidentiality-preserving refinement describes a relation between a specification and an implementation that ensures that all confidentiality properties required in the specification are preserved by the implementation in a probabilistic setting. The present paper investigates the condition under which that notion of refinement is compositional, i.e. the condition under which refining a subsystem of a larger system yields a confidentiality-preserving refinement of the larger system. It turns out that the refinement relation is not composition in general, but the condition for compositionality can be stated in a way that builds on the analysis of subsystems thus aiding system designers in analyzing a composition. |
|||||
BibTeX:
@inproceedings{SHP2002,
year = {2002},
title = {Confidentiality-Preserving Refinement is Compositional -- Sometimes},
booktitle = {Proc.\ Computer Security -- ESORICS 2002},
author = {Santen, Thomas and Heisel, Maritta and Pfitzmann, Andreas},
publisher = {Springer},
series = {LNCS 2502},
pages = {194--211},
url = {https://link.springer.com/}
}
|
|||||
| 2002 | Specification and Refinement of Secure IT Systems | Santen, T., Pfitzmann, A. & Heisel, M. | Proc. International Workshop on Refinement of Critical Systems | ||
BibTeX:
@inproceedings{SPH2002,
year = {2002},
title = {Specification and Refinement of Secure {IT} Systems},
booktitle = {Proc.\ International Workshop on Refinement of Critical Systems},
author = {Santen, Thomas and Pfitzmann, Andreas and Heisel, Maritta},
note = {http://www.esil.univ-mrs.fr/\verb|~|spc/rcs02/papers/Santen.ps.gz}
}
|
|||||
| 2001 | Specifying Safety-Critical Embedded systems with Statecharts and Z: An Agenda for Cyclic Software Components | Grieskamp, W., Heisel, M. & Dörr, H. | Science of Computer Programming | ||
| Abstract: The application of formal techniques can contribute much to the quality of software, which is of utmost importance for safety-critical embedded systems. These techniques, however, are not easy to apply. In particular, methodological guidance is often unsatisfactory. We address this problem by the concept of an agenda. An agenda is a list of activities to be performed for solving a task in software engineering. Agendas used to support the application of formal specification techniques provide detailed guidance for specifiers, templates of the used specification language that only need to be instantiated, and application independent validation criteria. We apply the agenda approach to a particular class of embedded safety-critical systems, the formal specification of which has been investigated in the case-studies of the German Espress project during the last two years. | |||||
BibTeX:
@article{Grieskamp2001,
year = {2001},
title = {Specifying Safety-Critical Embedded systems with {S}tatecharts and {Z}: An Agenda for Cyclic Software Components},
author = {Grieskamp, Wolfgang and Heisel, Maritta and D{\"{o}}rr, Heiko},
journal = {Science of Computer Programming},
volume = {40},
pages = {31--57}
}
|
|||||
| 2001 | Confidentiality-Preserving Refinement | Heisel, M., Pfitzmann, A. & Santen, T. | Proc. 14th IEEE Computer Security Foundations Workshop | ||
| Abstract: We develop a condition for confidentiality-preserving refinement which is both necessary and sufficient. Using a slight extension of CSP as notation, we give a toy example to illustrate the usefulness of our condition. Systems are specified by their behavior and a window. For an abstract system, the window specifies what information is allowed to be observed by its environment. For a concrete system, the window specifies what information cannot be hidden from its environment. A concrete system is a confidentiality-preserving refinement of an abstract system, if it behaviorally refines the abstract system and if the information revealed by the concrete window is allowed to be revealed according to the abstract window. |
|||||
BibTeX:
@inproceedings{HPS2001,
year = {2001},
title = {Confidentiality-Preserving Refinement},
booktitle = {Proc.\ 14th IEEE Computer Security Foundations Workshop},
author = {Heisel, Maritta and Pfitzmann, Andreas and Santen, Thomas},
publisher = {IEEE Computer Society},
pages = {295--305}
}
|
|||||
| 1999 | Modeling Safety-Critical Systems with Z and Petri Nets | Heiner, M. & Heisel, M. | Proceedings of the 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP) | Springer | |
| Abstract: We show how to combine the specification notation Z with Petri nets for modeling safety-critical systems. The combination preserves the strengths of the two formalisms, while ameliorating their drawbacks. We illustrate our approach by modeling a part of a production cell and validating that model with respect to safety-related properties. | |||||
BibTeX:
@inproceedings{Heiner1999,
year = {1999},
title = {Modeling Safety-Critical Systems with {Z} and {P}etri Nets},
booktitle = {Proceedings of the 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP)},
author = {Heiner, Monika and Heisel, Maritta},
publisher = {Springer},
series = {LNCS 1698},
pages = {361--374},
url = {http://www.springerlink.com/}
}
|
|||||
| 1999 | Combining Z and Petri Nets for Modeling Safety-Critical Systems | Heiner, M. & Heisel, M. | Sicherheit und Zuverlässigkeit software-basierter Systeme | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heiner1999a,
year = {1999},
title = {Combining {Z} and {P}etri Nets for Modeling Safety-Critical Systems},
booktitle = {Sicherheit und {Z}uverl{\"{a}}ssigkeit software-basierter {S}ysteme},
author = {Heiner, Monika and Heisel, Maritta},
publisher = {Institut f{\"{u}}r Sicherheitstechnologie},
series = {Bericht ISTec-A-367},
pages = {249--251},
note = {{ISBN} 3-00-004872-3}
}
|
|||||
| 1999 | A Method for Requirements Elicitation and Formal Specification | Heisel, M. & Souquières, J. | Proceedings 18th International Conference on Conceptual Modeling, ER'99 | Springer | |
| Abstract: We propose a method for the elicitation and the expression of requirements. The requirements are then transformed in a systematic way into a formal specification. The approach - which distinguishes between requirements and specifications - gives methodological support for requirements elicitation and specification development. It avoids introducing new notations but builds on known techniques. | |||||
BibTeX:
@inproceedings{Heisel1999,
year = {1999},
title = {A Method for Requirements Elicitation and Formal Specification},
booktitle = {Proceedings 18th International Conference on Conceptual Modeling, ER'99},
author = {Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
publisher = {Springer},
series = {LNCS 1728},
pages = {309--324},
url = {http://www.springerlink.com/}
}
|
|||||
| 1999 | De l'élicitation des besoins à la spécification formelle | Heisel, M. & Souquières, J. | Technique et science informatiques | ||
| Abstract: ABSTRACT. This paper proposes a method for the elicitation and the expression of requirements.It is based on a detailed analysis of requirements, leading to a better understanding of the problem to be solved. The approach – which clearly distinguishes between requirements and specifications – leads to the expression of a formal specification in a natural way. It does not introduce new languages but builds on known techniques. Agendas are used to describe the method | |||||
BibTeX:
@article{Heisel1999a,
year = {1999},
title = {De l'{\'{e}}licitation des besoins {\`{a}} la sp{\'{e}}cification formelle},
author = {Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
journal = {Technique et science informatiques},
volume = {18},
number = {7},
pages = {777--801}
}
|
|||||
| 1999 | Specifying the Safety Controllers of Traffic Light Systems in Z and Statecharts | Winter, K., Santen, T. & Heisel, M. | Sicherheit und Zuverlässigkeit software-basierter Systeme | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Winter1999,
year = {1999},
title = {Specifying the Safety Controllers of Traffic Light Systems in {Z} and {S}tatecharts},
booktitle = {Sicherheit und {Z}uverl{\"{a}}ssigkeit software-basierter {S}ysteme},
author = {Winter, Kirsten and Santen, Thomas and Heisel, Maritta},
publisher = {Institut f{\"{u}}r Sicherheitstechnologie},
series = {Bericht ISTec-A-367},
pages = {126--137},
note = {{ISBN} 3-00-004872-3}
}
|
|||||
| 1998 | Specifying safety-critical embedded systems with Statecharts and Z: An Agenda for Cyclic Software Components | Grieskamp, W., Heisel, M. & Dörr, H. | Proc. ETAPS-FASE'98 | Springer | |
| Abstract: The application of formal techniques can contribute much to the quality of software, which is of utmost importance for safety-critical embedded systems. These techniques, however, are not easy to apply. In particular, methodological guidance is often unsatisfactory. We address this problem by the concept of an agenda. An agenda is a list of activities to be performed for solving a task in software engineering. Agendas used to support the application of formal specification techniques provide detailed guidance for specifiers, templates of the used specification language that only need to be instantiated, and application independent validation criteria. We apply the agenda approach to a particular class of embedded safety-critical systems, the formal specification of which has been investigated in the case-studies of the German Espress project during the last two years. | |||||
BibTeX:
@inproceedings{Grieskamp1998,
year = {1998},
title = {Specifying safety-critical embedded systems with {S}tatecharts and {Z}: An Agenda for Cyclic Software Components},
booktitle = {Proc.\ {ETAPS-FASE'98}},
author = {Grieskamp, Wolfgang and Heisel, Maritta and D{\"{o}}rr, Heiko},
publisher = {Springer},
series = {LNCS 1382},
pages = {88--106},
url = {http://www.springerlink.com/}
}
|
|||||
| 1998 | Computer-Aided Formal Methods: A Generic Concept | Heisel, M. | Proc. Workshop Tools for System Development and Verification | ||
| Abstract: We present a formalism-independent approach to the design of support systems for the application of formal methods in software engineering. Its basis is a knowledge representation mechanism called strategy. Strategies represent development knowledge used to perform different software engineering activities. The development of an artefact is modeled as a problem solving process. The definition of strategies is generic in the definition of problems solutions and acceptability of a solution with respect to a problem. The notion of strategy is complemented by a generic system architecture that serves as a template for the implementation of support tools for strategy-based problem solving. Two different instantiations of the strategy framework and an implemented program synthesis system are presented. | |||||
BibTeX:
@inproceedings{Heisel1998,
year = {1998},
title = {Computer-Aided Formal Methods: A Generic Concept},
booktitle = {Proc.\ Workshop Tools for System Development and Verification},
author = {Heisel, Maritta},
publisher = {Shaker Verlag Aachen},
series = {BISS Monographs 1},
pages = {84--106}
}
|
|||||
| 1998 | Agendas -- A Concept to Guide Software Development Activites | Heisel, M. | Proc. Systems Implementation 2000 | ||
| Abstract: We present the concept of an agenda. This concept serves to represent process knowledge in the area of software development. An agenda consists of a list of steps to be performed when developing a software artifact. Each activity may have associated a schematic expression of the language in which the artifact is expressed and some validation conditions that help detect errors. We present example agendas and discuss the distinguishing features of the agenda concept in detail. Agendas provide methodological support to their users, make development knowledge explicit and thus comprehensible, and contribute to a standardization of software development activities and products. Agendas are flexible and useful in many different contexts and lay the basis for powerful machine support in software development. | |||||
BibTeX:
@inproceedings{Heisel1998a,
year = {1998},
title = {Agendas -- A Concept to Guide Software Development Activites},
booktitle = {Proc.\ Systems Implementation 2000},
author = {Heisel, Maritta},
publisher = {Chapman \& Hall London},
pages = {19--32}
}
|
|||||
| 1998 | Methodological Support for Requirements Elicitation and Formal Specification | Heisel, M. & Souquières, J. | Proc. 9th International Workshop on Software Specification and Design | IEEE Computer Society Press | |
| Abstract: We propose a method for the elicitation and the expression of requirements. The requirements can then be transformed in a systematic way into a formal specification that is a suitable basis for design and implementation of a software system. The approach – which distinguishes between requirements and specifications – gives methodological support for requirements elicitation and specification development. It does not introduce a new language but builds on known techniques. | |||||
BibTeX:
@inproceedings{Heisel1998g,
year = {1998},
title = {Methodological Support for Requirements Elicitation and Formal Specification},
booktitle = {Proc. 9th International Workshop on Software Specification and Design},
author = {Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
publisher = {IEEE Computer Society Press},
pages = {153--155},
url = {http://www.ieee.org/}
}
|
|||||
| 1998 | An Agenda for Event-Driven Software Components with Complex Data Models | Winter, K., Santen, T. & Heisel, M. | Proceedings of the 17th International Conference on Computer Safety, Reliability and Security (SAFECOMP) | Springer | |
| Abstract: We present a method to specify software for a special kind of safetycritical embedded systems, where sensors deliver low-level values that must be abstracted and pre-processed to express functional and safety requirements adequately. These systems are characterized by a reference architecture. The method is expressed as an agenda, which is a list of activities to be performed for setting up the software specification, complemented by validation conditions that help detect and correct errors. The specification language we use is a combination of the formal notation Z and the diagrammatic notation statecharts. Our approach not only provides detailed guidance to specifiers, but it is also part of a more general engineering concept for engineering safety-critical embedded systems that was developed in the ESPRESS project, a joint project of academia and industry. | |||||
BibTeX:
@inproceedings{Winter1998,
year = {1998},
title = {An Agenda for Event-Driven Software Components with Complex Data Models},
booktitle = {Proceedings of the 17th International Conference on Computer Safety, Reliability and Security (SAFECOMP)},
author = {Winter, Kirsten and Santen, Thomas and Heisel, Maritta},
publisher = {Springer},
series = {LNCS 1516},
pages = {16--31},
url = {http://www.springerlink.com/}
}
|
|||||
| 1997 | Methodology and Machine Support for the Application of Formal Techniques in Software Engineering | Heisel, M. | |||
| Abstract: Methodological support for the application of formal techniques in software engineering is the motto for this entire work We use the term formal techniques instead of the more common term formal methods because we nd the term formal method to be a misnomer A formal notation with a mathematically rigorous semantics is often called a formal method In comparison with notational and semantic issues methodological aspects are frequently neglected in the research on formal techniques In our opinion this fact is one of the greatest obstacles that hinders the transfer of formal techniques from academic environments into software engineering practice The word technique does not suggest that there exists a method for guiding the application of the formalism in question The aim of this work is to demonstrate how formal techniques can be protably employed in software engineering We do not treat the whole software engineering process and consider all known formal techniques but show areas where formal techniques can improve the quality of products or processes in software engineering For this purpose we describe some impor tant and typical situations and show what can be gained by applying formal techniques in these situations Examples are the development of safetycritical systems where formal spec ication techniques contribute to the overall system safety and software architectures where a formal characterization makes it possible to reuse previously acquired design knowledge in a semantically sound way Using formal techniques we can positively guarantee that the product of a development step of the software engineering process enjoys certain semantic properties In this respect formal techniques can lead to an improvement in software quality that cannot be achieved by traditional techniques alone However formal techniques are no panacea Even if a program is proven correct with respect to its specication this does not mean that it will perform to the satisfaction of its users The specication may not capture the requirements adequately the performance of the program may be unsatisfactory or the compiler or the operating system that are needed to execute the program may contain errors Hence informal methods as they are applied in traditional software engineering and especially informal validation techniques such as testing are still indispensable and we propose to complement traditional techniques by formal ones not to replace them | |||||
BibTeX:
@book{Heisel1997,
year = {1997},
title = {Methodology and Machine Support for the Application of Formal Techniques in Software Engineering},
author = {Heisel, Maritta},
publisher = {Habilitation Thesis}
}
|
|||||
| 1997 | Formalizing Communication Aspects of Design Patterns Using LOTOS | Heisel, M., Lévy, N., Losavio, F. & Matteo, A. | |||
| Abstract: In the research of design patterns, the main activities are the discovery or invention of new patterns, the application, and the specification or formal description of design patterns. This paper aims at formalizing the communication aspects of a subset of the design patterns defined by Gamma et al. [8]. The LOTOS specification language is used to formalize these communication aspects, where the objects are modeled as processes and the messages between objects are expressed by LOTOS communication patterns. Our formalization not only contributes to a semantic foundation of design patterns, but also supports validation and rapid prototyping. | |||||
BibTeX:
@techreport{Heisel1997a,
year = {1997},
title = {Formalizing Communication Aspects of Design Patterns Using {LOTOS}},
author = {Heisel, Maritta and L{\'{e}}vy, N. and Losavio, F. and Matteo, A.},
number = {97-R-202}
}
|
|||||
| 1997 | Methodological Support for Formally Specifying Safety-Critical Software | Heisel, M. & Sühl, C. | Proceedings 16th International Conference on Computer Safety, Reliability and Security (SAFECOMP) | Springer | |
| Abstract: We present the concept of an agenda and apply this concept to the formal specification of software for safety-critical applications. An agenda describes a list of activities to solving a task in software engineering, and validations of the results of the activities. Agendas used to support the application of formal specification techniques provide detailed guidance for specifiers, schematic expressions of the used specification language that only need to be instantiated, and application independent validation criteria. We present an agenda for a frequently used design of safety-critical systems and illustrate its usage by an example. Using agendas to systematically develop formal specifications for safety-critical software contributes to system safety because, first, the specifications are developed in a standardized way, making them better comprehensible for other persons. Secondly, using a formal language yields specifications with an unambiguous semantics as the starting point of further design and implementation. Thirdly, the recommended validation criteria draw the specifier’s attention to common mistakes and thus enhance the quality of the resulting specification. |
|||||
BibTeX:
@inproceedings{Heisel1997c,
year = {1997},
title = {Methodological Support for Formally Specifying Safety-Critical Software},
booktitle = {Proceedings 16th International Conference on Computer Safety, Reliability and Security (SAFECOMP)},
author = {Heisel, Maritta and S{\"{u}}hl, Carsten},
publisher = {Springer},
pages = {295--308},
url = {https://link.springer.com/}
}
|
|||||
| 1996 | A Pragmatic Approach to Formal Specification | Heisel, M. | Object-Oriented Behavioral Specifications | ||
| Abstract: I propose to overcome some difficulties arising in the practical usage of formal specification techniques by adopting a pragmatic attitude. I argue that the transition from informal requirements to a formal specification should not be made too early; that it is not necessary to formally specify every detail; that different formalisms should be combined where appropriate; and that sometimes it may be useful not to adhere to limitations imposed by the formal specification language. | |||||
BibTeX:
@incollection{Heisel1996,
year = {1996},
title = {A Pragmatic Approach to Formal Specification},
booktitle = {Object-Oriented Behavioral Specifications},
author = {Heisel, Maritta},
publisher = {Kluwer Academic Publishers},
pages = {41--62}
}
|
|||||
| 1996 | An Approach to Develop Provably Safe Software | Heisel, M. | High Integrity Systems | ||
| Abstract: We present a process model for the development of provably safe software. It is based on well-established tools and techniques to set up formal specifications in the specification language Z and a program synthesis system designed by the author. The model provides a guideline for the specification and implementation of safe software consisting of a number of steps that are complemented by proof obligations. The parts of the process specific to software safety are given special consideration. The approach is exemplified by the specification and partial implementation of a program controlling the pump of a steam boiler. Finally we relate software safety to correctness and reliability. | |||||
BibTeX:
@article{Heisel1996a,
year = {1996},
title = {An Approach to Develop Provably Safe Software},
author = {Heisel, Maritta},
journal = {High Integrity Systems},
volume = {1},
number = {6},
pages = {501--512}
}
|
|||||
| 1996 | Formal Specification of Safety-Critical Software with Z and Real-Time CSP | Heisel, M. & Sühl, C. | Proceedings 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP) | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1996b,
year = {1996},
title = {Formal Specification of Safety-Critical Software with {Z }and Real-Time {CSP}},
booktitle = {Proceedings 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP)},
author = {Heisel, Maritta and S{\"{u}}hl, Carsten},
publisher = {Springer London},
pages = {31--45}
}
|
|||||
| 1996 | Strategies -- A Generic Knowledge Representation Mechanism for Software Development Activities | Heisel, M. | |||
| Abstract: This paper introduces a knowledge representation called strategy designed to support the application of formal methods in software engineering. Strategies represent development knowledge used to perform different software engineering activities. The development of an artifact is modeled as a problem solving process. An important goal is to guarantee semantic properties of the developed product. Strategies support stepwise automation of development tasks. Since the definition of strategies is generic, they can be employed in different phases of the software lifecycle. The notion of strategy is complemented by a generic system architecture that serves as a template for the implementation of support tools for strategy-based problem solving. Two different instantiations of the strategy framework and an implemented program synthesis system are presented. | |||||
BibTeX:
@misc{Heisel96x,
year = {1996},
title = {Strategies -- A Generic Knowledge Representation Mechanism for Software Development Activities},
author = {Heisel, Maritta}
}
|
|||||
| 1996 | Combining Z and Real-Time CSP for the Development of Safety-Critical Systems | Heisel, M. & Sühl, C. | |||
| Abstract: We present a method for the specification and development of safety-critical systems. It is based on a combination of the formal languages Z and real-time CSP. Different reference architectures are introduced that represent frequently used designs of safety- critical systems. For these reference architectures, schematic specifications are given that can serve as guidelines for specifiers. Once the specification of the system is developed, it can be validated using a checklist and by demonstrating properties of it. Further steps consist in the renement of the specification and its implementation that can partially be supported by machine. | |||||
BibTeX:
@misc{HeiselSuehl96x,
year = {1996},
title = {Combining {Z} and Real-Time {CSP} for the Development of Safety-Critical Systems},
author = {Heisel, Maritta and S{\"{u}}hl, Carsten}
}
|
|||||
| 1996 | Expression of Style in Formal Specification | Souquières, J. & Heisel, M. | Proceedings Software Quality Conference | ||
| Abstract: This paper presents a framework for supporting the acquisition of formal specifications. It is possible to identify certain styles or orientation approaches according to which the specification process is performed. These styles are used locally, i.e. even in one development, one switches between different styles. Therefore, it is not reasonable to identify styles with specification languages, as is usually the case. We propose to explicitly represent styles as sets of development operators in a process oriented way which is independent of the respective specification language that is used. Our approach is illustrated by a case study where of subset of the Unix file system is specified. | |||||
BibTeX:
@inproceedings{Souqui`eres1996,
year = {1996},
title = {Expression of Style in Formal Specification},
booktitle = {Proceedings Software Quality Conference},
author = {Souqui{\`{e}}res, Jeanine and Heisel, Maritta},
publisher = {University of Abertay Dundee},
pages = {56--65}
}
|
|||||
| 1995 | Specification of the Unix File System: A Comparative Case Study | Heisel, M. | Proc. 4th Int. Conference on Algebraic Methodology and Software Technology | Springer | |
| Abstract: The starting point of this investigation are two different formal specifications of the user´s view of the Unix file system, one algebraic and one model-based. The different features exhibited by the specifications give rise to a discussion of desirable and undesirable properties of formal specifications. | |||||
BibTeX:
@inproceedings{Heisel1995,
year = {1995},
title = {Specification of the {U}nix File System: A Comparative Case Study},
booktitle = {Proc. 4th Int. Conference on Algebraic Methodology and Software Technology},
author = {Heisel, Maritta},
publisher = {Springer},
series = {LNCS 936},
pages = {475--488},
url = {http://www.springerlink.com/}
}
|
|||||
| 1995 | A Pragmatic Approach to Formal Specification | Heisel, M. | Proceedings Workshop on Semantic Integration in Complex Systems: Collective Behavior in Business rules and Software Transactions, OOPSLA'95 | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1995a,
year = {1995},
title = {A Pragmatic Approach to Formal Specification},
booktitle = {Proceedings Workshop on Semantic Integration in Complex Systems: Collective Behavior in Business rules and Software Transactions, OOPSLA'95},
author = {Heisel, Maritta},
publisher = {Robert Morris College},
pages = {25--29}
}
|
|||||
| 1995 | Six Steps Towards Provably Safe Software | Heisel, M. | Proceedings of the 14th International Conference on Computer Safety, Reliability and Security (SAFECOMP) | ||
| Abstract: We present an approach to the specification and implementation of provably safe software. It uses well-established tools and techniques that are usually employed to ensure correctness rather than safety of software. The approach comprises six steps each of which is complemented by some proof obligations. For each step the safety-related aspects are clearly elaborated. Thus designers of safety-critical systems are given guidance that helps to avoid potentially dangerous gaps in the specification of the system´s safety properties. | |||||
BibTeX:
@inproceedings{Heisel1995b,
year = {1995},
title = {Six Steps Towards Provably Safe Software},
booktitle = {Proceedings of the 14th International Conference on Computer Safety, Reliability and Security (SAFECOMP)},
author = {Heisel, Maritta},
publisher = {Springer London},
pages = {191--205}
}
|
|||||
| 1995 | Einbettung mathematischer Techniken in den Systementwurf | Heisel, M., Jähnichen, S., Simons, M. & Weber, M. | Proceedings Softwaretechnik '95 | ||
| Abstract: to be inserted | |||||
BibTeX:
@incollection{Heisel1995d,
year = {1995},
title = {Einbettung mathematischer {T}echniken in den {S}ystementwurf},
booktitle = {Proceedings Softwaretechnik '95},
author = {Heisel, Maritta and J{\"{a}}hnichen, Stefan and Simons, Martin and Weber, Matthias},
publisher = {Softwaretechnik-Trends},
volume = {15},
number = {3},
pages = {98--106}
}
|
|||||
| 1995 | Embedding Mathematical Techniques in System Engineering | Heisel, M., Jähnichen, S., Simons, M. & Weber, M. | Proceedings Workshop on Formal Methods Application in Software Engineering Practice, International Conference on Software Engineering | ||
| Abstract: Some of the reasons why formal methods have not been widely accepted in practice are analyzed. This analysis provides the basis for a more modest approach to embedding mathematical and formal techniques into the system design process: identifying places in traditional design methodologies where formal reasoning can be convincingly introduced. The approach is outlined in general and illustrated by giving overviews of three different research activities. | |||||
BibTeX:
@inproceedings{Heisel1995e,
year = {1995},
title = {Embedding Mathematical Techniques in System Engineering},
booktitle = {Proceedings Workshop on Formal Methods Application in Software Engineering Practice, International Conference on Software Engineering},
author = {Heisel, Maritta and J{\"{a}}hnichen, Stefan and Simons, Martin and Weber, Matthias},
pages = {53--60}
}
|
|||||
| 1995 | Bi-directional Approach to Modeling Architectures | Heisel, M. & Krishnamurthy, B. | |||
| Abstract: Software architecture can be broken down into a collection of architectural styles and services. We seek to capture a set of criteria to characterize architecture styles. The presence or absence of a criterion may be reflected in the features or limitations of the realization of an architecture. Our idea is to enumerate a set of criteria for a given architectural style (e.g. event-action) and try to map it to a formal specification of an instance of the style. We then map the formal specification to a reverse engineered level of the code. The goal is to bridge the gap between the architecture and the realization. In addition, the breakup into criteria and the mappings provides a way to locate functional and non-functional aspects of the architecture in the code. | |||||
BibTeX:
@techreport{Heisel1995f,
year = {1995},
title = {Bi-directional Approach to Modeling Architectures},
author = {Heisel, Maritta and Krishnamurthy, Balachander},
number = {95-31}
}
|
|||||
| 1995 | YEAST -- A formal specification case study in Z | Heisel, M. & Krishnamurthy, B. | |||
| Abstract: A formal specication in the language Z of an event-action system called YEAST is presented. Such a specification helps users of event- action systems to a deeper understanding of the system´s features than can be gained by natural language descriptions. Designers of such systems can use the formal specification as a starting point for the specification of new event-action systems. Finally, members of the formal specification community can profit from the general lessons learnt in this case study. | |||||
BibTeX:
@techreport{Heisel1995g,
year = {1995},
title = {{YEAST} -- A formal specification case study in {Z}},
author = {Heisel, Maritta and Krishnamurthy, Balachander},
number = {95-32}
}
|
|||||
| 1994 | Strategy-Based Program Synthesis with IOSS | Heisel, M., Santen, T. & Zimmermann, D. | Proceedings Workshop on Systems for Computer-Aided Specification, Development and Verification | ||
| Abstract: This paper presents the program synthesis system IOSS (Integrated Open Synthesis System). It is based on the concept of strategy as a uniform representation of development knowledge making the integration of different synthesis methods possible. The implemented system is an instantiation of a generic system architecture designed to provide machine support for the application of formal methods in software development The properties of the system are demonstrated by means of a sample development. | |||||
BibTeX:
@inproceedings{Heisel1994,
year = {1994},
title = {Strategy-Based Program Synthesis with {IOSS}},
booktitle = {Proceedings Workshop on Systems for Computer-Aided Specification, Development and Verification},
author = {Heisel, Maritta and Santen, Thomas and Zimmermann, Dominik},
publisher = {Christian-Albrechts-Universit{\"{a}}t Kiel},
series = {Technical Report 9416},
pages = {16--30}
}
|
|||||
| 1994 | Specification of the Unix Filing System: A Comparative Case Study | Heisel, M. | Proceedings Workshop on Methodology for the Development of Computer System Specifications | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1994a,
year = {1994},
title = {Specification of the {U}nix Filing System: A Comparative Case Study},
booktitle = {Proceedings Workshop on Methodology for the Development of Computer System Specifications},
author = {Heisel, Maritta},
publisher = {University of Namur},
pages = {25--36}
}
|
|||||
| 1994 | A Formal Notion of Strategy for Software Development | Heisel, M. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Heisel1994b,
year = {1994},
title = {A Formal Notion of Strategy for Software Development},
author = {Heisel, Maritta},
number = {94--28}
}
|
|||||
| 1994 | Korrekte Software: Nur eine Illusion? | Heisel, M. & Weber-Wulff, D. | Informatik -- Forschung und Entwicklung | ||
| Abstract: to be inserted | |||||
BibTeX:
@article{Heisel1994c,
year = {1994},
title = {{K}orrekte {S}oftware: {N}ur eine {I}llusion?},
author = {Heisel, Maritta and Weber-Wulff, Debora},
journal = {{I}nformatik -- {F}orschung und {E}ntwicklung},
volume = {9},
number = {4},
pages = {192--200}
}
|
|||||
| 1994 | How to Manage Formal Specifications? | Souquières, J. & Heisel, M. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Souqui`eres1994,
year = {1994},
title = {How to Manage Formal Specifications?},
author = {Souqui{\`{e}}res, Jeanine and Heisel, Maritta},
number = {CRIN 94-R-214}
}
|
|||||
| 1993 | A Theory of Top-Down Problem Solving Based on Relational Algebra | Heisel, M. | Proceedings ERCIM Workshop on Development and Transformation of Programs | ||
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1993,
year = {1993},
title = {A Theory of Top-Down Problem Solving Based on Relational Algebra},
booktitle = {Proceedings ERCIM Workshop on Development and Transformation of Programs},
author = {Heisel, Maritta},
publisher = {INRIA Lorraine},
pages = {79--92}
}
|
|||||
| 1992 | A Relational Approach to Top-Down Program Synthesis | Heisel, M. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Heisel1992,
year = {1992},
title = {A Relational Approach to Top-Down Program Synthesis},
author = {Heisel, Maritta},
number = {92--12}
}
|
|||||
| 1992 | Formalizing and Implementing Gries's Program Development Method in Dynamic Logic | Heisel, M. | Science of Computer Programming | ||
| Abstract: to be inserted | |||||
BibTeX:
@article{Heisel1992a,
year = {1992},
title = {Formalizing and Implementing {G}ries's Program Development Method in Dynamic Logic},
author = {Heisel, Maritta},
journal = {Science of Computer Programming},
volume = {18},
pages = {107--137}
}
|
|||||
| 1992 | Formale Programmentwicklung mit dynamischer Logik | Heisel, M. | Deutscher Universitätsverlag | ||
| Abstract: to be inserted | |||||
BibTeX:
@book{Heisel1992b,
year = {1992},
title = {{F}ormale {P}rogrammentwicklung mit dynamischer {L}ogik},
author = {Heisel, Maritta},
publisher = {Deutscher Universit{\"{a}}tsverlag},
url = {http://www.duv.com/}
}
|
|||||
| 1991 | Formal Software Development with the KIV System | Heisel, M., Reif, W. & Stephan, W. | Automating Software Design | ||
| Abstract: to be inserted | |||||
BibTeX:
@incollection{Heisel1991,
year = {1991},
title = {Formal Software Development with the {KIV} System},
booktitle = {Automating Software Design},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {AAAI Press},
pages = {547--574}
}
|
|||||
| 1990 | Der Karlsruhe Interactive Verifier (KIV) | Heisel, M., Menzel, W., Reif, W. & Stephan, W. | Sichere Software. Formale Spezifikation und Verifikation vertrauenswürdiger Systeme | ||
| Abstract: to be inserted | |||||
BibTeX:
@incollection{Heisel1990,
year = {1990},
title = {Der {K}arlsruhe {I}nteractive {V}erifier ({KIV})},
booktitle = {Sichere {S}oftware. Formale {S}pezifikation und {V}erifikation vertrauensw{\"{u}}rdiger {S}ysteme},
author = {Heisel, Maritta and Menzel, W. and Reif, W. and Stephan, W.},
publisher = {H{\"{u}}thig Buch Verlag},
pages = {172-193}
}
|
|||||
| 1990 | Tactical Theorem Proving in Program Verification | Heisel, M., Reif, W. & Stephan, W. | Proceedings 10th International Conference on Automated Deduction | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1990a,
year = {1990},
title = {Tactical Theorem Proving in Program Verification},
booktitle = {Proceedings 10th International Conference on Automated Deduction},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
series = {LNAI 449},
pages = {117--131},
url = {http://www.springerlink.com/}
}
|
|||||
| 1990 | Formal Program Development by Goal Splitting and Backward Loop Formation | Heisel, M. & Santen, T. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Heisel1990b,
year = {1990},
title = {Formal Program Development by Goal Splitting and Backward Loop Formation},
author = {Heisel, Maritta and Santen, Thomas},
number = {32/90}
}
|
|||||
| 1989 | Proceedings Workshop on Verification, Construction and Synthesis of Programs, Karlsruhe, April 6-7 | Furbach, U., Heisel, M., Reif, W. & Werner, S. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Furbach1989,
year = {1989},
title = {Proceedings Workshop on Verification, Construction and Synthesis of Programs, {K}arlsruhe, {A}pril 6-7},
author = {Furbach, Ulrich and Heisel, Maritta and Reif, Wolfgang and Werner, Stephan},
number = {19/89}
}
|
|||||
| 1989 | A Formalization and Implementation of Gries's Development Method within the KIV Environment | Heisel, M. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Heisel1989,
year = {1989},
title = {A Formalization and Implementation of {G}ries's Development Method within the {KIV} Environment},
author = {Heisel, Maritta},
number = {3/89}
}
|
|||||
| 1989 | A Dynamic Logic for Program Verification | Heisel, M., Reif, W. & Stephan, W. | Proceedings Logic at Botik | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1989a,
year = {1989},
title = {A Dynamic Logic for Program Verification},
booktitle = {Proceedings Logic at Botik},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
series = {LNCS 363},
pages = {134--145},
url = {http://www.springerlink.com/}
}
|
|||||
| 1989 | Machine-Assisted Program Construction and Verification | Heisel, M., Reif, W. & Stephan, W. | Proceedings of the 12th German Workshop for Artificial Intelligence | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1989b,
year = {1989},
title = {Machine-Assisted Program Construction and Verification},
booktitle = {Proceedings of the 12th {G}erman {W}orkshop for {A}rtificial {I}ntelligence},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
number = {216},
series = {Informatik Fachberichte},
pages = {338--347},
url = {http://www.springerlink.com/}
}
|
|||||
| 1988 | Program Verification Using Dynamic Logic | Heisel, M., Reif, W. & Stephan, W. | Proceedings of the first Workshop on Computer Science Logic | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1988,
year = {1988},
title = {Program Verification Using Dynamic Logic},
booktitle = {Proceedings of the first Workshop on Computer Science Logic},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
series = {LNCS 329},
pages = {102--117},
url = {http://www.springerlink.com/}
}
|
|||||
| 1988 | Implementing Verification Strategies in the KIV System | Heisel, M., Reif, W. & Stephan, W. | Proceedings 9th International Conference on Automated Deduction | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1988a,
year = {1988},
title = {Implementing Verification Strategies in the {KIV} System},
booktitle = {Proceedings 9th International Conference on Automated Deduction},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
series = {LNCS 310},
pages = {131--140},
url = {http://www.springerlink.com/}
}
|
|||||
| 1987 | Program Verification by Symbolic Execution and Induction | Heisel, M., Reif, W. & Stephan, W. | Proceedings of the 11th German Workshop for Artificial Intelligence | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Heisel1987,
year = {1987},
title = {Program Verification by Symbolic Execution and Induction},
booktitle = {Proceedings of the 11th {G}erman {W}orkshop for {A}rtificial {I}ntelligence},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
series = {Informatik Fachberichte 152},
pages = {201--210},
url = {http://www.springerlink.com/}
}
|
|||||
| 1986 | An Interactive Verification System Based on Dynamic Logic | Hähnle, R., Heisel, M., Reif, W. & Stephan, W. | Proceedings 8th International Conference on Automated Deduction | Springer | |
| Abstract: to be inserted | |||||
BibTeX:
@inproceedings{Hahnle1986,
year = {1986},
title = {An Interactive Verification System Based on Dynamic Logic},
booktitle = {Proceedings 8th International Conference on Automated Deduction},
author = {H{\"{a}}hnle, Reiner and Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
publisher = {Springer},
number = {230},
series = {LNCS 230},
pages = {306--315},
url = {http://www.springerlink.com/}
}
|
|||||
| 1986 | A Functional Language to Construct Proofs | Heisel, M., Reif, W. & Stephan, W. | |||
| Abstract: to be inserted | |||||
BibTeX:
@techreport{Heisel1986,
year = {1986},
title = {A Functional Language to Construct Proofs},
author = {Heisel, Maritta and Reif, Wolfgang and Stephan, Werner},
number = {1/86}
}
|
|||||
Created by JabRef on 13/03/2018.