Burkhart Wolff

David Basin, Burkhart Wolff

and software testing. As far as symbolic verification methods and modelbased testing techniques are concerned, the interest among researchers in the mutual fertilization of these fields is growing....

Overview 2 (2008)

• Formalizing Class Diagrams (2008)

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker

• Embedding OCL into Isabelle/HOL • Conclusion

Proof Environments for Formal Specification Languages (2008)

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Winter Term, Achim D. Brucker

Isabelle is not alone there are many successful theorem provers, e.g.: • Coq:

Organizers (2008)

John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...

This report contains the papers presented at FTfJP ’07: 9th workshop on Formal

Extensible Object-oriented Data Models in Isabelle/HOL (2008)

Under consideration for publication in Formal Aspects of Computing Verifying a Signature Architecture — A Comparative Case Study (2008)

Abstract We present an extensible encoding of object-oriented data models into higher-order logic (HOL). Our encoding is supported by a datatype package that enables the use of the shallow embedding...

Organizers (2008)

John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...

This report contains the papers presented at FTfJP ’07: 9th workshop on Formal

David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff

Abstract. We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently...

Semantic Issues of OCL: Past, Present, and Future (2008)

Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Dan Chiorean, Birgit Demuth, ...

Abstract: We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...

HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2008)

Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff

The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...

An MDA Framework Supporting OCL (2008)

Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Tiziana Margaria, Julia Padberg, ...

Abstract: We present a model-driven architecture (MDA) framework that integrates formal analysis techniques into an industrial software development process model. This comprises modeling using...

Semantic Issues of OCL: Past, Present, and Future (2008)

Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Dan Chiorean, Birgit Demuth, ...

Abstract: We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...

Abstract A Case Study of a Formalized Security Architecture (2008)

Achim D. Brucker, Eth Zürich, Burkhart Wolff

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...

Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) A Verification Approach for Applied System Security (2008)

An MDA Framework Supporting OCL (2008)

The date of receipt and acceptance will be inserted by the editor Abstract. We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by...

Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Tiziana Margaria, Julia Padberg, ...

Abstract: We present a model-driven architecture (MDA) framework that integrates formal analysis techniques into an industrial software development process model. This comprises modeling using...

TAS - A Generic Window Inference System (2007)

Correct Code-Generation in a Generic Framework (2007)

This paper presents work on technology for transformational proof and program development, as used by window inference calculi and transformation systems. The calculi are characterised by a certain...

Burkhart Wolff, Thomas Meyer

. One major motivation for theorem provers is the development of veried programs. In particular, synthesis or transformational development techniques aim at a formalised conversion of the original...

SPEC - A Unified Approach to Modularity, Parametrisation and Views in Attributations (2007)

Exte Nd Ed, Burkhart Wolff

) Burkhart Wolff 1. Introduction This paper is an extended abstract of [Wolff 94a], whose purpose is twofold: Firstly, it attempts to generalise the notion of "attribute grammar" to the...

Finitary Matching For Constructor Based Theories (2007)

Hui Shi, Burkhart Wolff

Acyclic Constructor Based (ACB) theories are induced by a restricted class of equations, which can be treated as convergent rewrite systems. We claim that solving matching problems with such theories...

Generic Transformation Systems for Formal Methods (2007)

Christoph Lüth, Thomas Meyer, Burkhart Wolff

Introduction We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle. Their distinguishing feature...

Transformational Development of LEX (2007)

Junbo Liu, Burkhart Wolff

In this paper we present a transformational development of an efficient implementation of a lexical scanner, corresponding to the well-known LEX in the UNIX system. Based on a formal requirement...

A Calculus of Transformation (Extended Abstract) (2007)

Burkhart Wolff, Hui Shi

) Burkhart Wolff, Hui Shi 1. Conceptual view This paper presents the concepts and the semantics of a transformation calculus TC that is generic w.r.t. concrete object languages (see also [WS 94])....

A Decidable Second-Order Semantic Matching in Isabelle (2007)

Hui Shi, Burkhart Wolff

We present a complete matching algorithm and an efficient implementation in the theorem prover Isabelle for solving a class of second-order semantic matching problems, where the equational theory...

Abstract A Case Study of a Formalized Security Architecture (2007)

Achim D. Brucker, Eth Zürich, Burkhart Wolff

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...

HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2007)

Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff

