A framework for the verification of certifying computations (Q2351144): Difference between revisions

@@ Property / describes a project that uses @@
+Maximum Cardinality Matching
@@ Property / describes a project that uses: Maximum Cardinality Matching / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Caduceus
@@ Property / describes a project that uses: Caduceus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL-Boogie
@@ Property / describes a project that uses: HOL-Boogie / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KRAKATOA
@@ Property / describes a project that uses: KRAKATOA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CeTA
@@ Property / describes a project that uses: CeTA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ShortestPath
@@ Property / describes a project that uses: ShortestPath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEDA
@@ Property / describes a project that uses: LEDA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VCC
@@ Property / describes a project that uses: VCC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Dijkstra Shortest Path
@@ Property / describes a project that uses: Dijkstra Shortest Path / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2001092196
@@ Property / OpenAlex ID: W2001092196 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.7462
@@ Property / arXiv ID: 1301.7462 / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Coq with Imperative Features and Its Application to SAT Verification
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Designing programs that check their work
@@ Property / cites work: Designing programs that check their work / rank @@
+Normal rank
@@ Property / cites work @@
+Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
+Normal rank
@@ Property / cites work @@
+HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
+Normal rank
@@ Property / cites work @@
+HOL-Boogie -- an interactive prover-backend for the verifying C compiler
+Normal rank
@@ Property / cites work @@
+Q3490989
@@ Property / cites work: Q3490989 / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Characteristic formulae for the verification of imperative programs
+Normal rank
@@ Property / cites work @@
+Maximum matching and a polyhedron with 0,1-vertices
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Bridging the Gap: Automatic Verified Abstraction of C
+Normal rank
@@ Property / cites work @@
+Certifying algorithms
@@ Property / cites work: Certifying algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Q4702188
@@ Property / cites work: Q4702188 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Certification of Termination Proofs Using CeTA
@@ Property / cites work: Certification of Termination Proofs Using CeTA / rank @@
+Normal rank