On invariant synthesis for parametric systems (Q2305429): Difference between revisions

@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+REDLOG
@@ Property / describes a project that uses: REDLOG / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cubicle
@@ Property / describes a project that uses: Cubicle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+H-PILoT
@@ Property / describes a project that uses: H-PILoT / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2969349375
@@ Property / OpenAlex ID: W2969349375 / rank @@
+Normal rank
@@ Property / cites work @@
+An extension of lazy abstraction with interpolation for programs with arrays
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving for hierarchic first-order theories
+Normal rank
@@ Property / cites work @@
+Invariant Synthesis for Combined Theories
@@ Property / cites work: Invariant Synthesis for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Property-directed incremental invariant generation
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Quantifier-free interpolation in combinations of equality interpolating theories
+Normal rank
@@ Property / cites work @@
+Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
+Normal rank
@@ Property / cites work @@
+When Is a Formula a Loop Invariant?
@@ Property / cites work: When Is a Formula a Loop Invariant? / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Modular proof systems for partial functions with Evans equality
+Normal rank
@@ Property / cites work @@
+Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
+Normal rank
@@ Property / cites work @@
+Loop Analysis by Quantification over Iterations
@@ Property / cites work: Loop Analysis by Quantification over Iterations / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifiers on demand
@@ Property / cites work: Quantifiers on demand / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination in Vampire
@@ Property / cites work: Interpolation and Symbol Elimination in Vampire / rank @@
+Normal rank
@@ Property / cites work @@
+Obtaining Finite Local Theory Axiomatizations via Saturation
+Normal rank
@@ Property / cites work @@
+Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
+Normal rank
@@ Property / cites work @@
+Deciding the Inductive Validity of ∀ ∃ * Queries
+Normal rank
@@ Property / cites work @@
+On Local Reasoning in Verification
@@ Property / cites work: On Local Reasoning in Verification / rank @@
+Normal rank
@@ Property / cites work @@
+On Hierarchical Reasoning in Combinations of Theories
+Normal rank
@@ Property / cites work @@
+Towards Complete Reasoning about Axiomatic Specifications
+Normal rank
@@ Property / cites work @@
+A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
+Normal rank
@@ Property / cites work @@
+Property-Directed Inference of Universal Invariants or Proving Their Absence
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / 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 @@
+On invariant synthesis for parametric systems
@@ Property / cites work: On invariant synthesis for parametric systems / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation in Local Theory Extensions
@@ Property / cites work: Interpolation in Local Theory Extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation in local theory extensions
@@ Property / cites work: Interpolation in local theory extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Hierarchical Reasoning for the Verification of Parametric Systems
+Normal rank
@@ Property / cites work @@
+Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
+Normal rank
@@ Property / cites work @@
+On Interpolation and Symbol Elimination in Theory Extensions
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank