Whole-Program Specifications Permit Better Abstraction and Concurrent Implementations (2009)
Bart Jacobs, Frank Piessens, Pieter Bekaert, Eric Steegmans
This article previews a new system for the formal specification and verification of object-oriented programs and modules. It differs from existing systems (see specifically [1], [4], and [3]) in that...
This paper studies convex sets categorically, namely as algebras of a distribution monad. It is shown that convex sets occur in two dual adjunctions, namely one with preframes via the Boolean truth...
Categorical Views on Computations on Trees (Extended Abstract) (2009)
Ichiro Hasuo, Bart Jacobs, Tarmo Uustalu
Abstract. Computations on trees form a classical topic in computing. These computations can be described in terms of machines (typically called tree transducers), or in terms of functions. This paper...
Dismantling MIFARE Classic (2009)
Flavio D. Garcia, Ruben Muijrers, Peter Van Rossum, Roel Verdult, Ronny Wichers Schreur, ...
Abstract. The mifare Classic is a contactless smart card that is used extensively in access control for office buildings, payment systems for public transport, and other applications. We reverse...
SEMANTICS OF GRAMMARS AND ATTRIBUTES VIA INITIALITY (2009)
ABSTRACT. This paper uses elementary categorical techniques to systematically describe the semantics of context-free grammars and of attribute evaluation for such grammars. The novelty lies in...
AHA: Amortized Heap Space Usage Analysis – Project Paper – (2009)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
Abstract: This paper introduces AHA, an NWO-funded2 344K Euro project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
Distributive laws for the coinductive solution of recursive equations (2009)
This paper illustrates the relevance of distributive laws for the solution of recursive equations, and shows that one approach for obtaining coinductive solutions of equations via infinite terms is...
support static detection of bugs in (2009)
Lieven Desmet, Bart Jacobs, Frank Piessens, Wolfram Schulte, Dries Vanoverberghe
Concern-specific annotation languages to
Bart Jacobs, Engelbert Hubbers, Joseph Kiniry, Martijn Oostdijk
This abstract provides some background information about the electronic voting experiment that is planned in the Netherlands for the European Elections of 2004, and about our own involvement in the...
Orthomodular lattices, Foulis Semigroups and Dagger Kernel Categories (2009)
This paper is a sequel to arXiv:0902.2355 and continues the study of quantum logic via dagger kernel categories. It develops the relation between these categories and both orthomodular lattices and...
Quantum Logic in Dagger Kernel Categories (2009)
This paper investigates quantum logic from the perspective of categorical logic, and starts from minimal assumptions, namely the existence of involutions/daggers and kernels. The resulting structures...
In deze scriptie vindt u hoe je te werk moet gaan bij het maken van een lichtstudie. Het is niet enkel en alleen het ontwerpen van een nieuwe installatie er komt veel meer bij kijken. Je ontwerp moet...
On the Role of Invariants in Reasoning about Object-Oriented Languages (2008)
Cees-bart Breunesse, Bart Jacobs, Erik Poll
1 Introduction Preconditions, postconditions and invariants are universally accepted as the basic ingredients for specification of OO programs. Invariants for classes play an important role in...
Ichiro Hasuo, The Netherl, Ichiro Hasuo, Bart Jacobs, Ana Sokolova
is attracting growing
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
Prof. Dr. Pieter Hartel, D. T. Janssen, Prof. Dr. Bart Jacobs
Contact info: www.sentinels.nl
This paper reports on an effort to increase the reliability of JavaCard-based smart cards by means of formal specification and verification of JavaCard source code. As a first step, lightweight...
Inspector Methods for State Abstraction (2008)
Most classes in an object-oriented program provide access to an object’s state through methods, so that client code does not depend on and cannot interfere with the object’s internal...
AHA: Amortized Heap Space Usage Analysis – Project Paper – (2008)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
This paper introduces AHA, an NWO-funded 1 344K Euro research project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
Abstract Generic Trace Theory (2008)
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism ” such as classical non-determinism (with a...
Abstract Coalgebras and Monads in the Semantics of Java ⋆ (2008)
This paper describes the basic structures in the denotational and axiomatic semantics of sequential Java, both from a monadic and a coalgebraic perspective. This semantics is an abstraction of the...
Categorical Views on Computations on Trees (Extended Abstract) (2008)
Ichiro Hasuo, Bart Jacobs, Tarmo Uustalu
Abstract. Computations on trees form a classical topic in computing. These computations can be described in terms of machines (typically called tree transducers), or in terms of functions. This paper...
Formal Specification of the JavaCard API in JML: the APDU class Abstract (2008)
This paper reports on an effort to increase the reliability of JavaCard-based smart cards by means of formal specification and verification of JavaCard source code. As a first step, formal interface...
Bart Jacobs, Jan Smans, Frank Piessens
A simple sequential reasoning approach for sound
Cation Language Ccsl, Jan Rothe, Hendrik Tews, Hendrik Tews, ...
This paper presents the Coalgebraic Class Speci cation Language ccsl that is developed within the loop project on formal methods for object-oriented languages . ccsl allows the (coalgebraic) speci...
Increased security through open source (2008)
Hoepman, Jaap-Henk, Jacobs, Bart
In this paper we discuss the impact of open source on both the security and transparency of a software system. We focus on the more technical aspects of this issue, combining and extending arguments...
Crossing Borders: Security and Privacy Issues of the European e-Passport (2008)
Hoepman, Jaap-Henk, Hubbers, Engelbert, Jacobs, Bart, Oostdijk, Martijn, Schreur, Ronny Wichers
The first generation of European e-passports will be issued in 2006. We discuss how borders are crossed regarding the security and privacy erosion of the proposed schemes, and show which borders need...
Inrichting van het Roefsels Bosch (2008)
Abstract Gedurende de stage bij Libost-Groep N.V. werd er mij voorgesteld om de verkaveling "het Roefsels Bosch" uit te werken in samenwerking met mijn promotoren ing. J. Vanderstraeten en ing. G....
possibilitistic and probabilistic systems (2008)
Coalgebraic trace semantics for combined
Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens
The primary goal of exception mechanisms is to help ensure that when an operation fails, code that depends on the operation’s successful completion is not executed (a property we call dependency...
Abstract This paper introduces a novel approach or architecture for fraud-resistant and privacy-friendly Electronic Traffic Pricing (ETP). One salient contribution is that it can satisfy the...
Frédéric Vogels, Bart Jacobs, Frank Piessens, Frédéric Vogels, Bart Jacobs, Frank Piessens, ...
A machine checked soundness proof for
Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens
This note describes a separation-logic-based approach for the specification and verification of safety properties of pointer-manipulating imperative programs. The programmer may declare inductive...
Exemplaric Expressivity of Modal Logics ⋆ (2008)
Abstract This paper investigates expressivity of modal logics for transition systems, multitransition systems, Markov chains, and Markov processes, as coalgebras of the powerset, finitely supported...
An automatic verifier for java-like programs based on dynamic frames (2008)
Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte
Abstract. Data abstraction is crucial in the construction of modular programs, since it ensures that internal changes in one module do not propagate to other modules. In object-oriented programs,...
1 A Programming Model for Concurrent Object-Oriented Programs (2008)
Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan, M. Leino, Wolfram Schulte
Reasoning about multithreaded object-oriented programs is difficult, due to the nonlocal nature of object aliasing and data races. We propose a programming regime (or programming model) that rules...
A number of difficulties in the formalism of Pure Type Systems (PTS's) is discussed and an alternative classification system for typed calculi is proposed. In the new approach the main novelty...
Formal Specication of the JavaCard API in JML: the APDU class (2007)
This paper reports on an eort to increase the reliability of JavaCard-based smart cards by means of formal specication and verication of JavaCard source code. As a rst step, formal interface...
Ulrich Hensel, Marieke Huisman, Bart Jacobs, Hendrik Tews, Inst Theor Informatik, Tu Dresden, ...
Abstract. A formal language ccsl is introduced for describing specifications of classes in object-oriented languages. We show how class specifications in ccsl can be translated into higher order...
Java Program Verication Challenges (2007)
Bart Jacobs, Joseph Kiniry, Martijn Warnier
Abstract. This paper aims to raise the level of verication challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on...
A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building block for a "lax...
JavaCard Program Verication (2007)
bart This abstract provides some background information on smart cards, and explains the challenges these cards represent for formal verication of software. Smart card trends Increasingly, physical...
Factorization systems and brations: Toward a bred Birkho variety theorem (2007)
It is well-known that a factorization system on a category (with sucient pullbacks) gives rise to a bration. This paper characterizes the brations that arise in such a way, by making precise the...
CTCS 2002 Preliminary Version Factorization systems and fibrations: Toward a (2007)
It is well-known that a factorization system on a category (with su#cient pullbacks) gives rise to a fibration. This paper characterizes the fibrations that arise in such a way, by making precise the...
Assertional and Behavioural Renement (2007)
Bart Jacobs, Hendrik Tews, Tu Dresden
Re nements between specications in a coalgebraic setting have been introduced in [13,14]. This paper presents a renewed, extended study of renements, based on more practical experience. It...
JavaCard's Application Identier Class (2007)
E. Poll, Bart Jacobs, Erik Poll
Formal Specication and Verication of
PMD '01 Precise Modelling and Deduction for Object-oriented Software Development (2007)
Bernhard Beckert, Bart Jacobs, Johann Schumann, Jon Whittle
(eds.)
On the Role of Invariants in Reasoning about Object-Oriented Languages (2007)
Cees-Bart Breunesse, Bart Jacobs, Erik Poll
The aim of this paper is to clarify the di#erent roles that class invariants play in the verification of object-oriented programs, namely in method specifications as proof obligations for method...
This paper reports on an eort to increase the reliability of JavaCard-based smart cards by means of formal speci cation and veri cation of JavaCard source code. As a rst step, lightweight formal...
Gary T. Leavens, Joint Yoonsik Cheon, Curt Clifton, Clyde Ruby, Arun Raghavan, ...
much easier to maintain than code .Rigorous semantics: can use for verification Approach .Java expressions for assertions ( la Eiffel) .Model-based specifications (Larch, VDM) Contribution .Language...
Formal Proofs of Confidentiality in Java Pograms (2007)
In this paper we introduce two new ways of establishing confidentiality for sequential Java source code. The first one uses a functional formulation of confidentiality, in what we call a...
A Type-Theoretic Memory Model for (2007)
Veri Cation Of, Marieke Huisman, Bart Jacobs, Erik Poll
This paper explains the details of the memory model underlying the veri cation of sequential Java programs in the framework of the \LOOP" project ([13,18]). The building blocks of this memory...
Generic Trace Semantics via Coinduction (2007)
Hasuo, Ichiro, Jacobs, Bart, Sokolova, Ana
Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to identify one...
Noirhomme, Mathieu, Meessen, Bruno, Griffiths, Fred, Ir, Por, Jacobs, Bart, Thor, Rasoka, ...
There is a large body of evidence that user fees in the health sector create exclusion. Health equity funds attempt to improve access to health care services for the poorest by paying the provider on...
A statically verifiable programming model for concurrent object-oriented programs (2007)
Vele kritische computerprogramma's, met hoge betrouwbaarheidsvereisten, zijn gelijktijdig (m.a.w., de volgorde van de bewerkingen is niet volledig gespecificeerd) en zijn geschreven in op gedeeld...
Biometrics and their use in e-passports (2007)
A succesful design, deployment and operation of biometric systems depends highly on the results for existing biometrical technologies and components. These existing technologies as well as new...
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Abstract. Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe that the same algebraic theory is...
URL:http://www.cs.ru.nl/B.Jacobs (2007)
This paper presents a sound BAN-like logic for reasoning about security protocols with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and...
Specification and verification of the Nova (2007)
Hendrik Tews, Bart Jacobs, Erik Poll, Marko Eekelen, Peter Rossum
microhypervisor Short note on the selected approach and how it is applied during the specification of some selected modules of the microhypervisor source code (Robin deliverable D.6)
Specification and verification of the Nova (2007)
Hendrik Tews, Bart Jacobs, Erik Poll, Marko Eekelen, Peter Rossum
microhypervisor Short note on the selected approach and how it is applied during the specification of some selected modules of the microhypervisor source code (Robin deliverable D.6)
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Abstract. Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe that the same algebraic theory is...
Increased security through open source (2007)
Jaap-henk Hoepman, Bart Jacobs
The last few years have shown a worldwide rise in the attention for, and ac-tual use of, open source software (OSS), most notably of the operating system
Increased security through open source (2007)
Jaap-henk Hoepman, Bart Jacobs
1 Introduction The last few years have shown a worldwide rise in the attention for, and actual use of, open source software (OSS), most notably of the operating system Linux and various applications...
Generic trace semantics via coinduction (2007)
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Abstract. Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to...
A Statically Verifiable Programming Model for Concurrent (2007)
Departement Computerwetenschappen, Prof Dr, F. Piessens, Prof Dr, E. Steegmans, Bart Jacobs, ...
Proefschrift voorgedragen tot het behalen van het doctoraat in de ingenieurswetenschappen door
Static verification of Code Access Security policy compliance of .NET applications (2006)
Jan Smans, Bart Jacobs, Frank Piessens
Stack inspection-based sandboxing originated as a security mechanism for safely executing partially trusted code. Today, it is widely used for the more general purpose of supporting the principle of...
Crossing borders: Security and privacy issues of the european e-passport (2006)
Jaap-henk Hoepman, Engelbert Hubbers, Bart Jacobs, Martijn Oostdijk, Ronny Wichers Schreur
Abstract. The first generation of European e-passports will be issued in 2006. We discuss how borders are crossed regarding the security and privacy erosion of the proposed schemes, and show which...
Verification of programs with inspector methods (2006)
Abstract. Most classes in an object-oriented program provide access to an object’s state through methods, so that client code does not depend on and cannot interfere with the object’s internal...
A statically verifiable programming model for concurrent object-oriented programs (2006)
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte
Abstract. Reasoning about multithreaded object-oriented programs is difficult, due to the non-local nature of object aliasing, data races, and deadlocks. We propose a programming model that prevents...
Boogie: A modular reusable verifier for object-oriented programs (2006)
Mike Barnett, Robert Deline, Bart Jacobs, K. Rustanm. Leino
Abstract. A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user...
Boogie: A modular reusable verifier for object-oriented programs (2006)
Mike Barnett, Robert Deline, Bart Jacobs, K. Rustan, M. Leino
Abstract. A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user...
Boogie: A modular reusable verifier for object-oriented programs (2006)
Mike Barnett, Robert Deline, Bart Jacobs, K. Rustan, M. Leino
Abstract. A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user...
Static verification of Code Access Security policy compliance of .NET applications (2006)
The base class library of the.NET Framework makes extensive use of the Code Access Security system to ensure that partially trusted code can be executed securely. Imperative or declarative permission...
Freyd is Kleisli, for arrows (2006)
Arrows have been introduced in functional programming as generalisations of monads. They also generalise comonads. Fundamental structures associated with (co)monads are Kleisli categories and...
Crossing borders: Security and privacy issues of the european e-passport (2006)
Jaap-henk Hoepman, Engelbert Hubbers, Bart Jacobs, Martijn Oostdijk, Ronny Wichers Schreur
Abstract. The first generation of European e-passports will be issued in 2006. We discuss how borders are crossed regarding the security and privacy erosion of the proposed schemes, and show which...
Arrows, like monads, are monoids (2006)
Monads are by now well-established as programming construct in functional languages. Recently, the notion of “Arrow ” was introduced by Hughes as an extension, not with one, but with two type...
Crossing borders: Security and privacy issues of the european e-passport (2006)
Jaap-henk Hoepman, Engelbert Hubbers, Bart Jacobs, Martijn Oostdijk, Ronny Wichers Schreur
Abstract. The first generation of European e-passports will be issued in 2006. We discuss how borders are crossed regarding the security and privacy erosion of the proposed schemes, and show which...
Safe Fine-Grained Locking for Aggregate Objects (2006)
Bart Jacobs, Frank Piessens, Wolfram Schulte, Ò Katholieke, Bart Jacobs, Frank Piessens, ...
Programmers have difficulty writing correct multithreaded code, not to mention code that scales well. One way to approach this problem is by offering a transaction construct, and leaving it to the...
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism ” such as classical non-determinism (with a...
Freyd is Kleisli, for arrows (2006)
Arrows have been introduced in functional programming as generalisations of monads. They also generalise comonads. Fundamental structures associated with (co)monads are Kleisli categories and...
This article presents research findings into the effectiveness of an innovative equity fund approach to improving access to public sector health services for the poor in Kirivong Operational Health...
Context-free languages via coalgebraic trace semantics (2005)
Abstract. We show that, for functors with suitable mild restrictions, the initial algebra in the category of sets and functions gives rise to the final coalgebra in the (Kleisli) category of sets and...
Safe Concurrency for Aggregate Objects with Invariants (2005)
Bart Jacobs Rustan, Bart Jacobs, K. Rustan, M. Leino, Frank Piessens, Wolfram Schulte
Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a flexible methodology for object-oriented...
The Spec# Programming System: Challenges and Directions. Position paper at VSTTE (2005)
Mike Barnett, Robert Deline, Bart Jacobs, Manuel Fähndrich, K. Rustan, M. Leino, ...
The Spec # programming system [2] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer...
The Spec# Programming System: Challenges and Directions. Position paper at VSTTE (2005)
Mike Barnett, Robert Deline, Bart Jacobs, Manuel Fähndrich, K. Rustan, M. Leino, ...
The Spec # programming system [2] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer...
RIES: Internet voting in action (2005)
Engelbert Hubbers, Bart Jacobs, Wolter Pieters
Abstract. RIES stands for Rijnland Internet Election System. It is an online voting system that was developed by one of the Dutch local authorities on water management. The system has been used twice...
AHA Amortized Heap Space Usage Analysis (2005)
Marko Van Eekelen, Bart Jacobs, Erik Poll, Sjaak Smetsers
project involves research into an amortized analysis of heap-space usage by functional and imperative programs. Estimating heap consumption is an active research area since it becomes more and more...
Coalgebraic trace semantics for probabilistic systems (2005)
Introduction The authors introduced in [1] the technique of coalgebraic trace semantics for the powerset monad P. There the initial F-algebra α: F A ∼ = → A
RIES: Internet voting in action (2005)
Engelbert Hubbers, Bart Jacobs, Wolter Pieters
RIES stands for Rijnland Internet Election System. It is an online voting system that has been used twice in the fall of 2004 for in total over two million potential voters. In this paper we describe...
program verifier. Verifying Programs Using Inspector Methods for State Abstraction (2005)
Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens
Most classes in an object-oriented program provide access to an object’s state through methods, so that client code does not depend on and cannot interfere with the object’s internal...
This article presents research findings into the effectiveness of an innovative equity fund approach to improving access to public sector health services for the poor in Kirivong Operational Health...
Towards integrated AlGaN/GaN based X-band high-power amplifiers (2004)
Doctoral degree 05-07-2004; Department of Electrical Engineering; Supervisors: L.M.F. Kaufmann and E. Kohn
Lieven Desmet, Bart Jacobs, Frank Piessens, Wouter Joosen
Abstract: In order to perform a useful threat analysis of a web application platform, some architectural assumptions about such applications must be made. This document describes a generic...
Threat Modelling for web services based web applications (2004)
Lieven Desmet, Bart Jacobs, Frank Piessens, Wouter Joosen
Abstract: Threat analysis of a web application can lead to a wide variety of identified threats. Some of these threats will be very specific to the application; others will be more related to the...
Support for metadata-driven selection of run-time services in .NET is promising but immature (2004)
Frank Piessens, Bart Jacobs, Eddy Truyen, Wouter Joosen
The.NET Framework allows developers to add run-time services to their classes by specifying them in metadata. This metadata-driven service selection is a very powerful and promising mechanism,...
Verification of multithreaded object-oriented programs with invariants (2004)
Bart Jacobs, K. Rustan, M. Leino
Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...
Leavens JML Framed! 3 Behavioral Interface Specification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Rustan Leino, Bart Jacobs, Erik Poll, ...
Behavioral interface specification language, tailored to Java • Records detailed designs • Pre- and postconditions, invariants,... • Synthesizes ideas in sequential specification
Source Code Verification of a Secure Payment Applet (2004)
Bart Jacobs, Martijn Oostdijk, Martijn Warnier
This paper discusses a case study in formal verification and development of secure smart card applications. An elementary Java Card electronic purse applet is presented whose specification can be...
Relating Two Approaches to Coinductive Solution of Recursive Equations (2004)
This paper shows that the approach of [2,12] for obtaining coinductive solutions of equations on infinite terms is a special case of a more general recent approach of [4] using distributive laws.
Software Security through Open Source (2004)
Jaap-henk Hoepman, Bart Jacobs
this paper. The following analogies may help to introduce the issues and controversies surrounding the open source debate
Semantics and logic for security protocols (2004)
This paper presents a sound BAN-like logic for reasoning about security protocols with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and...
Verification of multithreaded object-oriented programs with invariants (2004)
Bart Jacobs, K. Rustan, M. Leino
Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...
Verification of multithreaded object-oriented programs with invariants (2004)
Bart Jacobs, K. Rustan, M. Leino
Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...
Semantics and logic for security protocols (2004)
This paper presents a sound BAN-like logic for reasoning about security protocols with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and...
The impact of the introduction of user fees at a district hospital in Cambodia (2004)
Proponents of user fees in the health sector in poor countries cite a number of often interrelated rationales, relating inter alia to cost recovery, improved equity and greater efficiency. Opponents...
Simulations in coalgebra (2003)
A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building block for a "lax...
Java’s integral types in pvs (2003)
Abstract. This paper extends PVS's standard bitvector library with multiplication, division and remainder operations, together with associated results. This extension is needed to give...
Coalgebras and monads in the semantics of Java (2003)
This paper describes the basic structures in the denotational and axiomatic semantics of sequential Java, both from a monadic and a coalgebraic perspective. This semantics is an abstraction of the...
Java Program Verification at Nijmegen: Developments and Perspective (2003)
This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997--2003). It describes the development...
Java Program Verification Challenges (2003)
J. R. Kiniry, M.E. Warnier, Bart Jacobs, Joseph Kiniry, Martijn Warnier
This paper aims to raise the level of verification challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on the...
Java Program Verification at Nijmegen: Developments and Perspective (2003)
E. Poll, Bart Jacobs, Erik Poll
This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997--2003). It describes the development...
A π-Calculus Semantics of Java: The Full Definition (2003)
We present a formal semantics of the concurrent objectoriented programming language Java, as a mapping of Java programs to #-calculus processes. Our semantics shows how Java features such as...
Frank Piessens, Bart Jacobs, Wouter Joosen
As more and more software applications are directly or indirectly accessible from the Internet, the importance of the security of these applications grows steadily. Hence, it is important that...
Java program verification at nijmegen: Developments and perspective (2003)
Abstract. This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997–2003). It describes the...
Java program verification at nijmegen: Developments and perspective (2003)
E. Poll, Bart Jacobs, Erik Poll
Abstract. This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997–2003). It describes the...
Trace Semantics for Coalgebras (2003)
Traditionally, traces are the sequences of labels associated with paths in transition systems X # P(A X).
Bart Jacobs, Frank Piessens, Bart Jacobs, Frank Piessens
Abstract We present a formal semantics of the concurrent object-orientedprogramming language Java, as a mapping of Java programs to ss-calculus processes. Our semantics shows how Java features such...
Community participation in externally funded health projects: lessons from Cambodia (2003)
This article provides lessons learned on establishing effective community participation in two externally funded, NGO-implemented health projects working at district level in Cambodia. The first...
Specifying and verifying a decimal representation in Java for smart cards (2002)
Cees-bart Breunesse, Bart Jacobs
Abstract. This article describes a case study concerning a component of a Java Purse applet developed by the smart card manufacturer Gemplus. This component is a representation of decimal numbers in...
Voting using Java Card smart cards: A case study (2002)
Cees-Bart Breunesse, Bart Jacobs, Martijn Oostdijk
This paper documents a case study in the development of a Java Card application and describes some related security issues. An implementation of a simpli ed electronic voting system is presented, in...
Specifying and verifying a decimal representation in Java for smart cards (2002)
Cees-bart Breunesse, Bart Jacobs
Abstract. This article describes a case study concerning a component of a Java Purse applet developed by the smart card manufacturer Gemplus. This component is a representation of decimal numbers in...
Aan de universiteiten van Twente en Nijmegen zijn twee onderzoeksgroepen onder leiding van de auteurs intensief bezig met smartcards. Beide auteurs zijn eerder dit jaar betrokken geweest bij het...
A logic for the Java Modeling Language JML (2001)
fbart,erikpollg Abstract. This paper describes a specialised logic for proving speci-cations in the Java Modeling Language (JML). JML is an interface speci cation language for Java. It allows...
A formalisation of Java's exception mechanism (2001)
bart Abstract. This paper examines Java's exception mechanism, and formalises its main operations (throw, try-catch and try-catch-finally) in a type-theoretic setting. This formalisation uses...
The LOOP compiler for Java and JML (2001)
Abstract This paper describes the architecture of the loop tool, which is used for reasoning about sequential Java. The loop tool translates Java and JML (a specication language tailored to Java)...
A logic for the Java Modeling Language JML (2001)
fbart,erikpollg Abstract. This paper describes a specialised logic for proving speci-cations in the Java Modeling Language (JML). JML is an interface speci cation language for Java. It allows...
The LOOP compiler for Java and JML (2001)
Abstract This paper describes the architecture of the loop tool, which is used for reasoning about sequential Java. The loop tool translates Java and JML (a specication language tailored to Java)...
A logic for the Java Modeling Language JML (2001)
Abstract. This paper describes a specialised logic for proving specifications in the Java Modeling Language (JML). JML is an interface specification language for Java. It allows assertions like...
JML: notations and tools supporting detailed design in Java (2000)
Gary T. Leavens, K. Rustan, M. Leino, Erik Poll, Clyde Ruby, Bart Jacobs, ...
2000 ACM. Permission to make digital or hard copies of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial...
Sophia Antipolis, Sophia Drossopoulou, Susan Eisenbach, Bart Jacobs, Gary T. Leavens, I. Attali, ...
Formal Specification and Verification of JavaCard's Application Identifier Class (2000)
This paper discusses a verification in PVS of the AID (Application Identifier) class from the JavaCard API. The properties that are verified are formulated in the interface specification language...
A monad for basic Java semantics (2000)
fbart, erikpollg Abstract This paper describes the role of a computational monad in the denotational semantics of sequential Java and investigates some of its properties. This denotational semantics...
Inheritance in higher order logic: Modeling and reasoning (2000)
Abstract. This paper describes a way of modeling inheritance (in objectoriented programming languages) in higher order logic. This particular approach is used in the loop project for reasoning about...
Java Program Verification via a Hoare Logic with Abrupt Termination (2000)
This paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an...
The Coalgebraic Class Specification Language CCSL (2000)
Jan Rothe, Hendrik Tews, Bart Jacobs
. This note presents the Coalgebraic Class Specification Language CCSL that is developed within the LOOP project 1 . CCSL allows the (coalgebraic) specification of behavioral types or classes from...
A Monad for Basic Java Semantics (2000)
This paper describes the role of a computational monad in the denotational semantics of sequential Java and investigates some of its properties. This denotational semantics is an abstraction of the...
Inheritance in Higher Order Logic: Modeling and Reasoning (2000)
This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the loop project for reasoning about java...
JML: notations and tools supporting detailed design in Java (2000)
Gary T. Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby, K. Rustan, ...
JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it...
Inheritance in Higher Order Logic: Modeling and Reasoning (2000)
Marieke Huisman Bart, Bart Jacobs
. This paper describes a way of modeling inheritance (in objectoriented programming languages) in higher order logic. This particular approach is used in the loop project for reasoning about java...
The Coalgebraic Class Specification Language CCSL (2000)
Jan Rothe, Hendrik Tews, Bart Jacobs
This paper presents the Coalgebraic Class Speci cation Language CCSL that is developed within the loop project on formal methods for object-oriented languages. CCSL allows the (coalgebraic)...
A Monad for Basic Java Semantics (2000)
This paper describes the r^ole of a computational monad in the denotational semantics of sequential Java and investigates some of its properties. This denotational semantics is an abstraction of the...
Cation And Veri, Bart Jacobs, Erik Poll
This paper discusses a veri cation in PVS of the AID (Application Identi er) class from the JavaCard API. The properties that are veri ed are formulated in the interface speci cation language JML....
Towards a Duality Result in the Modal Logic of Coalgebras (2000)
This paper forms a step in the development of the recently emerged connection between coalgebra and modal logic. It introduces (back-and-forth) transformations between coalgebras of simple polynomial...
Formal Specification and Verification of JavaCard's Application Identifier Class (2000)
This note discusses a verication in PVS of the AID (Application Identier) class from JavaCard's API. The properties that are veried are formulated in the interface specication language JML. This...
First steps in formalising JML: Exceptions in Predicates (2000)
This note describes the rst steps toward a rigorous formal semantics of JML speci cations for Java. This semantics is developed within the framework of the LOOP project [5,11]. JML speci cations...
System Design as a Creative Mathematical Activity (1999)
Hanno Wupper, Angelika Mader, Bart Jacobs, Hans Meijer, Frits Va
This paper contributes to the understanding of rational systems design and verification. We give evidence that the rôle of mathematics in development and verification is not limited to useful...
A Type-Theoretic Memory Model for Verification of Sequential Java Programs (1999)
Marieke Huisman, Bart Jacobs, Erik Poll
This paper explains the details of the memory model underlying the verification of sequential Java programs in the "LOOP" project ([14, 20]). The building blocks of this memory are cells,...
Exercises in Coalgebraic Specification (1999)
An introduction to coalgebraic specification is presented via examples. A coalgebraic specification describes a collection of coalgebras satisfying certain assertions. It is thus an axiomatic...
A Case Study in Class Library Verification: Java's Vector Class (1999)
) Marieke Huisman, Bart Jacobs, Joachim van den Berg Computing Science Institute, University of Nijmegen Toernooiveld 1, 6525 ED Nijmegen, The Netherlands fmarieke,bart,joachimg@cs.kun.nl Abstract....
The Temporal Logic of Coalgebras via Galois Algebras (1999)
This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are dened for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois...
A Type-Theoretic Memory Model for Verification of Sequential Java Programs (1999)
Marieke Huisman, Bart Jacobs, Erik Poll
This paper explains the details of the memory model underlying the verification of sequential Java programs in the framework of the "LOOP" project ([13, 18]). The building blocks of this...
Coalgebras in Specification and Verification for Object-Oriented Languages (1999)
The aim of this short note is to give an impression of the use of coalgebras in specification and verification for object-oriented languages. Particular emphasis will be given to the rôle of...
Feasibility of hospital-based blood banking: a Tanzanian case study (1999)
The demand for blood transfusion is high in sub-Saharan Africa because of the high prevalence of anaemia and pregnancy related complications, but the practice is estimated to account for 10%...
Reasoning about Java classes (1998)
Bart Jacobs, Marieke Huisman, Martijn Van Berkum, Ulrich Hensel, Hendrik Tews
We present the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our...
Coalgebraic Theories of Sequences in PVS (1998)
This paper explains the setting of an extensive formalisation of the theory of sequences (finite and infinite lists of elements of some data type) in the Prototype Verification System pvs. This...
Coalgebraic Reasoning about Classes in Object-Oriented Languages (1998)
This note briefly discusses how some of the ideas developed in the theory of coalgebras are used in a front-end tool called LOOP, developed jointly in Dresden and Nijmegen, for reasoning (with a...
Reasoning about Java Classes (1998)
Bart Jacobs, Marieke Huisman, Martijn Van Berkum, Ulrich Hensel, Hendrik Tews, ...
We present the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our...
Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools (1998)
Ulrich Hensel, Marieke Huisman, Bart Jacobs, Hendrik Tews, Inst Theor Informatik, Tu Dresden, ...
. A formal language ccsl is introduced for describing specifications of classes in object-oriented languages. We show how class specifications in ccsl can be translated into higher order logic. This...
Structural Induction and Coinduction in a Fibrational Setting (1997)
. We present a categorical logic formulation of induction and coinduction principles for reasoning about inductively and coinductively defined types. Our main results provide sufficient criteria for...
A Tutorial on (Co)Algebras and (Co)Induction (1997)
. Algebraic structures which are generated by a collection of constructors--- like natural numbers (generated by a zero and a successor) or finite lists and trees--- are of well-established...
Invariants, Bisimulations and the Correctness of Coalgebraic Refinements (1997)
. Coalgebraic specifications are used to formally describe the behaviour of classes in object-oriented languages. In this paper, a general notion of refinement between two such coalgebraic...
Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs (1997)
. A notion of refinement is defined in the context of coalgebraic specification of classes in object-oriented languages. It tells us when objects in a "concrete" class behave exactly like...
Proof Principles for Datatypes with Iterated Recursion (1997)
. Data types like trees which are finitely branching and of (possibly) infinite depth are described by iterating initial algebras and terminal coalgebras. We study proof principles for such data...
Proof Principles for Datatypes with Iterated Recursion (1997)
. Data types like trees which are finitely branching and of (possibly) infinite depth are described by iterating initial algebras and terminal coalgebras. We study proof principles for such data...
Coalgebraic Theories of Sequences in PVS (1997)
This paper explains the setting of an extensive formalisation of the theory of sequences (finite and infinite lists of elements of some data type) in the Prototype Verification System pvs. This...
Coalgebraic specifications and models of deterministic hybrid systems (1996)
Abstract. Coalgebraic specification and semantics, as used earlier for object-oriented programming, is extended with temporal aspects. The (non-temporal) expression s:meth expressing that method meth...
Objects and classes, co-algebraically (1996)
B. Jacobs, Issn -x, Bart Jacobs
for promotion of mathematics and computer science and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Coalgebraic Specifications and Models of Deterministic Hybrid Systems (1996)
Coalgebraic specification and semantics, as used earlier for object-oriented programming, is extended with temporal aspects. The (non-temporal) expression s:meth expressing that method meth is...
Automata and Behaviours in Categories of Processes (1996)
An early result of Goguen [4, 5] describes the fundamental adjunction between categories of deterministic automata and their behaviours. Our first step is to redefine (morphisms in) these categories...
Relating Models of Impredicative Type Theories (1996)
Bart Jacobs, Eugenio Moggi, Thomas Streicher, Nl. Genova, I. Passau
The object of study of this paper is the categorical semantics of three impredicative type theories, viz. Higher Order -calculus F!, the Calculus of Constructions and Higher Order ML. The latter is...
Inheritance and Cofree Constructions (1996)
. The coalgebraic view on classes and objects is elaborated to include inheritance. Inheritance in coalgebraic specification (of classes) will be understood dually to parametrization in algebraic...
Structural Induction and Coinduction in a Fibrational Setting (1996)
. We present a categorical logic formulation of induction and coinduction principles for reasoning about inductively and coinductively defined types. Our main results provide sufficient criteria for...
Object-Oriented Hybrid Systems of Coalgebras plus Monoid Actions (1996)
. Hybrid systems combine discrete and continuous dynamics. We introduce a semantics for such systems consisting of a coalgebra together with a monoid action. The coalgebra captures the (discrete)...
Objects And Classes, Co-Algebraically (1996)
The co-algebraic perspective on objects and classes in object-oriented programming is elaborated: classes are described as co-algebras, which may occur as models (implementations) of co-algebraic...
On the sensitivity of solution components in linear systems of equations (1995)
bart The notion of an endofunctor having "greatest subcoalgebras " is introduced as a form of proof of the existence of limits for coalgebras---proved earlier by Worrell and by Gumm...
Duality beyond Sober Spaces: Topological Spaces and Observation Frames (1995)
Marcello Bonsangue, Bart Jacobs, Joost Kok
We introduce observation frames as an extension of ordinary frames. The aim is to give an abstract representation of a mapping from observable predicates to all predicates of a specific system. A...
Inheritance and Cofree Constructions (1995)
The coalgebraic view on classes and objects is elaborated to include inheritance. Inheritance in coalgebraic specification (of classes) will be understood dually to parametrization in algebraic...
Bisimulation and Apartness in Coalgebraic Specification (1995)
. A first basic fact in algebra (or, in algebraic specification) is the existence of free algebras, as suitable sets of terms. In coalgebraic specification, terminal coalgebras are known to exist in...
Mongruences and Cofree Coalgebras (1995)
. A coalgebra is introduced here as a model of a certain signature consisting of a type X with various "destructor" function symbols, satisfying certain equations. These destructor function...
Duality beyond Sober Spaces: Topological Spaces and Observation Frames (1995)
Marcello Bonsangue, Bart Jacobs, Joost N. Kok
We introduce observation frames as an extension of ordinary frames. The aim is to give an abstract representation of a mapping from observable predicates to all predicates of a specific system. A...
Quotients in Simple Type Theory (1994)
Introduction Quotients are used throughout mathematics for constructing new objects from old, by collapsing part of the structure, see for example any textbook on algebra or topology. Here we give a...
An Algebraic View of Structural Induction (1994)
We propose a uniform, category-theoretic account of structural induction for inductively defined data types. The account is based on the understanding of inductively defined data types as initial...
Coalgebras and Approximation (1994)
. Motivated by a new approach in the categorical semantics of linear logic, we investigate some specific categories of coalgebras. They all arise from the canonical comonad that one has on a category...
Translating Dependent Type Theory into Higher Order Logic (1993)
Bart Jacobs And, Bart Jacobs, Tom Melham
. This paper describes a translation of the complex calculus of dependent type theory into the relatively simpler higher order logic originally introduced by Church. In particular, it shows how type...
Translating Dependent Type Theory into Higher Order Logic (1993)
. This paper describes a translation of the complex calculus of dependent type theory into the relatively simpler higher order logic originally introduced by Church. In particular, it shows how type...
Categorical Typ e Theory (1991)
Phd Thesis Of, Bart Jacobs, Afdeling Wiskunde
wledgemen ts The first to be men tioned here is Henk Barendregt. He pro vided an atmosphere with the righ tcom bination of intellectual freedom and stim ulation, for this work to emerge. The years in...
Prof Dr, Bart Jacobs, Abunyang Emmanuel
The cost of delivering financial services in both developing and developed countries has always been an aspect of concern to financial institutions. Financial institutions incur exorbitant operating...