| | Refinement Modeling and Verification of RISC-V Assembly Using Knuckledragger (philipzucker.com) |
| 11 points by matt_d 10 days ago | past | discuss |
|
| | Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping (philipzucker.com) |
| 20 points by matt_d 12 days ago | past | 2 comments |
|
| | Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping (philipzucker.com) |
| 3 points by todsacerdoti 13 days ago | past | discuss |
|
| | SMTLIB as a Compiler IR I (philipzucker.com) |
| 1 point by matt_d 40 days ago | past |
|
| | Calling Lean Functions as Python Functions – Hey There Buddo (philipzucker.com) |
| 2 points by rbanffy 43 days ago | past |
|
| | Calling Lean Functions as Python Functions (philipzucker.com) |
| 3 points by todsacerdoti 44 days ago | past |
|
| | SMTMSMT: Gluing Together CVC5 and Z3 Nelson Oppen Style (philipzucker.com) |
| 1 point by matt_d 81 days ago | past |
|
| | SAT Etudes 2: Toy DPLL (philipzucker.com) |
| 1 point by matt_d 3 months ago | past |
|
| | A Slotted Hash Cons for Alpha Invariance (philipzucker.com) |
| 1 point by g0xA52A2A 6 months ago | past |
|
| | Compositional Datalog on SQL: Relational Algebra of the Environment (philipzucker.com) |
| 47 points by philzook 6 months ago | past | 3 comments |
|
| | Compositional Datalog on SQL: Relational Algebra of the Environment (philipzucker.com) |
| 3 points by Bogdanp 6 months ago | past |
|
| | A Python CLI for Verifying Assembly (philipzucker.com) |
| 1 point by philzook 7 months ago | past |
|
| | A Python CLI for Verifying Assembly (philipzucker.com) |
| 2 points by matt_d 7 months ago | past |
|
| | Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1 (philipzucker.com) |
| 2 points by matt_d 7 months ago | past |
|
| | Verified Assembly 2: Memory, RISC-V, Cuts for Invariants, and Ghost Code (philipzucker.com) |
| 3 points by todsacerdoti 7 months ago | past |
|
| | Semi-Automated Assembly Verification in Python Using Pypcode Semantics (philipzucker.com) |
| 2 points by matt_d 8 months ago | past |
|
| | Inequality Union Finds: Baby Steps to Refinement E-Graphs (philipzucker.com) |
| 1 point by todsacerdoti 8 months ago | past |
|
| | A Python frozenset interpretation of dependent type theory (philipzucker.com) |
| 2 points by fanf2 8 months ago | past |
|
| | Telescopes Are Tries: A Dependent Type Shellac on SQLite (philipzucker.com) |
| 16 points by matt_d 9 months ago | past |
|
| | Brute E-Graphs Modulo Theories 2: Extraction, Proofs, and Context (philipzucker.com) |
| 1 point by matt_d 9 months ago | past |
|
| | A Python Frozenset Interpretation of Dependent Type Theory (philipzucker.com) |
| 5 points by philzook 10 months ago | past |
|
| | "Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra (philipzucker.com) |
| 2 points by philzook 11 months ago | past |
|
| | A Small Prolog on the Z3 AST (philipzucker.com) |
| 3 points by philzook 11 months ago | past |
|
| | Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com) |
| 5 points by PaulHoule on Feb 22, 2025 | past |
|
| | Where are all the rewrite rules? (philipzucker.com) |
| 59 points by todsacerdoti on Feb 19, 2025 | past | 29 comments |
|
| | Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com) |
| 10 points by todsacerdoti on Feb 11, 2025 | past | 1 comment |
|
| | SAT Solver Etudes I (philipzucker.com) |
| 45 points by mathgenius on Jan 7, 2025 | past | 30 comments |
|
| | Symbolic Execution by Overloading __bool__ (philipzucker.com) |
| 81 points by philzook on Dec 24, 2024 | past | 10 comments |
|
| | Superposition as a Super Datalog (philipzucker.com) |
| 3 points by iamwil on Dec 2, 2024 | past |
|
| | SQL, Homomorphisms and Constraint Satisfaction Problems (philipzucker.com) |
| 153 points by xlinux on Nov 20, 2024 | past | 19 comments |
|
|
| More |
