From d63b97d62bab7b371643c48f91416adbc4bf029f Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Fri, 22 Aug 2025 13:24:48 -0600 Subject: [PATCH] Close #23 --- tools/mc/abc.md | 18 ++++++++++++++++++ tools/mc/avr.md | 16 ++++++++++++++++ tools/mc/fast-downward-pdr.md | 16 ++++++++++++++++ tools/mc/fbpdr.md | 16 ++++++++++++++++ tools/mc/fuseic3.md | 19 +++++++++++++++++++ tools/mc/geyser.md | 27 +++++++++++---------------- tools/mc/pdrc.md | 16 ++++++++++++++++ tools/mc/pdrlia.md | 19 +++++++++++++++++++ tools/mc/reach.md | 16 ++++++++++++++++ tools/mc/ric3.md | 16 ++++++++++++++++ tools/mc/simplepdr.md | 19 +++++++++++++++++++ tools/mc/z3ic3pdr.md | 19 +++++++++++++++++++ 12 files changed, 201 insertions(+), 16 deletions(-) create mode 100644 tools/mc/abc.md create mode 100644 tools/mc/avr.md create mode 100644 tools/mc/fast-downward-pdr.md create mode 100644 tools/mc/fbpdr.md create mode 100644 tools/mc/fuseic3.md create mode 100644 tools/mc/pdrc.md create mode 100644 tools/mc/pdrlia.md create mode 100644 tools/mc/reach.md create mode 100644 tools/mc/ric3.md create mode 100644 tools/mc/simplepdr.md create mode 100644 tools/mc/z3ic3pdr.md diff --git a/tools/mc/abc.md b/tools/mc/abc.md new file mode 100644 index 0000000..d7e080a --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tools/mc/avr.md b/tools/mc/avr.md new file mode 100644 index 0000000..0d4d91b --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tools/mc/fast-downward-pdr.md b/tools/mc/fast-downward-pdr.md new file mode 100644 index 0000000..18e51c4 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/mc/fbpdr.md b/tools/mc/fbpdr.md new file mode 100644 index 0000000..6d8124e --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/mc/fuseic3.md b/tools/mc/fuseic3.md new file mode 100644 index 0000000..e9b60c6 --- /dev/null +++ b/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 ++++ + +{{}} + +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. \ No newline at end of file diff --git a/tools/mc/geyser.md b/tools/mc/geyser.md index 860f64f..4a19c7f 100644 --- a/tools/mc/geyser.md +++ b/tools/mc/geyser.md @@ -1,21 +1,16 @@ +++ -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-solid fa-code' }, - # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +subtitle = 'Reachability Analysis' +links = [ { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-solid fa-code' }, ] -applications = ['Model Checker'] -# developers = ['Eindhoven University of Technology'] -licenses = ['MIT'] -# inputs = ['Sally'] -# interfaces = ['CLI'] -maintenance = ['Actively Maintained'] -techniques = ['PDR', 'CAR'] -# publications = [''] +applications = ["Model Checker"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 +++ -Geyser is a simple symbolic model checker for propositional transition system systems. \ No newline at end of file + Simple implementation of PDR and CAR model checking algorithms \ No newline at end of file diff --git a/tools/mc/pdrc.md b/tools/mc/pdrc.md new file mode 100644 index 0000000..619c87d --- /dev/null +++ b/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" \ No newline at end of file diff --git a/tools/mc/pdrlia.md b/tools/mc/pdrlia.md new file mode 100644 index 0000000..7b14d93 --- /dev/null +++ b/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 ++++ + +{{}} + + Implementation of Property Directed Reachability for linear integer arithmetic \ No newline at end of file diff --git a/tools/mc/reach.md b/tools/mc/reach.md new file mode 100644 index 0000000..f3c8933 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/mc/ric3.md b/tools/mc/ric3.md new file mode 100644 index 0000000..b6fbf18 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tools/mc/simplepdr.md b/tools/mc/simplepdr.md new file mode 100644 index 0000000..75db59b --- /dev/null +++ b/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 ++++ + +{{}} + +A reference implementation of property directed reachability for boolean transition systems. \ No newline at end of file diff --git a/tools/mc/z3ic3pdr.md b/tools/mc/z3ic3pdr.md new file mode 100644 index 0000000..1a852ff --- /dev/null +++ b/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 ++++ + +{{}} + + Implementation of the IC3 / Property Directed Reachability algorithm using the the Z3 SMT solver. \ No newline at end of file