Typos

tools/mc/pdrlia.md

@@ -1,5 +1,5 @@
 +++
-title = ' PDR-LIA'
+title = 'PDR-LIA'
 subtitle = 'Reachability Analyzer'
 links = [	{ title = "Source Code", url = "https://github.com/akaydesai/PDR-LIA", icon = 'fa-solid fa-code' },
 ]

tools/mc/tina.md

@@ -0,0 +1,18 @@
++++
+title = 'TINA'
+subtitle = 'Petri Net Toolbox'
+links = [
+	{ title = "Homepage", url = "http://www.eecs.berkeley.edu/~alanmi/abc/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/berkeley-abc/abc", icon = 'fa-solid fa-code' },
+]
+applications = ["Petri Nets"]
+developers = []
+licenses = ["All Rights Reserved"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+TINA (TIme petri Net Analyzer) is a toolbox for the editing and analysis of Petri Nets, with possibly inhibitor and read arcs, Time Petri Nets, with possibly priorities and stopwatches, and an extension of Time Petri Nets with data handling called Time Transition Systems. TINA has been developed in the OLC, then VerTICS, research groups of LAAS/CNRS. General Petri nets information can be found on the Petri Nets World site. 

tools/prob/infamy.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'INFAMY'
+subtitle = 'Quantitative Verification Tool'
+links = [
+    { title = "Homepage", url = "https://depend.cs.uni-saarland.de/tools/infamy/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Saarland University']
+licenses = ['All Rights Reserved']
+inputs = ['PRISM']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Kwiatkowska2011']
++++
+
+{{<inactive year="2010">}}
+INFAMY is a tool with the purpose of model checking CSL formulae on infinite state Markov chains in continuous time.

tools/prob/modest.md

@@ -1,7 +1,7 @@
 +++
 date = 2025-06-07
 draft = false
-title = ' The Modest Toolset'
+title = 'Modest Toolset'
 subtitle = 'Quantitative Verification Suite'
 links = [
     { title = "Homepage", url = "https://www.modestchecker.net/", icon = 'fa-solid fa-home' },

tools/prob/oris.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ORIS Tool'
+subtitle = 'Petri Net Analysis'
+links = [
+    { title = "Homepage", url = "https://www.oris-tool.org/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker', 'Petri Net Analysis']
+developers = ['Università di Firenze']
+licenses = ['All Rights Reserved']
+inputs = ['ORIS']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Kwiatkowska2011']
++++
+
+<!-- {{<inactive year="2023">}} -->
+The Modest Toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems.

tools/prob/param.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'PARAM'
+subtitle = 'Quantitative Verification Tool'
+links = [
+    { title = "Homepage", url = "https://depend.cs.uni-saarland.de/tools/param/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Saarland University']
+licenses = ['All Rights Reserved']
+inputs = ['PRISM']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Kwiatkowska2011']
++++
+
+{{<inactive year="2011">}}
+PARAM is a tool with the purpose of handling parametric variants of models specified in a variant of the PRISM language. PARAM is capable of computing the unbounded reachability probability for parametric discrete-time Markov chains. 

tools/prob/pass.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'PASS'
+subtitle = 'Quantitative Verification Tool'
+links = [
+    { title = "Homepage", url = "https://depend.cs.uni-saarland.de/tools/pass/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Abstraction']
+developers = ['Saarland University']
+licenses = ['All Rights Reserved']
+inputs = ['PRISM']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Kwiatkowska2011']
++++
+
+{{<inactive year="2010">}}
+PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. Models are specified in a variant of the PRISM language. PASS computes the probability of reaching a set of goal states specified by the user.

tools/prob/prohver.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ProHVer'
+subtitle = 'Quantitative Verification Tool'
+links = [
+    { title = "Homepage", url = "https://depend.cs.uni-saarland.de/tools/prohver/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Saarland University']
+licenses = ['All Rights Reserved']
+inputs = ['PRISM']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Kwiatkowska2011']
++++
+
+{{<inactive year="2011">}}
+ProHVer is a tool to handle systems which feature both discrete and continuous behaviour, and also involves randomness. ProHVer is capable of computing the unbounded reachability probability for a very general class of probabilistic hybrid automata. This homepage presents the tool, as well as some case studies on which it was applied.

tools/programs/shuttle.md

@@ -1,7 +1,7 @@
 +++
 date = 2025-07-10
 draft = false
-title = 'Loom'
+title = 'Shuttle'
 subtitle = 'Rust Verifier'
 links = [
     # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },