\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-030-72013-1_12
+Normal rank
@@ Property / OpenAlex ID @@
+W3137055701
@@ Property / OpenAlex ID: W3137055701 / rank @@
+Normal rank
@@ Property / cites work @@
+A verified proof checker for higher-order logic
@@ Property / cites work: A verified proof checker for higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Generating extended resolution proofs with a BDD-based SAT solver
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+Formally verifying the solution to the Boolean Pythagorean triples problem
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Verified Characteristic Formulae for CakeML
@@ Property / cites work: Verified Characteristic Formulae for CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient, verified checking of propositional proofs
+Normal rank
@@ Property / cites work @@
+What a difference a variable makes
@@ Property / cites work: What a difference a variable makes / rank @@
+Normal rank
@@ Property / cites work @@
+Strong extension-free proof systems
@@ Property / cites work: Strong extension-free proof systems / rank @@
+Normal rank
@@ Property / cites work @@
+Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
+Normal rank
@@ Property / cites work @@
+Inprocessing Rules
@@ Property / cites work: Inprocessing Rules / rank @@
+Normal rank
@@ Property / cites work @@
+Extended resolution simulates \({\mathsf{DRAT}}\)
@@ Property / cites work: Extended resolution simulates \({\mathsf{DRAT}}\) / rank @@
+Normal rank
@@ Property / cites work @@
+Computer-aided proof of Erdős discrepancy properties
+Normal rank
@@ Property / cites work @@
+Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Proof-producing translation of higher-order logic into pure and stateful ML
+Normal rank
@@ Property / cites work @@
+versat: A Verified Modern SAT Solver
@@ Property / cites work: versat: A Verified Modern SAT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+The verified CakeML compiler backend
@@ Property / cites work: The verified CakeML compiler backend / rank @@
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank