Code repositories: Difference between revisions
Jump to navigation
Jump to search
(Created page with "This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them. * [https://github.com/bbchallenge/bbchallenge-deciders The official bbchallenge deciders repo] * [https://github.com/ccz181078/Coq-BB5 Coq-BB5 by @mxdys] * [https://github.com/meithecatte/busycoq A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei]...") |
No edit summary |
||
| Line 12: | Line 12: | ||
* [https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Bouncers decider, by @savask] | * [https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Bouncers decider, by @savask] | ||
* [https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Reproduction of mxdys' repeated blocks decider, by @savask] | * [https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Reproduction of mxdys' repeated blocks decider, by @savask] | ||
* [https://github.com/savask/turing Collection of deciders by @savask] | |||
* [https://github.com/colette-b/bbchallenge The first SAT-based CTL/FAR decider, by @djmati1111] | * [https://github.com/colette-b/bbchallenge The first SAT-based CTL/FAR decider, by @djmati1111] | ||
* [https://github.com/FransFaase/SymbolicTM An early CTL verifier (regex-based) by Frans Faase] | * [https://github.com/FransFaase/SymbolicTM An early CTL verifier (regex-based) by Frans Faase] | ||
Revision as of 19:57, 4 June 2024
This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them.
- The official bbchallenge deciders repo
- Coq-BB5 by @mxdys
- A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei
- bbfind by Skelet wrapped via bbfind-stdin by @wizord
- Accelerated TM simulators in Python utilizing memoization (like HashLife), by @Mateon1
- Forward segment TM decider by @Mateon1 (variant of Halting Segment)
- Closed Position Set (CPS) TM decider by @Mateon1
- SAT Solver CTL code by @Mateon1; TODO dependencies still in Discord posts
- The closed position set decider, reverse-engineered from Skelet's program, by @savask
- Bouncers decider, by @savask
- Reproduction of mxdys' repeated blocks decider, by @savask
- Collection of deciders by @savask
- The first SAT-based CTL/FAR decider, by @djmati1111
- An early CTL verifier (regex-based) by Frans Faase
- Bouncers decider, by @Iijil
- Bruteforce-CTL decider, by @Iijil
- Meet-in-the-Middle Weighted Finite Automata... Reduction... by @Iijil
- Some progress toward a FAR verifier checked by Lean, by @-d
- An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978
- Deciders formally verified using Dafny, by @nathanf
- CTL decider by @nathanf
- A dramatic simplification of CPS (much less resource-intensive and not as strong) by @nathanf
- A formally verified CTL checker by @nathanf
- https://github.com/nickdrozd/busy-beaver-stuff
- https://github.com/phinanix/busy-beavers
- https://github.com/sligocki/busy-beaver
- https://github.com/TonyGuil/bbchallenge
- https://github.com/uncombedcoconut/bbchallenge
- https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction
- https://github.com/UncombedCoconut/bbchallenge-nfa-verification
- https://github.com/univerz/bbc