The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...

Verifying Explicit Substitution Calculi in Binding Structures with Effect-Binding (2007)

Burkhart Wolff

Abstract. Binding structures enrich traditional abstract syntax by providing support for representing binding mechanisms (based on deBruijn indices), term-schemata and a very clean algebraic theory...

Technical Report 157 Checking OCL Constraints in Distributed Component Based Systems (2007)

Test-sequence generation with HOL-TestGen – with an application to firewall testing (2007)

We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...

Abstract HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is...

Outline (2007)

Test-sequence generation with HOL-TestGen – with an application to firewall testing (2007)

Outline Theorem-prover based Testing with HOL-TestGen (2007)

Abstract HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is...

B.: Building formal method tools in the Isabelle/Isar framework (2007)

Makarius Wenzel, Burkhart Wolff

Abstract We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising...

B.: Building formal method tools in the Isabelle/Isar framework (2007)

Makarius Wenzel, Burkhart Wolff

Abstract We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising...

Assisted proof document authoring (2006)

David Aspinall, Christoph Lüth, Burkhart Wolff

Abstract. Recently, significant advances have been made in formalised mathematical texts for large, demanding proofs. But although such large developments are possible, they still take an inordinate...

A Model Transformation Semantics and Analysis Methodology for SecureUML (2006)

An MDA Framework Supporting OCL (2006)

Abstract SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a uml notation in terms of a uml profile, and can be combined...

Applications (2006)

Achim D. Brucker, Joint Work, Jürgen Doser, Burkhart Wolff, A St, Ard Compliant, ...

The semantics of ocl 2.0 is spread over several places: Chapter 7 “ocl Language Description ” (informative): introduces ocl informally using examples, Chapter 10 “Semantics Described using uml...

Achim D. Brucker, Jürgen Doser, Burkhart Wolff

Abstract We present an mda framework, developed in the functional programming language sml, that tries to bridge the gap between formal software development and the needs of industrial software...

Semantic issues of ocl: Past, present, and future (2006)

Achim D. Brucker, Jürgen Doser, Burkhart Wolff

Abstract We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...

A package for extensible object-oriented data models with an application to imp (2006)

Assisted proof document authoring (2006)

with an Application to IMP++

David Aspinall, Christoph Lüth, Burkhart Wolff

Abstract. Recently, significant advances have been made in formalised mathematical texts for large, demanding proofs. But although such large developments are possible, they still take an inordinate...

Contents (2006)

Achim D. Brucker, Burkhart Wolff, Burkhart Wolff

Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies. Permission is granted to copy and...

Applications (2006)

Achim D. Brucker, Jürgen Doser, Burkhart Wolff

The semantics of ocl 2.0 is spread over several places: Chapter 7 “ocl Language Description ” (informative): introduces ocl informally using examples, Chapter 10 “Semantics Described using uml...

A Model Transformation Semantics and Analysis Methodology for SecureUML (2006)

Achim D. Brucker, Achim D. Brucker, Jürgen Doser, Jürgen Doser, Burkhart Wolff, Burkhart Wolff

Abstract SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a uml notation in terms of a uml profile, and can be combined...

A package for extensible object-oriented data models with an application to imp (2006)

• Formalizing Class Diagrams (2005)

We present a datatype package that enables the use of shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented...

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker

Higher-Order Logic Application: Denotational Semantics for Functional Languages 1057 Global Outline (2) (2005)

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Well-founded Orders

◦ Z and Data-Refinement,

• Arithmetic (2005)

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Scons X Y

We are still looking at how the different parts of mathematics are encoded in the Isabelle/HOL library.

Higher-Order Logic (HOL) is: (2005)

David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, David Basin

Higher-Order Logic (HOL) is: • an expressive foundation for mathematics: analysis, algebra,... computer science: program correctness, hardware verification,...

HOL-TestGen 1.0.0 user guide (2005)

Achim D. Brucker, Burkhart Wolff, Burkhart Wolff

Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies. Permission is granted to copy and...

Information Security (2005)

Symbolic test case generation for primitive recursive functions (2005)

Verification of a signature architecture with HOL-Z (2005)

Abstract We present a method for the automatic generation of test cases for HOL formulae containing primitive recursive predicates. These test cases can be used for the animation of specifications as...

David Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff

Abstract. We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to specify and verify a security architecture for administering digital signatures. We have used HOL-Z to...

