Building program construction and verification tools from algebraic principles (Q736461): Difference between revisions

@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Verification of sequential and concurrent programs
+Normal rank
@@ Property / cites work @@
+Internal axioms for domain semirings
@@ Property / cites work: Internal axioms for domain semirings / rank @@
+Normal rank
@@ Property / cites work @@
+Algebras for Program Correctness in Isabelle/HOL
@@ Property / cites work: Algebras for Program Correctness in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+A refinement strategy for Circus
@@ Property / cites work: A refinement strategy for Circus / rank @@
+Normal rank
@@ Property / cites work @@
+On Hoare logic and Kleene algebra with tests
@@ Property / cites work: On Hoare logic and Kleene algebra with tests / rank @@
+Normal rank
@@ Property / cites work @@
+Programming and automating mathematics in the Tarski-Kleene hierarchy
+Normal rank
@@ Property / cites work @@
+Automated Reasoning in Higher-Order Regular Algebra
+Normal rank
@@ Property / cites work @@
+Winskel is (almost) right: Towards a mechanized semantics textbook
+Normal rank
@@ Property / cites work @@
+Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+An Efficient Coq Tactic for Deciding Kleene Algebras
+Normal rank
@@ Property / cites work @@
+A Program Construction and Verification Tool for Separation Logic
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning in Kleene Algebra
@@ Property / cites work: Automated Reasoning in Kleene Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Hoare logic and auxiliary variables
@@ Property / cites work: Hoare logic and auxiliary variables / rank @@
+Normal rank
@@ Property / cites work @@
+Q4362921
@@ Property / cites work: Q4362921 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767087
@@ Property / cites work: Q2767087 / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Q4301161
@@ Property / cites work: Q4301161 / rank @@
+Normal rank
@@ Property / cites work @@
+Algebras of modal operators and partial correctness
+Normal rank
@@ Property / cites work @@
+Relational Methods in Computer Science
@@ Property / cites work: Relational Methods in Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Q4411818
@@ Property / cites work: Q4411818 / rank @@
+Normal rank
@@ Property / cites work @@
+Hoare type theory, polymorphism and separation
@@ Property / cites work: Hoare type theory, polymorphism and separation / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Kleene Algebra with Tests and Coq Tools for while Programs
+Normal rank
@@ Property / cites work @@
+Certification of Nontermination Proofs
@@ Property / cites work: Certification of Nontermination Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3969890
@@ Property / cites work: Q3969890 / rank @@
+Normal rank