Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
List of model checking tools
open-in-new
<h2 id="overview-of-some-model-checking-tools">Overview of some model checking tools</h2> <p>The following table includes model checkers that have </p> <ol><li>a web site from which it can be downloaded,</li> <li>a declared license,</li> <li>a description published in archived literature, and</li> <li>a Wikipedia article describing it.</li></ol> <p>In the below table, the following abbreviations are used: </p> <ul><li>Equivalences: <ul><li>SB: Strong Bisimulation</li> <li>WB: Weak Bisimulation</li> <li>BB: Branching Bisimulation</li> <li>STE: Strong Trace Equivalence</li> <li>WTE: Weak Trace Equivalence</li> <li>me: May Equivalence</li> <li>ME: Must Equivalence</li> <li>OE: Observational Equivalence</li> <li>SE: Safety Equivalence</li> <li>t*E: tau*.a Equivalence</li></ul></li> <li>Software license: <ul><li>FUSC: Free Under Specific Condition (e.g., free for academics)</li></ul></li></ul> <table><tbody><tr><th>Name</th><th colspan="3">Model Checking</th><th colspan="2">Equivalence checking</th><th colspan="3">GUI</th><th colspan="3">Availability</th></tr><tr><th></th><th>Plain, Probabilistic, Stochastic, ...</th><th>Modelling language</th><th>Properties language</th><th>Supported equivalences</th><th>Counter example generation</th><th> GUI </th><th>Graphical Specification</th><th>Counter example visualization</th><th>Software license</th><th>Programming language used</th><th>Platform, OS</th></tr><tr><td><a href="/facts/BLAST_model_checker/jaHt31L0">BLAST</a></td><td>Code analysis</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a></td><td>Monitor automata</td><td></td><td>Yes</td><td>No</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/OCaml/ThBGLND8">OCaml</a></td><td>Windows, Unix related</td></tr><tr><td><a href="/facts/CADP/0B2WvN8q">CADP</a></td><td>Plain and probabilistic</td><td><a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">LOTOS</a>, FC2, FSP, LNT</td><td>AFMC, MCL, XTL</td><td>SB, WB, BB, OE, STE, WTE, SE, tau*E</td><td>Yes</td><td>Yes</td><td>No</td><td>Yes</td><td>FUSC</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a>, <a href="/facts/Bourne_shell/wUCh3Qkl">Bourne shell</a>, <a href="/facts/Tcl/s7fbKYtR">Tcl</a>/<a href="/facts/Tk_(software)/Y6NBxcbF">Tk</a>, <a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">LOTOS</a>, LNT</td><td>macOS, Linux, <a href="/facts/Oracle_Solaris/KPfT98EJ">Solaris</a>, Windows</td></tr><tr><td><a href="/facts/CPAchecker/2ud9JXqg">CPAchecker</a></td><td>Code analysis</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a></td><td>Monitor automata</td><td></td><td>Yes</td><td>Yes</td><td>No</td><td>Yes</td><td>Free</td><td>Java</td><td>Any</td></tr><tr><td><a href="/facts/DREAM_(software)/uwjnKNK8">DREAM</a></td><td>Real-time</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Timed_automaton/Ca89Xnbd">Timed automata</a></td><td>Monitor automata</td><td></td><td>Yes</td><td>No</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a></td><td>Windows, Unix related</td></tr><tr><td>FizzBee Specification Language</td><td>Plain and probabilistic</td><td><a href="/facts/Python_(programming_language)/YbuGqofa">Python</a></td><td><a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a></td><td></td><td>Yes</td><td>Yes</td><td>No</td><td>Yes</td><td>Free</td><td><a href="/facts/Go_(programming_language)/oWlsmAFJ">Go</a></td><td>macOS, Windows, Linux</td></tr><tr><td><a href="https://github.com/greatspn/SOURCES">GreatSPN</a></td><td>Plain, probabilistic, real-time, stochastic</td><td>Time Petri Nets, Stochastic Petri Nets, Colored Petri Nets, Well-formed Petri Nets</td><td><a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a>, <a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a>, <a href="/facts/CTL*/emAMSuXt">CTL*</a>, CSL, CSLTA</td><td></td><td>No</td><td>Yes</td><td>Yes</td><td>No</td><td>Free</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a>, <a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>macOS, Windows, Linux</td></tr><tr><td><a href="/facts/Java_Pathfinder/qos34qGV">Java Pathfinder</a></td><td>Plain and timed</td><td>Java</td><td>unknown</td><td></td><td>No</td><td>Yes</td><td>No</td><td>No</td><td>Open Source Agreement</td><td><a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>macOS, Windows, Linux</td></tr><tr><td>Murφ (Murphi)</td><td>Plain</td><td>Murφ</td><td>Invariants, assertions</td><td></td><td>Yes</td><td>No</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a></td><td>Linux</td></tr><tr><td><a href="/facts/NuSMV/BTMkwhgx">NuSMV</a></td><td>Plain</td><td>SMV input language</td><td><a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a>, <a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a>, <a href="/facts/Property_Specification_Language/2cGX8xlm">PSL</a></td><td></td><td>Yes</td><td>No</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a></td><td>Unix, Windows, macOS</td></tr><tr><td><a href="/facts/PAT_(model_checker)/l23YAqzw">PAT</a></td><td>Plain, real-time, probabilistic</td><td><a href="/facts/Symbolic_model_verification/FwvKMlw9">CSP#</a>, timed CSP, probabilistic CSP</td><td><a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a>, <a href="/facts/Assertion_(computing)/lxSfLdLY">assertions</a></td><td></td><td>Yes</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Free</td><td><a href="/facts/C_Sharp_(programming_language)/UC2gxeyb">C#</a></td><td>Windows, others with <a href="/facts/Mono_(software)/PlyeJxRS">Mono</a></td></tr><tr><td><a href="/facts/PRISM_(model_checker)/YvPYJFAa">PRISM</a></td><td>Probabilistic</td><td><a href="/facts/PEPA/ypBwNmqd">PEPA</a>, PRISM language, Plain MC</td><td>CSL, PLTL, <a href="/facts/Probabilistic_CTL/MfKCcbyM">PCTL</a></td><td></td><td>No</td><td>Yes</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>Windows, Linux, macOS</td></tr><tr><td><a href="https://github.com/Smattr/rumur">Rumur</a></td><td>Plain</td><td>Murφ</td><td>Invariants, assertions</td><td></td><td>Yes</td><td>No</td><td>No</td><td>No</td><td>Free</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a></td><td>macOS, Linux</td></tr><tr><td><a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a></td><td>Plain</td><td><a href="/facts/Promela/raQIHtsA">Promela</a></td><td><a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a></td><td></td><td>Yes</td><td>Yes</td><td>No</td><td>Yes</td><td>FUSC</td><td><a href="/facts/C_(programming_language)/Ky2No763">C</a>, <a href="/facts/C%252B%252B/Et0F2qn9">C++</a></td><td>Windows, Unix related</td></tr><tr><td><a href="/facts/TAPAAL_Model_Checker/WK5U95jn">TAPAAL</a></td><td>Real-time</td><td>Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs</td><td>TCTL subset</td><td></td><td>No</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Free</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>macOS, Windows, Linux</td></tr><tr><td><a href="/facts/TAPAs_model_checker/PQCI00uD">TAPAs</a></td><td>Plain</td><td>CCSP</td><td><a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a>, <a href="/facts/%25CE%259C-calculus/Dv9lcbDI">μ-calculus</a></td><td>SB, WB, BB, STE, WTE, me, ME, OE</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Free</td><td><a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>Windows, macOS, Unix related</td></tr><tr><td><a href="/facts/Uppaal_Model_Checker/6R4VmIpp">UPPAAL</a></td><td>Real-time</td><td><a href="/facts/Timed_automaton/Ca89Xnbd">Timed automata</a>, C subset</td><td>TCTL subset</td><td></td><td>Yes</td><td>Yes</td><td>Yes</td><td>Yes</td><td>FUSC</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>macOS, Windows, Linux</td></tr><tr><td><a href="/facts/Romeo_Model_Checker/PaWyMS1e">ROMEO</a></td><td>Real-time</td><td>Time Petri Nets, stopwatch parametric Petri nets</td><td>TCTL subset</td><td></td><td>Yes</td><td>Yes</td><td>Yes</td><td>No</td><td>Free</td><td><a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, <a href="/facts/Tcl/s7fbKYtR">Tcl</a>/<a href="/facts/Tk_(software)/Y6NBxcbF">Tk</a></td><td>macOS, Windows, Linux</td></tr><tr><td><a href="/facts/TLA%252B/cy4IfLBa">TLA+</a> Model Checker (TLC)</td><td>Plain</td><td><a href="/facts/TLA%252B/cy4IfLBa">TLA+</a>, <a href="/facts/PlusCal/LNUFf6TE">PlusCal</a></td><td><a href="/facts/Temporal_logic_of_actions/AMKECrvK">TLA</a></td><td></td><td>Yes</td><td>Yes</td><td>Yes</td><td>No</td><td>Free</td><td><a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>macOS, Windows, Linux</td></tr></tbody></table> <h2 id="modelling-languages">Modelling languages</h2> <ul><li>CCSP: A process calculus obtained from <a href="/facts/Calculus_of_communicating_systems/0FNkQbug">CCS</a> by incorporating some operators of <a href="/facts/Communicating_sequential_processes/bzKGnJ50">CSP</a>. It is defined by Olderog<a class="footnote-ref" id="fnref:1" href="#fn:1"><sup>1</sup></a> and by van Glabbeek/Vaandrager.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a></li> <li><a href="/facts/Communicating_sequential_processes/bzKGnJ50">CSP</a>: Communicating sequential processes; formal language for describing patterns of interaction in concurrent systems. <a href="/facts/FDR2/68lJqyPL">FDR2</a> is a refinement checking tool for CSP, comparing two models for compatibility.</li> <li>DVE input language: a system is described as Network of Extended Finite State Machines communicating via shared variables and unbuffered channels. Does not contain support for buffered channels and for checking the type of message to be received without performing the receive proper.</li> <li>FC2: (Common Format V2) Machine-level ASCII representation for synchronized (hierarchical) networks of automata. Defined by the Esprit Basic Research Action CONCUR, 1992. Used as an input and exchange format by a number of verification tools, mainly in the area of process algebras.</li> <li>FSP: Finite State Processes language defined at Imperial College.</li> <li><a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a>: Object-oriented programming language.</li> <li>LNT: LOTOS New Technology; a specification language inspired by process calculi, functional programming languages, and imperative programming languages; LNT was designed as a modern replacement for <a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">LOTOS</a> and <a href="/facts/E-LOTOS/pwvyk46M">E-LOTOS</a>.</li> <li><a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">LOTOS</a>: Language Of Temporal Ordering Specification (ISO standard 8807); formal specification language based on temporal ordering used for protocol specification in ISO OSI standards.</li> <li><a href="/facts/MCRL2/eupvG7D6">mCRL2</a>: A specification language for describing concurrent discrete event systems.</li> <li>Murφ: Guarded commands and an asynchronous, interleaving model of concurrency, with all synchronization and communication done through global variables.</li> <li><a href="/facts/PEPA/ypBwNmqd">PEPA</a>: Performance Evaluation Process Algebra; it is a stochastic process algebra designed for modelling computer and communication systems.</li> <li>Plain MC: simple text-file formats used in MRMC and PRISM.</li> <li><a href="/facts/Promela/raQIHtsA">Promela</a>: Process or Protocol Meta Language; it is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems.</li> <li><a href="/facts/Starlark/WMlwGEdd">Starlark</a>: Starlark is a dialect of Python created by Google for Bazel. Model checkers like FizzBee uses Starlark/Python as the modeling language.</li> <li><a href="/facts/TLA%252B/cy4IfLBa">TLA+</a>: General-purpose specification language based on the Temporal Logic of Actions, originally used for distributed and concurrent systems. The language for the specifications and their properties is the same.</li></ul> <h2 id="properties-language">Properties language</h2> <ul><li>AFMC: Alternation-Free <a href="/facts/Modal_%25CE%25BC-calculus/Dv9lcbDI">modal μ-calculus</a>.</li> <li><a href="/facts/Assertion_(computing)/lxSfLdLY">Assertions</a>: Imperative assertion statements.</li> <li>CSL: Continuous Stochastic Logic, characterizes bisimulation of continuous-time Markov processes.</li> <li>CSRL: Continuous Stochastic Reward Logic; a logic to specify measures over CTMCs extended with a reward structure (so-called Markov reward models).</li> <li><a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a>: Computation Tree Logic; a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized.</li> <li><a href="/facts/Invariant_(mathematics)/9TeNN2ed">Invariants</a>: Predicates over a system state.</li> <li><a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a>: Linear temporal logic; a modal temporal logic with modalities referring to time.</li> <li>MCL: Model Checking Language; Alternation-Free <a href="/facts/Modal_%25CE%25BC-calculus/Dv9lcbDI">Modal μ-calculus</a> extended with user-friendly regular expressions and value-passing constructs; subsumes <a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a> and <a href="/facts/Linear_temporal_logic/Gh5yxXK7">LTL</a>.</li> <li><a href="/facts/MCRL2/eupvG7D6">mCRL2</a> mu-calculus: Kozen's propositional <a href="/facts/Modal_%25CE%25BC-calculus/Dv9lcbDI">modal μ-calculus</a> (excluding atomic propositions), extended with: data-depended processes, quantification over data types, multi-actions, time, and regular formulas.</li> <li><a href="/facts/Probabilistic_CTL/MfKCcbyM">PCTL</a>: Probabilistic <a href="/facts/Computation_tree_logic/h04gVzsL">CTL</a>; an extension of CTL which allows for probabilistic quantification of described properties.</li> <li>PLTL: Probabilistic Linear Temporal Logic.</li> <li>PRCTL: Probabilistic Reward Computation Tree Logic; it extends <a href="/facts/Probabilistic_CTL/MfKCcbyM">PCTL</a> with reward-bounded properties.</li> <li><a href="/facts/Property_Specification_Language/2cGX8xlm">PSL</a>: Property specification language</li> <li>SVA: <a href="/facts/SystemVerilog/wkBdc179">SystemVerilog</a> standards assertion language subset, standardized as IEEE 1800</li> <li>XTL: eXtended Temporal Language; a domain-specific language for quickly implementing action-based, explicit-state, value-passing model checkers.</li></ul> <h2 id="comparison-of-model-checking-tools">Comparison of model checking tools</h2> <h3>Scientific publications</h3> <p>There exists a few papers that systematically compare various model checkers on a common case study. The comparison usually discusses the modelling tradeoffs faced when using the input languages of each model checker, as well as the comparison of performances of the tools when verifying correctness properties. One can mention: </p> <ul><li>In 1999, Judi Romijn compared two model checkers (<a href="/facts/Construction_and_Analysis_of_Distributed_Processes/0B2WvN8q">CADP</a> and <a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a>) on the HAVi interoperability audio-video protocol for consumer electronics.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a></li></ul> <ul><li>In 2003, Yifei Dong, Xiaoqun Du, Gerard J. Holzmann, and Scott A. Smolka published a comparison of four model checkers (namely: Cospan, Murphi, <a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a>, and XMC) on a communication protocol, the GNU i-protocol.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a></li></ul> <ul><li>In 2005, Elena M. Bortnik, Nikola Trcka, Anton Wijs, Bas Luttik, J. M. van de Mortel-Fronczak, Jos C. M. Baeten, Wan Fokkink, and J. E. Rooda published a comparison of four model checkers (namely: <a href="/facts/Construction_and_Analysis_of_Distributed_Processes/0B2WvN8q">CADP</a>, muCRL, <a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a>, and <a href="/facts/Uppaal_Model_Checker/6R4VmIpp">UPPAAL</a>) on an industrial manufacturing system, a rotating drilling machine.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a></li></ul> <ul><li>In 2018, F. Mazzanti and A. Ferrari published a comparison of ten model checkers (namely: <a href="/facts/Construction_and_Analysis_of_Distributed_Processes/0B2WvN8q">CADP</a>, CPN Tools, FDR4, <a href="/facts/NuSMV/BTMkwhgx">NuSMV</a>/nuXmv, <a href="/facts/MCRL2/eupvG7D6">mCRL2</a>, ProB, <a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a>, <a href="/facts/TLA%252B/cy4IfLBa">TLA+</a>, UMC, and <a href="/facts/Uppaal_Model_Checker/6R4VmIpp">UPPAAL</a>) on a train supervision problem, taking into account both the user-friendliness of the languages and the performance of the tools.<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a></li></ul> <h3>International software competitions</h3> <ul><li>Since 2007, the Hardware Model Checking Competition (HWMCC) compares the performances of model checking tools oriented towards hardware design.</li> <li>Since 2011, the Model Checking Contest (MCC) compare performances of model checking tools designed to analyze highly concurrent systems.</li></ul> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/AltaRica/4jXbNLbe">AltaRica</a></li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="https://web.archive.org/web/20151106214218/http://anna.fi.muni.cz/yahoda/">Tools</a>: a database for verification tools</li> <li><a href="https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md">A list of verification and synthesis tools (public domain repository on GitHub)</a></li> <li><a href="http://cadp.inria.fr/resources/zoo">A list of verification tools for probabilistic, stochastic, hybrid, and timed systems</a></li></ul> Common benchmarks <ul><li><a href="http://mcc.lip6.fr/models.php">MCC</a> (models of the Model Checking Contest): a collection of hundreds of Petri nets originating from many academic and industrial case studies.</li> <li><a href="http://cadp.inria.fr/resources/vlts/">VLTS</a> (Very Large Transition Systems): a collection of Labelled Transition Systems of increasing sizes, used in many scientific publications.</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>E.R. Olderog: Operational Petri net semantics for CCSP <a href="/wiki/Ernst-R%C3%BCdiger_Olderog" target="_blank">/wiki/Ernst-R%C3%BCdiger_Olderog</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Rob van Glabbeek, Frits Vaandrager: Bundle Event Structures and CCSP <a href="https://doi.org/10.1007%2F978-3-540-45187-7_4" target="_blank">https://doi.org/10.1007%2F978-3-540-45187-7_4</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Romijn, Judi (June 1999). Model Checking a HAVi Leader Election Protocol (Technical report). Amsterdam: CWI. SEN-R9915. Archived from the original on 2019-09-11. Retrieved 2018-06-14. <a href="http://cadp.inria.fr/case-studies/99-a-havi.html" target="_blank">http://cadp.inria.fr/case-studies/99-a-havi.html</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking". Software Tool for Technology Transfer. 4 (4): 505–528. <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, J. M.; Baeten, Jos C. M.; Fokkink, Wan; Rooda, J. E. (2005). "Analyzing a chi model of a turntable system using Spin, CADP and Uppaal" (PDF). Journal of Logical and Algebraic Methods in Programming. 65 (2): 51–104. doi:10.1016/j.jlap.2005.05.001. Archived (PDF) from the original on 2021-01-27. Retrieved 2018-05-25. <a href="https://research.tue.nl/files/2448829/200423.pdf" target="_blank">https://research.tue.nl/files/2448829/200423.pdf</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Mazzanti, Franco; Ferrari, Alessio (2018). "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation (MARS/VPT’18), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science. Vol. 268. pp. 104–149. arXiv:1803.10324v1. doi:10.4204/EPTCS.268.4. <a href="/wiki/ArXiv_(identifier)" target="_blank">/wiki/ArXiv_(identifier)</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> </ol>