Formalizing Java’s two’s-complement integral type in isabelle/HOL (2003)

Nicole Rauch, Burkhart Wolff

We present a formal model of the Java two’s-complement integral arithmetics. The model directly formalizes the arithmetic operations as given in the Java Language Specification (JLS). The algebraic...

A case study of a formalized security architecture (2003)

Theorem Proving in Higher Order Logics (2003)

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...

David Basin, Burkhart Wolff (eds.), Eth Zentrum, Burkhart Wolff

Algebra in Type Theory with Dependent Records . . . 13 Xin Yu, Aleksey Nogin, Alexei Kopylov and Jason Hickey Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant . . . . . . ....

A case study of a formalized security architecture (2003)

Using theory morphisms for implementing formal methods tools (2003)

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...

A proposal for a formal OCL semantics in Isabelle/HOL (2002)

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...

HOL-OCL: Experiences, Consequences and Design Choices (2002)

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...

A proposal for a formal OCL semantics in Isabelle/HOL (2002)

Abstract 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....

HOL-OCL: Experiences, Consequences and Design Choices (2002)

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...

A proposal for a formal OCL semantics in Isabelle/HOL (2002)

Abstract 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....

HOL-Z 2.0: A proof environment for Z-specifications (2002)

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...

A Note on Design Decisions of Formalization of the OCL - The View Freiburg (2002)

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...

HOL-Z 2.0: A proof environment for Z-specifications (2002)

We compare several formal and informal approaches define the semantics the Object Constraint Language (OCL) [22]. This comparison reveals a number minor and major design problems settled upcoming...

-- The View of Freiburg-- (2002)

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...

A proposal for a formal OCL semantics in Isabelle/HOL (2002)

Technical Report 182 A CVS-Server Security Architecture Concepts and Formal Analysis (2002)

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...

A Note on Design Decisions of a Formalization of the OCL — The View of Freiburg — (2002)

We would like to thank Nicole Rauch (Uni Kaiserslautern) for many valuable comments

HOL-OCL: Experiences, Consequences and Design Choices (2002)

We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL) [22]. This comparison reveals a number of minor and major design problems to be...

-- Concepts and Formal Analysis (2002)

Abstract 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....

A proposal for a formal OCL semantics in Isabelle/HOL (2002)

This is based on a refinement, mapping a system architecture on an implementation architecture abstractly describing CVS in our implementation. The system architecture describes the abstract system...

HOL-Z 2.0: A proof environment for Z-specifications (2002)

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...

Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff

The design of tools for formal specification languages (SL) can be roughly devided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...

Abstract (2002)

Burkhart Wolff, Oliver Berthold, Sebastian Clauß, Hannes Federrath, Stefan Köpsell, Andreas Pfitzmann, ...

We present a formal model of Chaum’s Mix concept and apply known analysis techniques to a new type of security property, namely anonymity, in a network composed of senders, receivers and Mix...

Testing distributed component based systems using UML/OCL (2001)

Testing Distributed Component Based Systems Using UML/OCL (2001)

We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...

Achim Brucker Burkhart, Achim D. Brucker, Burkhart Wolff

We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...

Testing distributed component based systems using UML/OCL (2001)

Technical Report 157 Checking OCL Constraints in Distributed Component Based Systems (2001)

We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...

Component Based Systems (2001)

We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...

Testing distributed component based systems using UML/OCL (2001)

Abstract We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for...

WordNet 1.6 Reference Manual, Section 7: Miscellaneous Topics, WordNet database statistics -- wnstats(7WN). Available in the World-Wide Web at http://www.cogsci.princeton.edu/~wn (2000)

Abstract We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for...

Burkhart Wolff, Thomas Meyer

tminformatik.uni-bremen.de Abstract. One major motivation for theorem provers is the development of verified programs. In particular, synthesis or transformational development techniques aim at a...

More About TAS and IsaWin - Tools for Formal Program Development (2000)

TAS — a generic window inference system (2000)

We present a family of tools for program development and verification, comprising the transformation system TAS and the theorem proving interface IsaWin. Both are based on the theorem prover Isabelle...

More about TAS and IsaWin: Tools for formal program development (2000)

Abstract. This paper presents work on technology for transformational proof and program development, as used by window inference calculi and transformation systems. The calculi are characterised by a...