Close #23

tools/mc/abc.md

@@ -0,0 +1,18 @@
++++
+title = 'ABC'
+subtitle = 'Sequential Logic Verifier'
+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 = ["Theorem Prover","Model Checker"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+System for Sequential Logic Synthesis and Formal Verification

tools/mc/avr.md

@@ -0,0 +1,16 @@
++++
+title = 'AVR'
+subtitle = 'Reachability Analysis'
+links = [	{ title = "Source Code", url = "https://github.com/aman-goel/avr", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+ Reads a state transition system and performs property checking 

tools/mc/fast-downward-pdr.md

@@ -0,0 +1,16 @@
++++
+title = 'Fast Downward PDR'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/Tiim/fast-downward-pdr", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+ Implementation of the Property-Directed Reachability algorithm in the Fast Downward planning system. 

tools/mc/fbpdr.md

@@ -0,0 +1,16 @@
++++
+title = 'fbPDR'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/tobiasseufert/fbPDR", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Forward / backward PDR/IC3 implementation.

tools/mc/fuseic3.md

@@ -0,0 +1,19 @@
++++
+title = 'FuseIC3'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/rohitdureja/FuseIC3", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2017
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2017">}}
+
+FuseIC3 is a SAT-based algorithm for checking a set of models. It extends IC3 to minimize time spent in exploring the common state space between related models.

tools/mc/geyser.md

@@ -1,21 +1,16 @@
 +++
-date = 2025-06-07
-draft = false
 title = 'Geyser'
-subtitle = 'Model Checker'
+subtitle = 'Reachability Analysis'
-links = [
+links = [	{ title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-solid fa-code' },
-    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-solid fa-code'  },
-    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
-applications = ['Model Checker']
+applications = ["Model Checker"]
-# developers = ['Eindhoven University of Technology']
+developers = []
-licenses = ['MIT']
+licenses = ["MIT"]
-# inputs = ['Sally']
+inputs = []
-# interfaces = ['CLI']
+interfaces = ["CLI"]
-maintenance = ['Actively Maintained']
+maintenance = ["Actively Maintained"]
-techniques = ['PDR', 'CAR']
+draft = false
-# publications = ['']
+date = 2025-08-22
 +++
 
-Geyser is a simple symbolic model checker for propositional transition system systems.
+ Simple implementation of PDR and CAR model checking algorithms 

tools/mc/pdrc.md

@@ -0,0 +1,16 @@
++++
+title = 'PDRC'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/Gy-Hu/PDRC", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+ Reproduce of "HVC2017: A Supervisory Control Algorithm Based on Property-Directed Reachability" 

tools/mc/pdrlia.md

@@ -0,0 +1,19 @@
++++
+title = ' PDR-LIA'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/akaydesai/PDR-LIA", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["CRAPL"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2018
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2018">}}
+
+ Implementation of Property Directed Reachability for linear integer arithmetic

tools/mc/reach.md

@@ -0,0 +1,16 @@
++++
+title = 'Reach'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/go-air/reach", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Reach is a symbolic finite state reachability checker. One could also say that Reach is a safety model checker.

tools/mc/ric3.md

@@ -0,0 +1,16 @@
++++
+title = 'rIC3'
+subtitle = 'Hardware Model Checker'
+links = [	{ title = "Source Code", url = "https://github.com/gipsyh/rIC3", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+ Hardware Formal Verification Tool 

tools/mc/simplepdr.md

@@ -0,0 +1,19 @@
++++
+title = 'SimplePDR'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/rohitdureja/SimplePDR", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2016
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2016">}}
+
+A reference implementation of property directed reachability for boolean transition systems.

tools/mc/z3ic3pdr.md

@@ -0,0 +1,19 @@
++++
+title = 'Z3-IC3-PDR'
+subtitle = 'Reachability Analyzer'
+links = [	{ title = "Source Code", url = "https://github.com/pddenhar/Z3-IC3-PDR", icon = 'fa-solid fa-code' },
+]
+applications = ["Model Checker"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2016
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2016">}}
+
+ Implementation of the IC3 / Property Directed Reachability algorithm using the the Z3 SMT solver.