The Stability Problem for Verification of Concurrent Object-Oriented Programs (2008)
Marieke Huisman, Clément Hurlin
Modular static verification of concurrent object-oriented programs remains a challenge. This paper discusses the impact of concurrency on the use and meaning of behavioural specifications, and in...
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
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
Formal Techniques for Java-like Programs (FTfJP) (2008)
Ro Coglio, Marieke Huisman, Joseph R. Kiniry, Peter Müller, Erik Poll
Abstract. This report gives an overview of the sixth Workshop on Formal
Reasoning about Java's reentrant locks (2008)
Haack, Christian, Huisman, Marieke, Hurlin, Clément
This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each...
Reasoning about Java's reentrant locks (2008)
Haack, Christian, Huisman, Marieke, Hurlin, Clément
This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each...
method declarations . . . . . . . . . . . . . . . . . . . . . . . . . 34 Chapter 4. Processing 35 4.1 Compiler pass . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35...
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...
Formal specication of Gemplus ' electronic purse case study (2007)
Nestor Cata~no Collazos, Marieke Huisman
Abstract. This paper presents a case study in formal specication of smart card programs, using ESC/Java. It discusses an electronic purse application, provided by Gemplus, that we have annotated with...
Formal specication and static checking of Gemplus ' electronic purse using ESC/Java (2007)
Abstract. This paper presents a case study in formal specication of smart card programs, using ESC/Java. It discusses an electronic purse application, provided by Gemplus, that we have annotated with...
Verication of Java's AbstractCollection class: a case study (2007)
Abstract. This paper presents a case study that is done in the context of the loop project in Nijmegen. A functional behaviour specication of the class AbstractCollection from java's standard...
Gilles Barthe, Dilian Gurov, Marieke Huisman
Compositional specication and verication of control AEow based security properties of multi-application programs
Simulation Logic, Applets and Compositional Verification (2007)
Christoph Sprenger, Dilian Gurov, Marieke Huisman, Inria Sophia Antipolis, Inria Sophia Antipolis, Sophia Antipolis, ...
We present a compositional verication method for control ow based safety properties of smart card applets. Our method rests on a close correspondence between transition system models ordered by...
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...
Permission Specifications for Common Multithreaded Programming Patterns (2007)
Huisman, Marieke, Hurlin, Clément
Multithreading is the next challenge for program verification. To support modular verification of multithreaded programs, one should know when data might be accessed or updated by the different...
The stability problem for verification of concurrent object-oriented programs (2007)
Huisman, Marieke, Hurlin, Clément
Modular static verification of concurrent object-oriented programs remains a challenge. This paper discusses the impact of concurrency on the use and meaning of behavioural specifications, and in...
Permission Specifications for Common Multithreaded Programming Patterns (2007)
Huisman, Marieke, Hurlin, Clément
Multithreading is the next challenge for program verification. To support modular verification of multithreaded programs, one should know when data might be accessed or updated by the different...
The stability problem for verification of concurrent object-oriented programs (2007)
Huisman, Marieke, Hurlin, Clément
Modular static verification of concurrent object-oriented programs remains a challenge. This paper discusses the impact of concurrency on the use and meaning of behavioural specifications, and in...
Factorising Temporal Specifications (2005)
Marieke Huisman, Kerry Trentelman
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that...
Verification of Liveness Properties with JML (2004)
Bellegarde, Françoise, Groslambert, Julien, Huisman, Marieke, Julliand, Jacques, Kouchnarenko, Olga
This paper proposes a way to verify liveness properties in an extension of JML. The verification is divided into two subtasks: (1) generation of appropriate JML annotations that allow to verify that...
Abstraction over Public Interfaces (2004)
Gurov, Dilian, Huisman, Marieke
The use of public interfaces as a means of encapsulating method implementations has become standard in software design, but still requires the development of appropriate verification techniques. In...
Factorising temporal specifications (2004)
Huisman, Marieke, Trentelman, Kerry
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that...
Verification of Liveness Properties with JML (2004)
Bellegarde, Françoise, Groslambert, Julien, Huisman, Marieke, Julliand, Jacques, Kouchnarenko, Olga
This paper proposes a way to verify liveness properties in an extension of JML. The verification is divided into two subtasks: (1) generation of appropriate JML annotations that allow to verify that...
Abstraction over Public Interfaces (2004)
Gurov, Dilian, Huisman, Marieke
The use of public interfaces as a means of encapsulating method implementations has become standard in software design, but still requires the development of appropriate verification techniques. In...
Factorising temporal specifications (2004)
Huisman, Marieke, Trentelman, Kerry
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that...
Verification of Liveness Properties with JML (2004)
Bellegarde, Françoise, Groslambert, Julien, Huisman, Marieke, Julliand, Jacques, Kouchnarenko, Olga
This paper proposes a way to verify liveness properties in an extension of JML. The verification is divided into two subtasks: (1) generation of appropriate JML annotations that allow to verify that...
Abstraction over Public Interfaces (2004)
Gurov, Dilian, Huisman, Marieke
The use of public interfaces as a means of encapsulating method implementations has become standard in software design, but still requires the development of appropriate verification techniques. In...
Factorising temporal specifications (2004)
Huisman, Marieke, Trentelman, Kerry
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that...
Enforcing high-level security properties for applets (2004)
Mariela Pavlova, Mariela Pavlova, Gilles Barthe, Gilles Barthe, Lilian Burdy, Lilian Burdy, ...
apport de recherche
Compositional Verification for Secure Loading of Smart Card Applets (2004)
Christoph Sprenger, Dilian Gurov, Marieke Huisman
We present an algorithmic compositional verification method for smart card applets and control flow based safety properties expressed in a modal logic with simultaneous greatest fixed points. Our...
Enforcing High-Level Security Properties for Applets (2004)
Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-louis Lanet
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties,...
Enforcing High-Level Security Properties for Applets (2004)
Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-louis Lanet
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties,...
Enforcing High-Level Security Properties For Applets (2003)
Pavlova, Mariela, Huisman, Marieke, Lanet, Jean-Louis
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Such policies are usually described by high-level security properties, stating...
Simulation Logic, Applets and Compositional Verification (2003)
Sprenger, Christoph, Gurov, Dilian, Huisman, Marieke
We present a compositional verification method for control flow based safety properties of smart card applets. Our method rests on a close correspondence between transition system models ordered by...
Enforcing High-Level Security Properties For Applets (2003)
Pavlova, Mariela, Huisman, Marieke, Lanet, Jean-Louis
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Such policies are usually described by high-level security properties, stating...
Simulation Logic, Applets and Compositional Verification (2003)
Sprenger, Christoph, Gurov, Dilian, Huisman, Marieke
We present a compositional verification method for control flow based safety properties of smart card applets. Our method rests on a close correspondence between transition system models ordered by...
Enforcing High-Level Security Properties For Applets (2003)
Pavlova, Mariela, Huisman, Marieke, Lanet, Jean-Louis
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Such policies are usually described by high-level security properties, stating...
Simulation Logic, Applets and Compositional Verification (2003)
Sprenger, Christoph, Gurov, Dilian, Huisman, Marieke
We present a compositional verification method for control flow based safety properties of smart card applets. Our method rests on a close correspondence between transition system models ordered by...
Chase: a static checker for JML’s assignable clause (2003)
Abstract. This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their...
Checking absence of illicit applet interactions: a case study (2003)
Marieke Huisman, Dilian Gurov, Christoph Sprenger, Gennady Chugunov
Abstract. This paper presents the use of a method and its corresponding tool set for compositional verication of applet interactions on a realistic industrial smart card case study. The case study,...
Simulation logic, applets and compositional verication (2003)
Christoph Sprenger, Christoph Sprenger, Dilian Gurov, Dilian Gurov, Marieke Huisman, Marieke Huisman
apport de recherche
Checking absence of illicit applet interactions: a case study (2003)
Marieke Huisman, Dilian Gurov, Christoph Sprenger, Gennady Chugunov
Abstract This paper presents the use of a method and its corresponding tool set for compositional verication of applet interactions on a realistic industrial smart card case study. The case study, an...
Compositional verication of secure applet interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Abstract. Recent developments in mobile code and embedded systems have lead to an increased interest in open platforms, i.e. platforms which enable dierent applications to interact in a dynamic...
Extending JML Specifications with Temporal Logic (2002)
Kerry Trentelman, Marieke Huisman
This paper proposes an extension of the Java Modeling Language (JML) with temporal specifications. The extension is inspired by the patterns and specification language used within the Bandera...
Extending JML specifications with temporal logic (2002)
Kerry Trentelman, Marieke Huisman
Abstract. This paper proposes an extension of the Java Modeling Language (JML) with temporal specifications. The extension is inspired by the patterns and specification language used within the...
Compositional verification of secure applet interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Abstract. Recent developments in mobile code and embedded systems have lead to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic...
Compositional Verification of Secure Applet Interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment....
Reasoning about Java programs in higher order logic using PVS and Isabelle (2001)
This thesis describes the first steps of a project aimed at formal verification of Java programs. The work presented here is part of a larger project called LOOP, for Logic of Object Oriented...
Modular Specification of Frame Properties in JML (2001)
Kees Huizing, Ruurd Kuiper, Davide Ancona, Giovanni Lagorio, ...
Program Committee:
Barthe, Gilles, Gurov, Dilian, Huisman, Marieke
The paper presents a compositional program model of multi-application programs and sketches a framework for compositional specification and verification of temporal properties of such programs.
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...
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...
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,...
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....
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...
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...
A comparison of PVS and Isabelle/HOL (1998)
David Griffioen, Marieke Huisman
Abstract. There is an overwhelming number of different proof tools available and it is hard to find the right one for a particular application. Manuals usually concentrate on the strong points of 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...
A Comparison of PVS and Isabelle/HOL (1998)
David Griffioen, Marieke Huisman
. There is an overwhelming number of different proof tools available and it is hard to find the right one for a particular application. Manuals usually concentrate on the strong points of a proof...
The Calculation of a Polytypic Parser (1996)
In this paper it is shown how inverses can be used to calculate a parser. A polytypic unparser is given and by using rules for calculating inverses a polytypic parser is calculated from it. It can be...
Functional outcome after sacrospinous hysteropexy for uterine descensus
Dietz, Viviane, Huisman, Marieke, De Jong, Joyce M., Heintz, Peter M., Van Der Vaart, Carl H.
The study aimed to evaluate urogenital symptoms, defecatory symptoms and quality of life before and after a sacrospinous hysteropexy for uterovaginal prolapse. Seventy-two women with symptomatic...