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

@@ 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