Achim D. Brucker, Burkhart Wol
CVS is a widely known version management system, which can be used for the distributed development of software as well as its distribution from a central database. In this paper, we provide an...
Using theory morphisms for implementing formal methods tools (2003)
Achim D. Brucker, Burkhart Wol
Abstract Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed meta-logic, which allows their safe...
A case study of a formalized security architecture (2003)
Achim D. Brucker, Frank Rittinger, Burkhart Wol
These days, the Concurrent Versions System (CVS) is a widely used tool for version management in many industrial software development projects, and plays a key role in open source projects usually...
Proof Environment For, Achim D. Brucker, Frank Rittinger, Burkhart Wol, ...
We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the embedding,...
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wol
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wol
Abstract: We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the...
Proof Environment For, Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wol
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wol# Albert-Ludwigs-Universitat Freiburg {brucker,friedric,rittinge,wolff}@informatik.uni-freiburg.de 1
HOL-OCL: Experiences, Consequences and Design Choices (2002)
Achim Brucker And, Achim D. Brucker, Burkhart Wol
Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [1], we explore several key issues of the design of a formal semantics of the OCL. These...