Loop verification with invariants and contracts (Q2152642): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W4205272345
@@ Property / OpenAlex ID: W4205272345 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.05812
@@ Property / arXiv ID: 2010.05812 / rank @@
+Normal rank
@@ Property / cites work @@
+A unifying view on SMT-based software verification
+Normal rank
@@ Property / cites work @@
+Horn Clause Solvers for Program Verification
@@ Property / cites work: Horn Clause Solvers for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+An elementary and unified approach to program correctness
+Normal rank
@@ Property / cites work @@
+Automated Reasoning with Analytic Tableaux and Related Methods
+Normal rank
@@ Property / cites work @@
+Q5674963
@@ Property / cites work: Q5674963 / rank @@
+Normal rank
@@ Property / cites work @@
+HoIce: an ICE-based non-linear Horn clause solver
@@ Property / cites work: HoIce: an ICE-based non-linear Horn clause solver / rank @@
+Normal rank
@@ Property / cites work @@
+Program verification through characteristic formulae
+Normal rank
@@ Property / cites work @@
+Verifying Array Programs by Transforming Verification Conditions
+Normal rank
@@ Property / cites work @@
+Reverse Hoare Logic
@@ Property / cites work: Reverse Hoare Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified invariants via syntax-guided synthesis
@@ Property / cites work: Quantified invariants via syntax-guided synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Loop invariants
@@ Property / cites work: Loop invariants / rank @@
+Normal rank
@@ Property / cites work @@
+Inferring Loop Invariants Using Postconditions
@@ Property / cites work: Inferring Loop Invariants Using Postconditions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4493907
@@ Property / cites work: Q4493907 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement of Trace Abstraction
@@ Property / cites work: Refinement of Trace Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+A tutorial on the universality and expressiveness of fold
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Hoare-style logic for unstructured programs
@@ Property / cites work: Hoare-style logic for unstructured programs / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+The specification statement
@@ Property / cites work: The specification statement / rank @@
+Normal rank
@@ Property / cites work @@
+Transforming Programs into Recursive Functions
@@ Property / cites work: Transforming Programs into Recursive Functions / rank @@
+Normal rank
@@ Property / cites work @@
+Verified analysis of random binary tree structures
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Circular Coinduction: A Proof Theoretical Foundation
+Normal rank
@@ Property / cites work @@
+RGITL: a temporal logic framework for compositional reasoning about interleaved programs
+Normal rank
@@ Property / cites work @@
+Automating induction for solving Horn clauses
@@ Property / cites work: Automating induction for solving Horn clauses / rank @@
+Normal rank
@@ Property / cites work @@
+Intertwined Forward-Backward Reachability Analysis Using Interpolants
+Normal rank