The Syntax and Semantics of uCRL (2009)
Abstract A simple specification language based on CRL (Common Representation Language) and therefore called uCRL (micro CRL) is proposed. It has been developed to study processes with data. So the...
Switching graphs are graphs containing switches. By using boolean functions called switch settings, these switches can be put in a fixed direction to obtain an ordinary graph. For many problems,...
Parameterised anonymity (2009)
Jan Friso Groote, Simona Orzan
Abstract. We introduce the notion of parameterised anonymity, to formalize the anonymity property of protocols with an arbitrary number of participants. This definition is an extension of the well...
Designing and Understanding the Behaviour of Systems (2009)
Jan Friso Groote, Michel Reniers
Robin Milner observed in 1973 that the primary task of computers appeared to interact with their environment, yet the theory of programs and programming at that time seemed to ignore this fact...
Designing and Understanding the Behaviour of Systems (2008)
Jan Friso Groote, Michel Reniers
Robin Milner observed in 1973 that the primary task of computers appeared to be interacting with their environment, yet the theory of programs and programming at that time seemed to ignore this fact...
Software Engineering Reference Framework (2008)
Michel Chaudron, Jan Friso Groote, Kees Van Hee, Kees Hemerik, Lou Somers, Tom Verhoeff
framework will be used to unify the basic concepts and the terminology in the various courses that cover topics of software engineering and in the OGOprojects, including the Software Engineering...
SOS formats and meta-theory: 20 years after (2008)
Mohammadreza Mousavi, Michel A. Reniers, Jan Friso Groote
In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [113]. Subsequently,...
Statistical Certification of Software Systems (2008)
Ro Di Bucchianico, Jan Friso Groote, Kees Van Hee, Ronald Kruidhof
Common software release procedures based on statistical techniques try to optimise the trade-off between further testing costs and costs due to remaining errors. We propose new software release...
Transformation of BPMN models for Behaviour Analysis (2008)
Ivo Raedts, Marija Petković, Yaroslav S. Usenko, Jan Friso Groote, Lou Somers
Abstract. In industry, many business processes are modelled and stored in Enterprise Information Systems (EIS). Tools supporting the verification and validation of business processes can help to...
Analysing the BKE-security protocol with μCRL (2008)
Jan Friso Groote, Sjouke Mauw, Alexander Serebrenik, Jan Friso, Groote Sjouke, Mauw Alexander Serebrenik
The CRL language and its corresponding tool set form a powerful methodology for the verification of distributed systems. We demonstrate its use by applying it to a well-known security protocol: the...
Binary Decision Diagrams for First Order Predicate Logic (2008)
We present an extension of Binary Decision Diagrams (BDDs) such that they can be used for predicate logic. We present a sound and complete proof search method which we apply to a number of examples....
Operational semantics for Petri Net components (2008)
Jan Friso Groote, Marc Voorhoeve
We develop a theory for net components with labeled interface places and transitions. Nets are shown to be isomorphic to algebraic terms, with marked places and transitions as atoms and arc addition,...
Jan Friso Groote, Wim H. Hesselink, Sjouke Mauw, Rogier Vermeulen
(will be inserted by the editor) An algorithm for the asynchronous Write-All problem based on process collision
Focus Points and Convergent Process Operators (2007)
Proof Strategy For, J. F. Groote, J. G. Springintveld, Issn -x, Jan Friso Groote, Jan Springintveld
We present a strategy for finding algebraic correctness proofs for communication systems. It is described in the setting of CRL [11], which is, roughly, ACP [2, 3] extended with a formal treatment of...
Alternative Quantification Vs. Input Prefixing (2007)
Jan Friso, Jan Friso Groote, Bas Luttik
This is a summary of our paper "Process algebras with alternative quantification over data" (Groote and Luttik (1998)). In this paper, we define a class of process algebras with a...
Marc Bezem, Jan Friso Groote, Roland Bol
This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that proofs can be verified, and partly constructed, by...
Task Allocation in a Multi-Server System (2007)
S. C. Borst, O. J. Boxma, J. F. Groote, S. Mauw, Sem Borst, Onno Boxma, ...
CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...
J. F. Groote, B. Lisser, Jan Friso Groote, Bert Lisser
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Waitfree Distributed Memory Management by (2007)
W. H. Hesselink, J. F. Groote, Wim H. Hesselink, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Operational semantics for Petri Net components (2007)
Jan Friso Groote, Marc Voorhoeve
We develop a theory for net components with labeled interface places and transitions. Nets are shown to be isomorphic to algebraic terms, with marked places and transitions as atoms and arc addition,...
The Formal Specification Language mCRL2 (2007)
Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, Muck Van Weerdenburg
Abstract. We introduce mCRL2, a specification language that can be used to specify and analyse the behaviour of distributed systems. This language is the successor of the µCRL specification...
The Formal Specification Language mCRL2 (2007)
Groote, Jan Friso, Mathijssen, Aad, Reniers, Michel, Usenko, Yaroslav, Van Weerdenburg, Muck
We introduce mCRL2, a specification language that can be used to specify and analyse the behaviour of distributed systems. This language is the successor of the mCRL specification language. The mCRL2...
Parameterised boolean equation systems (2005)
Jan Friso Groote, Tim Willemse
Boolean equation system are a useful tool for verifying formulas from modal mu-calculus on transition systems (see [18] for an excellent treatment). We are interested in an extension of boolean...
A syntactic commutativity format for SOS (2005)
Mohammadreza Mousavi, Michel Reniers, Jan Friso Groote
Considering operators defined using Structural Operational Semantics (SOS), commutativity axioms are intuitive properties that hold for many of them. Proving this intuition is usually a laborious...
A syntactic commutativity format for SOS (2005)
Mohammadreza Mousavi, Michel Reniers, Jan Friso Groote
Considering operators defined using Structural Operational Semantics (SOS), commutativity axioms are intuitive properties that hold for many of them. Proving this intuition is usually a laborious...
A Sub-quadratic Algorithm for Conjunctive and Disjunctive BESs (2004)
Jan Friso Groote, Misa Keinänen
We present an algorithm for conjunctive and disjunctive Boolean equation systems (BESs), which arise frequently in the verification and analysis of finite state concurrent systems. In contrast to the...
Congruence for SOS with Data (2004)
Mohammadreza Mousavi Michel, Michel Reniers, Jan Friso Groote
While studying the specification of the operational semantics of di#erent programming languages and formalisms, one can observe the following three facts. Firstly, Plotkin's style of Structured...
Congruence for SOS with data (2004)
Mohammadreza Mousavi, Michel Reniers, Jan Friso Groote
While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. Firstly, Plotkin’s style of Structured...
Congruence for SOS with data (2004)
Mohammadreza Mousavi, Michel Reniers, Jan Friso Groote
While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. Firstly, Plotkin’s style of Structured...
Lock-free dynamic hash tables with open addressing (2003)
Gao, Hui, Groote, Jan Friso, Hesselink, Wim H.
We present an efficient lock-free algorithm for parallel accessible hash tables with open addressing, which promises more robust performance and reliability than conventional lock-based...
Transforming equality logic to propositional logic (2003)
Hans Zantema, Jan Friso Groote
We investigate and compare various ways of transforming equality formulas to propositional formulas, in order to be able to solve satisfiability in equality logic by means of satisfiability in...
Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points (2003)
Jan Friso Groote, Misa Keinänen
This paper presents a technique for the resolution of alternating disjunctive/conjunctive boolean equation systems. The technique can be used to solve various verification problems on finite-state...
Large state space visualization (2003)
Jan Friso Groote, Frank Van Ham
Abstract. Insight in the global structure of a state space is of great help in the analysis of the underlying process. We advocate the use of visualization for this purpose and present a new method...
Large State Space Visualization (2003)
Jan Friso Groote, Frank Van Ham
Insight in the global structure of a state space is of great help in the analysis of the underlying process. We present a tool to visualize the structure of very large state spaces. It uses a...
THE JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING (2002)
Jan Friso Groote, Olga Tveretina
www.elsevier.com/locate/jlap Binary decision diagrams for first-order predicate logic
A Checker for Modal Formulas for Processes with Data (2002)
We propose an algorithm for the automatic verification of first-order modal µ-calculus formulae on infinite state, data-dependent processes. The use of boolean equation systems for solving the...
µCRL: A toolset for analysing algebraic specifications (2001)
Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak Van Langevelde, Bert Lisser
µCRL [13] is a language for specifying and verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour in a process-algebraic style and of data elements...
The Parallel Composition of Uniform Processes with Data (2001)
Jan Friso Groote, Jos Van Wamel
A general basis for the definition of a finite but unbounded number of parallel processes is the equation S(n; dt) = P (0; get(0; dt))/ eq(n; 0) .(P (n; get(n; dt)) k S(n \Gamma 1; dt)). In this...
Analysis of three hybrid systems in timed µCRL (2001)
J. F. Groote, J. Van Wamel, Issn -x, Jan Friso Groote, Jos Van Wamel
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Task Allocation in a Multi-Server System (2001)
S. C. Borst, O. J. Boxma, J. F. Groote, S. Mauw, Sem Borst, Onno Boxma, ...
CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...
Computer assisted manipulation of algebraic process specifications (2001)
J. F. Groote, B. Lisser, Copyright Stichting, Mathematisch Centrum, Jan Friso Groote, Bert Lisser
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Linearization in parallel pCRL (2001)
J. F. Groote, A. Ponse, Y. S. Usenko, Issn -x, Jan Friso Groote, Alban Ponse, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially (2000)
Jan Friso Groote, Hans Zantema
There are many di#erent ways of proving formulas in proposition logic. Many of these can easily be characterized as forms of resolution (e.g. [12] and [9]). Others use so-called binary decision...
Equational Binary Decision Diagrams (2000)
J. F. Groote, Jan Friso Groote
We incorporate equations in binary decision diagrams (BDD). The resulting objects are called EQ-BDDs. A straightforward notion of ordered EQ-BDDs (EQ-OBDD) is defined, and it is proved that each...
Linearization in Parallel pCRL (2000)
J. F. Groote, A. Ponse, Y. S. Usenko, Mathematisch Centrum (smc, The Dutch Foundation, Jan Friso Groote, ...
We describe a linearization algorithm for parallel pCRL processes similar to the one implemented in the linearizer of the CRL Toolset. This algorithm finds its roots in formal language theory: the...
ABSTRACT Equational Binary Decision Diagrams (2000)
J. F. Groote, Issn -x, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially (2000)
Jan Friso Groote, Hans Zantema
There are many different ways of proving formulas in proposition logic. Many of these can easily be characterized as forms of resolution (e.g. [12] and [9]). Others use so-called binary decision...
The propositional formula checker heerhugo (2000)
Jan Friso Groote, Joost P. Warners, Issn -x
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Verification of Temporal Properties of Processes in a Setting with Data (1999)
Abstract. We define a value-based modal-calculus, built from firstorder formulas, modalities, and fixed point operators parameterized by data variables, which allows to express temporal properties...
Tutorial and Reference Guide for the µCRL toolset version 1.0 (1999)
This document provide sufficient material to use the algebraic process description language CRL and the tools in the toolset (version 1.0). First an explanation for the data and process part of CRL...
The Propositional Formula Checker HeerHugo (1999)
J. F. Groote, J. P. Warners, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, Jan Friso Groote
HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. Its main ingredient is the branch/merge rule, that is inspired by an algorithm proposed by...
1.0, LAnguage for Railway Interlocking Specifications, To appear as a publication of CWI, the (1999)
Wan Fokkink, Jan Friso Groote, Marco Hollenberg
This document has been produced in cooperation
Basic theorems for parallel processes in timed CRL (1998)
J. F. Groote, J. Van Wame, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Basic theorems for parallel processes in timed CRL (1998)
Jan Friso Groote, Jos Van Wamel
Abstract. Timed CRL is a process algebra-based formalism for the specification and verification of parallel, communicating systems with explicit time [6, 9]. In this paper various basic results are...
Waitfree distributed memory management by Create, and Read Until Deletion (CRUD) (1998)
Wim H. Hesselink, Jan Friso Groote
The acronym CRUD represents an interface specification and an algorithm for the management of memory shared by concurrent processes. The memory cells form a directed acyclic graph. This graph is only...
Checking Verifications of Protocols and Distributed Systems By Computer (1998)
Jan Friso Groote, Francois Monin
We provide a treatise about checking proofs of distributed systems by computer using general purpose proof checkers. In particular, we present two approaches to verifying and checking the...
Basic theorems for parallel processes in timed CRL (1998)
J. F. Groote, J. Van Wamel, Issn -x, Copyright Stichting, Mathematisch Centrum, Jan Friso Groote, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
The syntax and semantics of timed CRL (1997)
J. F. Groote, Issn -x, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
A Note on n Similar Parallel Processes (1997)
J. F. Groote, Issn -x, Jan Friso Groote
We show that defining a finite but unbounded number of parallel processes using the equation S(k, dt) = P (0, get(0, dt))/eq(k, 0).(S(k - 1, dt) || P (k, get(k, dt))) is well defined, if one adopts...
The Syntax and Semantics of timed muCRL (1997)
J. F. Groote, Issn -x, Jan Friso Groote
We define a specification language called `timed CRL'. This language is designed to describe communicating processes employing data and time. Timed CRL is the successor of CRL [17]. It differs...
The syntax and semantics of timed CRL (1997)
J. F. Groote, Issn -x, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Algebraic Verification of a Distributed Summation Algorithm (1996)
J. F. Groote, J. G. Springintveld, Issn -x, Jan Friso Groote, Jan Springintveld
In this note we present an algebraic verification of Segall's Propagation of Information with Feedback (PIF) algorithm. This algorithm serves as a nice benchmark for verification exercises (see...
A Proof of a Leader Election Protocol in microCRL ($\mu$CRL) (1995)
Fredlund, Lars-åke, Groote, Jan Friso, Korver, Henri
In 1982 Dolev, Klawe & Rodeh presented an O(n log n) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem}. At the same time Peterson came up with a...
A complete equational axiomatization for mpa with string iteration (1995)
Jan Friso Groote, Luca Aceto, Luca Aceto
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
A complete equational axiomatization for mpa with string iteration (1995)
L. Aceto, J. F. Groote, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, Luca Aceto, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Specification and Implementation of Components of a muCRL Toolbox (1995)
We develop a set of tools to translate linear ¯CRL specifications to finite transition systems. These tools are intended to function as the core of larger toolsets comprising model checkers, weak or...
Focus Points and Convergent Process Operators. A Proof Strategy for Protocol Verification (1995)
We present a strategy for finding algebraic correctness proofs for communication systems. It is described in the setting of ¯CRL [11], which is, roughly, ACP [2, 3] extended with a formal treatment...
Formal Verification of a Leader Election Protocol in Process Algebra (1995)
Lars-åke Fredlund, Jan Friso Groote, Lars-ake Fredlund, Jan Friso, Henri Korver
In 1982 Dolev, Klawe & Rodeh presented an O(n log n) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem. At the same time Peterson came up with a...
A complete equational axiomatization for mpa with string iteration (1995)
L. Aceto, J. F. Groote, Copyright Stichting, Mathematisch Centrum, Luca Aceto, Jan Friso Groote
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Algebraic Data Types and Induction in µCRL (1994)
Jan Friso Groote, Jos Van Wamel
In this paper a thorough treatment of elementary data types is given in the specification language ¯CRL, which integrates data specification with process specification. Data specification in ¯CRL...
A Correctness Proof of the Bakery Protocol in mCRL (1994)
Jan Friso Groote, Henri Korver
A specification of a bakery protocol is given in ¯CRL. We provide a simple correctness criterion for the protocol. Then the protocol is proven correct using a proof system that has been developed...
A Correctness Proof of the Bakery Protocol in µCRL (1994)
Jan Friso Groote, Henri Korver
A specification of the bakery protocol is given in ¯CRL. We provide a simple correctness criterion for the protocol. Then the protocol is proven correct using a proof system that has been developed...
Hiding Propositional Constants in BDDs (1994)
this paper. At the end of the article we describe an experiment with randomised 3-SAT formulas. It is shown that if the number of occurrences of variables in 3-SAT formulas is small hiding functions...
A Formal Verification of the Alternating Bit Protocol in the Calculus of Constructions (1993)
We report on a formal verification of the Alternating Bit Protocol (ABP) in the Calculus of Constructions. We outline a semi-formal correctness proof of the ABP with sufficient detail to be...
This note describes a protocol for the transmission of data packets that are too large to be transferred in their entirety. Therefore, the protocol splits the data packets and broadcasts it in parts....
A protocol is described for the transmission of large data packets over unreliable channels. The protocol splits each data packet and broadcasts it in parts. In case of failure of transmission, only...
Verification of Parallel Systems via Decomposition (1992)
Jan Friso Groote, Faron Moller
Recently, Milner and Moller have presented several decomposition results for processes. Inspired by these, we investigate decomposition techniques for the verification of parallel systems. In...
Towards a Formal Mathematical Vernacular (1992)
Contemporary proof verificators often use a command language to construct proofs. These commands are often called tactics. This new generation of theorem provers is a substantial improvement over...
A proof theory for the specification language µCRL (micro CRL) is proposed. µCRL consists of process algebra extended with abstract data types. The proof theory is meant to formalize the...
Undecidable Equivalences for Basic Process Algebra (1991)
A recent theorem [3, 7, 19] shows that strong bisimilarity is decidable for the class of normed BPA processes, which correspond to a class of context-free grammars generating the ffl-free...