What’s Decidable About Program Verification Modulo Axioms? (Q5164172): Difference between revisions

@@ Property / cites work @@
+Deductive verification in decidable fragments with Ivy
+Normal rank
@@ Property / cites work @@
+Graph minors. I. Excluding a forest
@@ Property / cites work: Graph minors. I. Excluding a forest / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive Unsolvability of a problem of Thue
@@ Property / cites work: Recursive Unsolvability of a problem of Thue / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848689
@@ Property / cites work: Q2848689 / rank @@
+Normal rank
@@ Property / cites work @@
+Decidability of inferring inductive invariants
@@ Property / cites work: Decidability of inferring inductive invariants / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+The tree width of auxiliary storage
@@ Property / cites work: The tree width of auxiliary storage / rank @@
+Normal rank
@@ Property / cites work @@
+Complexity results for classes of quantificational formulas
+Normal rank
@@ Property / cites work @@
+Kleene Algebra with Equations
@@ Property / cites work: Kleene Algebra with Equations / rank @@
+Normal rank
@@ Property / cites work @@
+Q4362921
@@ Property / cites work: Q4362921 / rank @@
+Normal rank
@@ Property / cites work @@
+Modular reasoning about heap paths via effectively propositional formulas
+Normal rank
@@ Property / cites work @@
+Nested interpolants
@@ Property / cites work: Nested interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement of Trace Abstraction
@@ Property / cites work: Refinement of Trace Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Assertion Checking Unified
@@ Property / cites work: Assertion Checking Unified / rank @@
+Normal rank
@@ Property / cites work @@
+Invariant Checking for Programs with Procedure Calls
+Normal rank
@@ Property / cites work @@
+Proof Spaces for Unbounded Parallelism
@@ Property / cites work: Proof Spaces for Unbounded Parallelism / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs that count
@@ Property / cites work: Proofs that count / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive data flow graphs
@@ Property / cites work: Inductive data flow graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Kleene algebra with hypotheses
@@ Property / cites work: Kleene algebra with hypotheses / rank @@
+Normal rank
@@ Property / cites work @@
+Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth
+Normal rank
@@ Property / cites work @@
+Algorithms for algebraic path properties in concurrent systems of constant treewidth components
+Normal rank
@@ Property / cites work @@
+EUFORIA: complete software model checking with uninterpreted functions
+Normal rank
@@ Property / cites work @@
+Q4804887
@@ Property / cites work: Q4804887 / rank @@
+Normal rank
@@ Property / cites work @@
+Structural Abstraction of Software Verification Conditions
+Normal rank
@@ Property / cites work @@
+Reveal: A Formal Verification Tool for Verilog Designs
+Normal rank