Distributed Computing, 17:21–42, 2005. (2008)
B. Badban, W. Fokkink, J. F. Groote, J. Pang, C. Baier, L. Cloth, ...
[4] H. Gao, J.F. Groote, and W.H. Hesselink. Lock-free dynamic hash tables with open addressing.
Sarir: A Rebeca to mCRL2 Translator (2008)
H. Hojjat, M. Sirjani, M. R. Mousavi, J. F. Groote
We describe a translation from Rebeca, an actorbased language, to mCRL2, a process algebra enhanced with data types. The main motivation is to exploit the verification tools and theories developed...
Centrum voor Wiskunde en Informatica REPORTRAPPORT Report SEN-R0008 (2008)
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
A Dedicated Verification Approach for Scheduling in Complex Manufacturing Machines (2008)
Dynamic scheduling of the production in complex industrial manufacturing machines can lead to problems such as, for instance, deadlocks bringing the production to a standstill. An approach to ensure...
Statistical Certification of Software Systems (2008)
A. Di Bucchianico, J. F. Groote, R. Kruidhof
Common software release procedures based on statistical techniques try to optimise the tradeoff between further testing costs and costs due to remaining errors. We propose new software release...
\Gamma\Gamma\Gamma\Gamma s (2007)
Abstract. We provide several notions of confluence in processes and we show how these relate to-inertness, i.e. if s
Completeness of Timed CRL # (2007)
Mathematisch Centrum (smc, The Dutch Foundation, J. F. Groote, J. F. Groote, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
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...
Tlca' Pages, Pa Gordon Plotkin, In M. Bezem, J. F. Groote, Cc Patrick Cousot, ...
interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming...
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...
Issn -x, J. F. Groote, J. F. Groote, J. Pang, J. Pang, A. G. Wouters, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
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
Alternative Quantification over Data (2007)
S. P. Luttik, Mathematisch Centrum (smc, The Dutch Foundation, J. F. Groote, J. F. Groote
Centrum voor Wiskunde en Informatica Undecidability and completeness results for process algebras with alternative quantification over data
Model-checking processes with data (2005)
We propose a procedure for automatically verifying properties (expressed in an extension of the modal µ-calculus) over processes with data, specified in µCRL. We first briefly review existing work,...
Verifying a Sliding Window Protocol in µCRL (2004)
W. J. Fokkink, J. F. Groote, J. Pang, B. Badban, Wan Fokkink, ...
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...
Analysis of a distributed system for lifting trucks (2003)
Issn -x, J. F. Groote, J. F. Groote, J. Pang, J. Pang, A. G. Wouters, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Analysis of a distributed system for lifting trucks (2003)
J. F. Groote, J. Pang, A. G. Wouters
The process algebraic language µCRL is used to analyse an existing distributed system for lifting trucks. Four errors are found in the original design. We propose solutions for these problems and...
Completeness of timed μCRL (2002)
J. F. Groote, J. F. Groote, M. A. Reniers, M. A. Reniers, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Completeness of timed μCRL (2002)
J. F. Groote, M. A. Reniers, J. F. Groote, M. A. Reniers, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Algebraic process verification (2001)
This chapter addresses the question how to verify distributed and communicating systems in an effective way from an explicit process algebraic standpoint. This means that all calculations are based...
A balancing act: Analyzing a distributed lift system (2001)
J. F. Groote, J. Pang, A. G. Wouters
The process-algebraic language crl is used to analyze an existing distributed system for lifting trucks. Four errors were found in the original design. We propose solutions for these problems and...
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)
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...
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...
Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially (2000)
H. Zantema, J. F. Groote, J. F. Groote
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...
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...
Towards a Unified Toolset for Embedded Systems Development (2000)
A. G. Bakhmurov, V. I. Chervin, M. V. Chistolinov, J. F. Groote, V. A. Kostenko, R.L. Smeliansky, ...
This paper contains a comparative analysis of three toolsets and associated techniques for development of embedded systems. The comparison is based on the experience acquired by applying the...
Algebraic Process Verification (2000)
This paper addresses the question how to verify distributed and communicating systems in an effective way from an explicit process algebraic standpoint. This means that all calculations are based on...
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 (2000)
J. F. Groote, H. Zantema, H. Zantema
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
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...
The propositional formula checker HeerHugo (1999)
HeerHugo is a propositional formula checker 1 , that determines whether a given formula is satisfiable or not. Its name comes from the dutch railway station Heerhugowaard, as it was developed to...
Mathematisch Centrum (smc, The Dutch Foundation, J. F. Groote, J. F. Groote, S. P. Luttik, S. P. Luttik
Centrum voor Wiskunde en Informatica A complete axiomatisation of branching bisimulation for process algebras with alternative quantification over data
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
Analysis of three hybrid systems in timed CRL (1998)
J. F. Groote, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation
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 (1998)
Mathematisch Centrum (smc, The Dutch Foundation, J. F. Groote, J. F. Groote, R. Mateescu, R. Mateescu
We define a value-based modal -calculus, built from first-order formulas, modalities, and fixed point operators parameterized by data variables, which allows to express temporal properties involving...
J. F. Groote, S. P. Luttik, Copyright Stichting, Mathematisch Centrum
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
J. F. Groote, J. F. Groote, S. P. Luttik, S. P. Luttik
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Abstract Veri�cation of Temporal Properties of Processes in a Setting with Data (1998)
J. F. Groote, R. Mateescu, Issn -x, R. Mateescu
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)
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
Confluence for Process Verification (1996)
We provide several notions for confluence in processes and we show how these relate to -inertness, i.e. if s \Gamma\Gamma\Gamma s 0 , then s and s 0 are equivalent. Using clustered linear processes...
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...
Confluence for Process Verification (1996)
We provide several notions of confluence in processes and we show how these relate to ø-inertness, i.e. if s ø \Gamma\Gamma\Gamma s 0 , then s and s 0 are equivalent. Using deterministic linear...
Confluence for Process Verification (1996)
We provide several notions of confluence in processes and we show how these relate to ø-inertness, i.e. if s ø \Gamma\Gamma\Gamma s 0 , then s and s 0 are equivalent. Using deterministic linear...
Specification and implementation of components of a μCRL 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)
Groote, J.F., Springintveld, J.
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...
Binary Decision Diagrams for First Order Predicate Logic (1995)
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.
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
The Safety Guaranteeing System at Station Hoorn-Kersenboogerd (1995)
At the Dutch station Hoorn--Kersenboogerd, computer equipment is used for the safe and in time movement of trains. The computer equipment can be divided in two layers. A top layer offering an...
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
The safety guaranteeing system at station Hoorn-Kersenboogerd (1994)
At the Dutch station Hoorn-Kersenboogerd, computer equipment is used for the safe and in time movement of trains. The computer equipment can be divided in two layers. A top layer offering an...
Hiding Propositional Constants in BDDs (1994)
In [6] it is described how correctness of safety control systems of railways (interlockings) can be expressed using (large) propositional formulas. Interlockings are correct if these formulas are...
The language μCRL allows to specify processes with data and to reason with them in an algebraic vein. This allows to express and reason about global correctness of systems. Sometimes,one only needs...
Proving a graph well founded using resolution (1994)
Using the resolution theorem prover OTTER we prove that a certain directed graph has no infinite path. We argue that this technique complements the well known combinatorial algorithms in cases in...
A Correctness Proof of a One-bit Sliding Window Protocol in μCRL (1994)
ION The most substantial step in the correctness proof of the one-bit sliding window protocol is provided by the following lemma. It states, roughly, that the partial abstraction ø føc ;ø c 2 ;ø...
The language µCRL allows to specify processes with data and to reason with them in an algebraic vein. This allows to express and reason about global correctness of systems. Sometimes, one only needs...
A Correctness Proof of a One-bit Sliding Window Protocol in {micro}CRL (1994)
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in μCRL, which is a process algebra extended with data....
A Correctness Proof of a One-bit Sliding Window Protocol in μCRL (1993)
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in μCRL, which is a process algebra extended with data....
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....
Invariants in Process Algebra with Data (1993)
We provide rules for calculating with invariants in process algebra with data, and illustrate these with examples. The new rules turn out to be equivalent to the well known Recursive Specification...
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...
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 Correctness Proof of the Bakery Protocol in μCRL (1992)
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...