default search action
Jan Friso Groote
Person information
- affiliation: Eindhoven University of Technology, The Netherlands
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j64]Jan Friso Groote, Marieke Huisman:
Formal Methods for Industrial Critical Systems. Int. J. Softw. Tools Technol. Transf. 26(2): 127-129 (2024) - [c91]Jan Martens, Jan Friso Groote:
Minimal Depth Distinguishing Formulas Without Until for Branching Bisimulation. Logics and Type Systems in Theory and Practice 2024: 188-202 - [c90]Kevin H. J. Jilissen, Peter Dieleman, Jan Friso Groote:
Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment. MARS@ETAPS 2024: 101-127 - [i23]Jan Friso Groote, Sander van Heesch, Matthias Volk:
Formal Modelling and Analysis of Slot Machines. CoRR abs/2407.06809 (2024) - [i22]Jan Friso Groote, Tim A. C. Willemse:
On Woolhouse's Cotton-Spinning Problem. CoRR abs/2408.12623 (2024) - 2023
- [b4]Muhammad Atif, Jan Friso Groote:
Understanding Behaviour of Distributed Systems Using mCRL2, 1. Springer 2023, ISBN 978-3-031-23007-3, pp. 1-200 - [j63]Jan Friso Groote, Jan Martens, Erik P. de Vink:
Lowerbounds for Bisimulation by Partition Refinement. Log. Methods Comput. Sci. 19(2) (2023) - [j62]Johri van Eerd, Jan Friso Groote, Pieter Hijma, Jan Martens, Muhammad Osama, Anton Wijs:
Innermost many-sorted term rewriting on GPUs. Sci. Comput. Program. 225: 102910 (2023) - [j61]Jan Martens, Jan Friso Groote, Lars B. van den Haak, Pieter Hijma, Anton Wijs:
Linear parallel algorithms to compute strong and branching bisimilarity. Softw. Syst. Model. 22(2): 521-545 (2023) - [c89]Jan Friso Groote, Tim A. C. Willemse:
Real Equation Systems with Alternating Fixed-Points. CONCUR 2023: 28:1-28:17 - [c88]Jan Martens, Jan Friso Groote:
Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. CONCUR 2023: 32:1-32:17 - [c87]Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink, Erik P. de Vink:
Minimisation of Spatial Models Using Branching Bisimilarity. FM 2023: 263-281 - [c86]Faezeh Labbaf, Jan Friso Groote, Hossein Hojjat, Mohammad Reza Mousavi:
Compositional Learning for Interleaving Parallel Automata. FoSSaCS 2023: 413-435 - [c85]Tom T. P. Franken, Thomas Neele, Jan Friso Groote:
An Autonomous Data Language. ICTAC 2023: 158-177 - [c84]Kevin H. J. Jilissen, Peter Dieleman, Jan Friso Groote:
A formal analysis of Dutch Generic Integral Tunnel Design models. SAC 2023: 1681-1684 - [c83]Rob van Glabbeek, Jan Friso Groote, Erik P. de Vink:
A Cancellation Law for Probabilistic Processes. EXPRESS/SOS 2023: 42-58 - [i21]Sander Thuijsman, Gökhan Kahraman, Alireza Mohamadkhani, Ferry Timmers, Loek Cleophas, Marc Geilen, Jan Friso Groote, Michel A. Reniers, Ramon R. H. Schiffelers, Jeroen Voeten:
Tool interoperability for model-based systems engineering. CoRR abs/2302.03503 (2023) - [i20]Jan Martens, Jan Friso Groote:
Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable. CoRR abs/2307.05265 (2023) - [i19]Jan Friso Groote, Tim A. C. Willemse:
Real Equation Systems with Alternating Fixed-points (full version with proofs). CoRR abs/2307.07455 (2023) - 2022
- [c82]Jan Friso Groote, Kevin H. J. Jilissen, Maurice Laveaux, P. H. M. van Spaendonck, Tim A. C. Willemse:
Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 306-320 - [c81]Bram Hooimeijer, Marc Geilen, Jan Friso Groote, Dennis Hendriks, Ramon R. H. Schiffelers:
Constructive Model Inference: Model Learning for Component-based Software Architectures. ICSOFT 2022: 146-158 - [c80]Jan Friso Groote, Maurice Laveaux, P. H. M. van Spaendonck:
A Thread-Safe Term Library - (with a New Fast Mutual Exclusion Protocol). ISoLA (1) 2022: 422-459 - [e7]Jan Friso Groote, Marieke Huisman:
Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, Proceedings. Lecture Notes in Computer Science 13487, Springer 2022, ISBN 978-3-031-15007-4 [contents] - [i18]Jan Friso Groote, Jan Martens, Erik P. de Vink:
Lowerbounds for Bisimulation by Partition Refinement. CoRR abs/2203.07158 (2022) - 2021
- [b3]Jan Friso Groote, Rolf Morel, Julien Schmaltz, Adam Watkins:
Logic Gates, Circuits, Processors, Compilers and Computers. Springer 2021, ISBN 978-3-030-68552-2, pp. 1-193 - [j60]Maurice Laveaux, Jan Friso Groote, Tim A. C. Willemse:
Correct and Efficient Antichain Algorithms for Refinement Checking. Log. Methods Comput. Sci. 17(1) (2021) - [c79]Jan Friso Groote, Jan Martens, Erik P. de Vink:
Bisimulation by Partitioning Is Ω((m+n)log n). CONCUR 2021: 31:1-31:16 - [c78]Jan Martens, Jan Friso Groote, Lars B. van den Haak, Pieter Hijma, Anton Wijs:
A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions. FACS 2021: 115-133 - [c77]Jan Friso Groote, Jeroen J. A. Keiren:
Tutorial: Designing Distributed Software in mCRL2. FORTE 2021: 226-243 - [c76]Johri van Eerd, Jan Friso Groote, Pieter Hijma, Jan Martens, Anton Wijs:
Term Rewriting on GPUs. FSEN 2021: 175-189 - [c75]Rick Erkens, Jan Friso Groote:
A Set Automaton to Locate All Pattern Matches in a Term. ICTAC 2021: 67-85 - [c74]Jan Friso Groote:
Infinite Choice and Probability Distributions. An Open Problem: The Real Hotel. EXPRESS/SOS 2021: 2-8 - [e6]Jan Friso Groote, Kim Guldstrand Larsen:
Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I. Lecture Notes in Computer Science 12651, Springer 2021, ISBN 978-3-030-72015-5 [contents] - [e5]Jan Friso Groote, Kim Guldstrand Larsen:
Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science 12652, Springer 2021, ISBN 978-3-030-72012-4 [contents] - [i17]Jan Friso Groote, Jeroen J. A. Keiren:
Tutorial: Designing Distributed Software in mCRL2. CoRR abs/2104.10542 (2021) - [i16]Jan Martens, Jan Friso Groote, Lars B. van den Haak, Pieter Hijma, Anton Wijs:
A linear parallel algorithm to compute bisimulation and relational coarsest partitions. CoRR abs/2105.11788 (2021) - [i15]Rick Erkens, Jan Friso Groote:
A Set Automaton to Locate All Pattern Matches in a Term. CoRR abs/2106.15311 (2021) - [i14]Yousra Hafidi, Jeroen J. A. Keiren, Jan Friso Groote:
Fair Mutual Exclusion for N Processes (extended version). CoRR abs/2111.02251 (2021) - [i13]Jan Friso Groote, Maurice Laveaux, P. H. M. van Spaendonck:
A thread-safe Term Library. CoRR abs/2111.02706 (2021) - 2020
- [j59]Ferry Timmers, Jan Friso Groote:
A Complete Axiomatisation for Probabilistic Trace Equivalence. Sci. Ann. Comput. Sci. 30(1): 69-104 (2020) - [j58]Jan Friso Groote, Tim A. C. Willemse:
A symmetric protocol to establish service level agreements. Log. Methods Comput. Sci. 16(3) (2020) - [j57]Thomas Neele, Tim A. C. Willemse, Jan Friso Groote:
Finding compact proofs for infinite-data parameterised Boolean equation systems. Sci. Comput. Program. 188: 102389 (2020) - [c73]David N. Jansen, Jan Friso Groote, Ferry Timmers, Pengfei Yang:
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. CONCUR 2020: 8:1-8:20 - [c72]Omar al Duhaiby, Jan Friso Groote:
Active Learning of Decomposable Systems. FormaliSE@ICSE 2020: 1-10 - [c71]Arash Khabbaz Saberi, Jos Hegge, Terry Fruehling, Jan Friso Groote:
Beyond SOTIF: Black Swans and Formal Methods. SysCon 2020: 1-5 - [c70]David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs:
An O(m log n) algorithm for branching bisimilarity on labelled transition systems. TACAS (2) 2020: 3-20 - [i12]Jan Friso Groote, Tim A. C. Willemse:
A symmetric protocol to establish service level agreements. CoRR abs/2001.07658 (2020) - [i11]Johri van Eerd, Jan Friso Groote, Pieter Hijma, Jan Martens, Anton Wijs:
Term Rewriting on GPUs. CoRR abs/2009.07174 (2020) - [i10]Yuting Fu, Andrei Sergeevich Terechko, Jan Friso Groote, Arash Khabbaz Saberi:
A Formally Verified Fail-Operational Safety Concept for Automated Driving. CoRR abs/2011.00892 (2020)
2010 – 2019
- 2019
- [j56]Dmitry A. Zaitsev, Tatiana R. Shmeleva, Jan Friso Groote:
Verification of hypertorus communication grids by infinite petri nets and process algebra. IEEE CAA J. Autom. Sinica 6(3): 733-742 (2019) - [c69]Rob J. van Glabbeek, Jan Friso Groote, Erik P. de Vink:
A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice - (Extended Abstract). The Art of Modelling Computational Systems 2019: 139-162 - [c68]Jan Friso Groote, Erik P. de Vink:
An Axiomatization of Strong Distribution Bisimulation for a Language with a Parallel Operator and Probabilistic Choice. From Software Engineering to Formal Methods and Tools, and Back 2019: 449-463 - [c67]Jan Friso Groote, Jeroen J. A. Keiren, Bas Luttik, Erik P. de Vink, Tim A. C. Willemse:
Modelling and Analysing Software in mCRL2. FACS 2019: 25-48 - [c66]Maurice Laveaux, Jan Friso Groote, Tim A. C. Willemse:
Correct and Efficient Antichain Algorithms for Refinement Checking. FORTE 2019: 185-203 - [c65]Lisette Sanchez, Jan Friso Groote, Ramon R. H. Schiffelers:
Active Learning of Industrial Software with Data. FSEN 2019: 95-110 - [c64]Thomas Neele, Marijn Rol, Jan Friso Groote:
Verifying System-Wide Properties of Industrial Component-Based Software. FSEN 2019: 158-175 - [c63]Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, Tim A. C. Willemse:
The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability. TACAS (2) 2019: 21-39 - [c62]Omar al Duhaiby, Jan Friso Groote:
Distribution of Behaviour into Parallel Communicating Subsystems. EXPRESS/SOS 2019: 54-68 - [i9]Maurice Laveaux, Jan Friso Groote, Tim A. C. Willemse:
Correct and Efficient Antichain Algorithms for Refinement Checking. CoRR abs/1902.09880 (2019) - [i8]David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs:
A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems. CoRR abs/1909.10824 (2019) - 2018
- [j55]Jan Friso Groote, Jao Rivera Verduzco, Erik P. de Vink:
An Efficient Algorithm to Determine Probabilistic Bisimulation. Algorithms 11(9): 131 (2018) - [c61]Thomas Neele, Tim A. C. Willemse, Jan Friso Groote:
Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting. FACS 2018: 216-236 - [c60]Omar al Duhaiby, Arjan J. Mooij, Hans van Wezep, Jan Friso Groote:
Pitfalls in Applying Model Learning to Industrial Legacy Software. ISoLA (4) 2018: 121-138 - 2017
- [j54]Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, Anton Wijs:
An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation. ACM Trans. Comput. Log. 18(2): 13:1-13:34 (2017) - [c59]Mahmoud Talebi, Jan Friso Groote, Jean-Paul M. G. Linnartz:
The Mean Drift: Tailoring the Mean Field Theory of Markov Processes for Real-World Applications. ASMTA 2017: 196-211 - [c58]Jan Friso Groote, Erik P. de Vink:
Problem Solving Using Process Algebra Considered Insightful. ModelEd, TestEd, TrustEd 2017: 48-63 - [c57]Rutger van Beusekom, Jan Friso Groote, Paul F. Hoogendijk, Robert Howe, Wieger Wesselink, Rob Wieringa, Tim A. C. Willemse:
Formalising the Dezyne Modelling Language in mCRL2. FMICS-AVoCS 2017: 217-233 - [c56]Ammar Osaiweran, Jelena Marincic, Jan Friso Groote:
Assessing the Quality of Tabular State Machines through Metrics. QRS 2017: 426-433 - [c55]Mahmoud Talebi, Jan Friso Groote, Conrad Dandelski:
Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode. MARS@ETAPS 2017: 117-128 - 2016
- [j53]Jan Friso Groote, Remco van der Hofstad, Matthias Raffelsieper:
On the random structure of behavioural transition systems. Sci. Comput. Program. 128: 51-67 (2016) - [j52]Jan Friso Groote, Freek Wiedijk, Hans Zantema:
A Probabilistic Analysis of the Game of the Goose. SIAM Rev. 58(1): 143-155 (2016) - [j51]Ammar Osaiweran, Mathijs Schuts, Jozef Hooman, Jan Friso Groote, Bart J. van Rijnsoever:
Evaluating the effect of a lightweight formal technique in industry. Int. J. Softw. Tools Technol. Transf. 18(1): 93-108 (2016) - [c54]Marieke Huisman, Herbert Bos, Sjaak Brinkkemper, Arie van Deursen, Jan Friso Groote, Patricia Lago, Jaco van de Pol, Eelco Visser:
Software that Meets Its Intent. ISoLA (2) 2016: 609-625 - [c53]Jan Friso Groote, Anton Wijs:
An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation. TACAS 2016: 607-624 - [i7]Jan Friso Groote, Anton Wijs:
An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation. CoRR abs/1601.01478 (2016) - 2015
- [j50]Mark van den Brand, Jan Friso Groote:
Software engineering: Redundancy is key. Sci. Comput. Program. 97: 75-81 (2015) - [j49]Jan Friso Groote, Tim W. D. M. Kouters, Ammar Osaiweran:
Specification guidelines to avoid the state space explosion problem. Softw. Test. Verification Reliab. 25(1): 4-33 (2015) - [c52]Mahmoud Talebi, Jan Friso Groote, Jean-Paul M. G. Linnartz:
Continuous approximation of stochastic models for wireless sensor networks. SCVT 2015: 1-6 - [e4]Rob J. van Glabbeek, Jan Friso Groote, Peter Höfner:
Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, November 23, 2015. EPTCS 196, 2015 [contents] - [i6]Mahmoud Talebi, Jan Friso Groote, Jean-Paul M. G. Linnartz:
Communication Patterns in Mean Field Models for Wireless Sensor Networks. CoRR abs/1503.07693 (2015) - [i5]Sarmen Keshishzadeh, Jan Friso Groote:
Exact Real Arithmetic with Perturbation Analysis and Proof of Correctness. CoRR abs/1509.06265 (2015) - 2014
- [b2]Jan Friso Groote, Mohammad Reza Mousavi:
Modeling and Analysis of Communicating Systems. MIT Press 2014, ISBN 9780262027717 - [j48]Jan Friso Groote, Mohammad Reza Mousavi:
Book Announcement: Modeling and Analysis of Communicating Systems. Bull. EATCS 114 (2014) - [j47]Jan Friso Groote, Remco van der Hofstad, Matthias Raffelsieper:
On the Random Structure of Behavioural Transition Systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014) - [i4]Mark G. J. van den Brand, Jan Friso Groote:
Redundancy in the Software Design Process is Essential for Designing Correct Software. ERCIM News 2014(99) (2014) - 2013
- [c51]Arash Khabbaz Saberi, Jan Friso Groote, Sarmen Keshishzadeh:
Analysis of Path Planning Algorithms: a Formal Verification-based Approach. ECAL 2013: 232-239 - [c50]Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, Tim A. C. Willemse:
An Overview of the mCRL2 Toolset and Its Recent Advances. TACAS 2013: 199-213 - 2012
- [c49]Ammar Osaiweran, Tom Fransen, Jan Friso Groote, Bart J. van Rijnsoever:
Experience Report on Designing and Developing Control Components Using Formal Methods. FM 2012: 341-355 - [c48]Jan Friso Groote, Ammar Osaiweran, Jacco H. Wesselius:
Analyzing a Controller of a Power Distribution Unit Using Formal Methods. ICST 2012: 420-428 - [c47]Jan Friso Groote, Ammar Osaiweran, Jacco H. Wesselius:
Experience report on developing the Front-end client unit under the control of formal methods. SAC 2012: 1183-1190 - [c46]Frank P. M. Stappers, Michel A. Reniers, Sven Weber, Jan Friso Groote:
Dogfooding the Formal Semantics of mCRL2. SEW 2012: 90-99 - [i3]Mark G. J. van den Brand, Jan Friso Groote:
Advances in Model Driven Software Engineering. ERCIM News 2012(91) (2012) - 2011
- [j46]Christoph Brandt, Frank Hermann, Jan Friso Groote:
Generation and Evaluation of Business Continuity Processes using Algebraic Graph Transformation and the mCRL2 Process Algebra. J. Res. Pract. Inf. Technol. 43(1): 65-86 (2011) - [j45]Jan Friso Groote, Jeroen Keiren, Frank P. M. Stappers, Wieger Wesselink, Tim A. C. Willemse:
Experiences in developing the mCRL2 toolset. Softw. Pract. Exp. 41(2): 143-153 (2011) - [j44]Sjoerd Cranen, Jan Friso Groote, Michel A. Reniers:
A linear translation from CTL* to the first-order modal μ -calculus. Theor. Comput. Sci. 412(28): 3129-3139 (2011) - [c45]Jan Friso Groote, Tim W. D. M. Kouters, Ammar Osaiweran:
Specification Guidelines to Avoid the State Space Explosion Problem. FSEN 2011: 112-127 - [c44]Jan Friso Groote, Ammar Osaiweran, Jacco H. Wesselius:
Analyzing the effects of formal methods on the development of industrial control software. ICSM 2011: 467-472
2000 – 2009
- 2009
- [j43]Jan Friso Groote, Bas Ploeger:
Switching Graphs. Int. J. Found. Comput. Sci. 20(5): 869-886 (2009) - [j42]Tom A. N. Engels, Jan Friso Groote, Muck van Weerdenburg, Tim A. C. Willemse:
Search algorithms for automated validation. J. Log. Algebraic Methods Program. 78(4): 274-287 (2009) - [c43]Gerard J. M. Smit, Gerrit F. van der Hoeven, Jan Friso Groote, Ralph H. J. M. Otten, Hans Tonino, Ben H. H. Juurlink, Boudewijn R. H. M. Haverkort:
The 3TU embedded systems master in the Netherlands. WESE@ESWEEK 2009: 8-12 - [c42]Frank P. M. Stappers, Michel A. Reniers, Jan Friso Groote:
Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study. FMCO 2009: 166-185 - 2008
- [j41]Alessandro Di Bucchianico, Jan Friso Groote, Kees M. van Hee, Ronald Kruidhof:
Statistical Certification of Software Systems. Commun. Stat. Simul. Comput. 37(2): 346-359 (2008) - [c41]Jan Friso Groote, Simona Orzan:
Parameterised Anonymity. Formal Aspects in Security and Trust 2008: 177-191 - [c40]Jan Friso Groote, Michel A. Reniers, Yaroslav S. Usenko:
Verification of networks of timed automata using mCRL2. IPDPS 2008: 1-8 - [c39]Jan Friso Groote, Bas Ploeger:
Switching Graphs. RP 2008: 119-135 - 2007
- [j40]Hui Gao, Jan Friso Groote, Wim H. Hesselink:
Lock-free parallel and concurrent garbage collection by mark&sweep. Sci. Comput. Program. 64(3): 341-374 (2007) - [j39]Mohammad Reza Mousavi, Michel A. Reniers, Jan Friso Groote:
SOS formats and meta-theory: 20 years after. Theor. Comput. Sci. 373(3): 238-272 (2007) - [j38]Jan Friso Groote, Marc Voorhoeve:
Operational semantics for Petri net components. Theor. Comput. Sci. 379(1-2): 1-19 (2007) - [c38]Hossein Hojjat, Marjan Sirjani, Mohammad Reza Mousavi, Jan Friso Groote:
Sarir: A Rebeca to mCRL2 Translator. ACSD 2007: 216-222 - [c37]Ivo Raedts, Marija Petkovic, Yaroslav S. Usenko, Jan Martijn E. M. van der Werf, Jan Friso Groote, Lou J. Somers:
Transformation of BPMN Models for Behaviour Analysis. MSVVEIS 2007: 126-137 - 2006
- [j37]Jan Friso Groote, Frank van Ham:
Interactive visualization of large state spaces. Int. J. Softw. Tools Technol. Transf. 8(1): 77-91 (2006) - [c36]Jan Friso Groote, Michel A. Reniers, Yaroslav S. Usenko:
Time abstraction in timed μCRL a la regions. IPDPS 2006 - [i2]Jan Friso Groote, Aad Mathijssen, Michel A. Reniers, Yaroslav S. Usenko, Muck van Weerdenburg:
The Formal Specification Language mCRL2. MMOSS 2006 - 2005
- [j36]Hui Gao, Jan Friso Groote, Wim H. Hesselink:
Lock-free dynamic hash tables with open addressing. Distributed Comput. 18(1): 21-42 (2005) - [j35]Jan Friso Groote, François Monin, Jan Springintveld:
A computer checked algebraic verification of a distributed summation algorithm. Formal Aspects Comput. 17(1): 19-37 (2005) - [j34]Bahareh Badban, Wan J. Fokkink, Jan Friso Groote, Jun Pang, Jaco van de Pol:
Verification of a sliding window protocol in µCRL and PVS. Formal Aspects Comput. 17(3): 342-388 (2005) - [j33]