diff --git a/tools/lang/_index.md b/tools/lang/_index.md new file mode 100644 index 0000000..9aa1846 --- /dev/null +++ b/tools/lang/_index.md @@ -0,0 +1,10 @@ ++++ +title = "Languages" +layout = "section" ++++ + +This page lists all of the languages on this site in alphabetical order. +Click a tool name in the first column to view tool details. +Click a colorful item in the second column to view all the tools for which that term applies. +Item colors mean nothing and are intended to make it easy to skim the page. +Colors are generated by hashing each term's name and converting it to RGB color values. \ No newline at end of file diff --git a/tools/lang/tlaplus.md b/tools/lang/tlaplus.md new file mode 100644 index 0000000..5efcf80 --- /dev/null +++ b/tools/lang/tlaplus.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'TLA+' +subtitle = 'Modeling Language' +links = [ + { title = "Homepage", url = "https://lamport.azurewebsites.net/tla/tla.html", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Modeling Language'] +developers = [' Leslie Lamport'] +licenses = ['Open Source 3.0', 'BSD', 'GPLv2'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + + +TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. \ No newline at end of file diff --git a/tools/mc/blast.md b/tools/mc/blast.md new file mode 100644 index 0000000..3ae9beb --- /dev/null +++ b/tools/mc/blast.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'BLAST' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://forge.ispras.ru/projects/blast", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Uppsala Universitet', 'Aalborg University'] +licenses = ['Apache-2.0'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution. \ No newline at end of file diff --git a/tools/mc/cadp.md b/tools/mc/cadp.md new file mode 100644 index 0000000..afb659e --- /dev/null +++ b/tools/mc/cadp.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'CADP' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://cadp.inria.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['INRIA Rocquencourt'] +licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + +{{}} +CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package") is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc. \ No newline at end of file diff --git a/tools/mc/cgaal.md b/tools/mc/cgaal.md new file mode 100644 index 0000000..815fe25 --- /dev/null +++ b/tools/mc/cgaal.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'CGAAL' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/d702e20/CGAAL", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['University of Twente'] +licenses = ['AGPL-v3'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs). \ No newline at end of file diff --git a/tools/mc/cpachecker.md b/tools/mc/cpachecker.md new file mode 100644 index 0000000..7478ed7 --- /dev/null +++ b/tools/mc/cpachecker.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'CPAchecker' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://cpachecker.sosy-lab.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://gitlab.com/sosy-lab/software/cpachecker/", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Ludwig-Maximilians-Universität München'] +licenses = ['Apache-2.0'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + +{{}} +CPAchecker is a tool for configurable software verification. \ No newline at end of file diff --git a/tools/mc/esbmc.md b/tools/mc/esbmc.md new file mode 100644 index 0000000..087c409 --- /dev/null +++ b/tools/mc/esbmc.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'ESBMC' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://ssvlab.github.io/esbmc/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/esbmc/esbmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Federal University of Amazonas', 'University of Bristol', 'University of Manchester', 'University of Stellenbosch', 'University of Southampton'] +licenses = ['Apache-2.0', 'BSD 4-clause', 'MIT', 'BSD 3-clause', 'GPLv3', ] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. \ No newline at end of file diff --git a/tools/mc/geyser.md b/tools/mc/geyser.md new file mode 100644 index 0000000..2b5c8e5 --- /dev/null +++ b/tools/mc/geyser.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Geyser' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['Eindhoven University of Technology'] +licenses = ['MIT'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +techniques = ['PDR', 'CAR'] +# publications = [''] ++++ + +Geyser is a simple symbolic model checker for propositional transition system systems. \ No newline at end of file diff --git a/tools/mc/imspin.md b/tools/mc/imspin.md new file mode 100644 index 0000000..f78b689 --- /dev/null +++ b/tools/mc/imspin.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'ImSpin' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/MrDiver/ImSpin", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['Eindhoven University of Technology'] +licenses = ['MIT'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['PDR', 'CAR'] +# publications = [''] ++++ + +ImSpin is a frontend for the [SPIN](../spin) model checker, providing an environment for users engaged in model checking tasks. \ No newline at end of file diff --git a/tools/mc/kind2.md b/tools/mc/kind2.md new file mode 100644 index 0000000..d480625 --- /dev/null +++ b/tools/mc/kind2.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Kind 2' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://kind2-mc.github.io/kind2/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/kind2-mc/kind2", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['University of Iowa'] +licenses = ['Apache-2.0'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems. \ No newline at end of file diff --git a/tools/mc/ltsa.md b/tools/mc/ltsa.md new file mode 100644 index 0000000..52bbac5 --- /dev/null +++ b/tools/mc/ltsa.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'LTSA' +subtitle = 'Labelled Transition System Analyser' +links = [ + { title = "Homepage", url = "https://www.doc.ic.ac.uk/ltsa/", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['University of Twente'] +# licenses = ['BSD'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour. \ No newline at end of file diff --git a/tools/mc/mcltlrs.md b/tools/mc/mcltlrs.md new file mode 100644 index 0000000..2ab73e1 --- /dev/null +++ b/tools/mc/mcltlrs.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'mcltl-rs' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/NotBad4U/mcltl-rs", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['Fondazione Bruno Kessler'] +# licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} + +mcltl-rs is an experimental model checker for LTL written in Rust. \ No newline at end of file diff --git a/tools/mc/mercury.md b/tools/mc/mercury.md new file mode 100644 index 0000000..9428eb0 --- /dev/null +++ b/tools/mc/mercury.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Mercury' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/rtsaad/mercury", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['LAAS-CNRS', 'Vertics'] +licenses = ['MIT'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory. \ No newline at end of file diff --git a/tools/mc/nusmv.md b/tools/mc/nusmv.md new file mode 100644 index 0000000..84a336f --- /dev/null +++ b/tools/mc/nusmv.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'NuSMV' +subtitle = 'Symbolic Model Checker' +links = [ + { title = "Homepage", url = "https://nusmv.fbk.eu/index.html", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Fondazione Bruno Kessler'] +licenses = ['LGPL'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + +NuSMV is a symbolic model checker. \ No newline at end of file diff --git a/tools/mc/nuxmv.md b/tools/mc/nuxmv.md new file mode 100644 index 0000000..e0f663e --- /dev/null +++ b/tools/mc/nuxmv.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'NuXMV' +subtitle = 'Symbolic Model Checker' +links = [ + { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Fondazione Bruno Kessler'] +licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + +{{}} +nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems. \ No newline at end of file diff --git a/tools/mc/pnmc.md b/tools/mc/pnmc.md new file mode 100644 index 0000000..a020587 --- /dev/null +++ b/tools/mc/pnmc.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Pnmc' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['University of Twente'] +licenses = ['BSD'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +Pnmc is a symbolic model checker for Petri nets. \ No newline at end of file diff --git a/tools/mc/romeo.md b/tools/mc/romeo.md new file mode 100644 index 0000000..fd22dbe --- /dev/null +++ b/tools/mc/romeo.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Roméo' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://romeo.ls2n.fr/", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['University of Nantes'] +licenses = ['GPL'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + + +Romeo allows the modelling of complex systems using extensions of time Petri nets. \ No newline at end of file diff --git a/tools/mc/spin.md b/tools/mc/spin.md new file mode 100644 index 0000000..07fe3a8 --- /dev/null +++ b/tools/mc/spin.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Spin' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://spinroot.com/spin/whatispin.html", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/nimble-code/Spin", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Bell Labs'] +licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['PDR', 'CAR'] +# publications = [''] ++++ + +Spin is a model checker for multi-threaded software. \ No newline at end of file diff --git a/tools/mc/tapaal.md b/tools/mc/tapaal.md new file mode 100644 index 0000000..b499f22 --- /dev/null +++ b/tools/mc/tapaal.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'TAPAAL' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://www.tapaal.net/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Aalborg University'] +licenses = ['Open Source 3.0', 'BSD', 'GPLv2'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + + +TAPAAL is a tool for verification of timed-arc petri nets \ No newline at end of file diff --git a/tools/mc/timesolver.md b/tools/mc/timesolver.md new file mode 100644 index 0000000..a564532 --- /dev/null +++ b/tools/mc/timesolver.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'TimeSolver' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/jkeiren/TimeSolver", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = ['Fondazione Bruno Kessler'] +# licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems). \ No newline at end of file diff --git a/tools/mc/uppaal.md b/tools/mc/uppaal.md new file mode 100644 index 0000000..84700ca --- /dev/null +++ b/tools/mc/uppaal.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Uppaal' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://uppaal.org/", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Uppsala Universitet', 'Aalborg University'] +licenses = ['All Rights Reserved'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). \ No newline at end of file