\textsc{Diffy}: inductive reasoning of array programs using difference invariants (Q832320): Difference between revisions

@@ Property / describes a project that uses @@
+FLATA
@@ Property / describes a project that uses: FLATA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FunArray
@@ Property / describes a project that uses: FunArray / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoVaC
@@ Property / describes a project that uses: CoVaC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Booster
@@ Property / describes a project that uses: Booster / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3183515470
@@ Property / OpenAlex ID: W3183515470 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.14748
@@ Property / arXiv ID: 2105.14748 / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants for Arrays
@@ Property / cites work: Lazy Abstraction with Interpolants for Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Booster: An Acceleration-Based Verification Framework for Array Programs
+Normal rank
@@ Property / cites work @@
+Invariant Synthesis for Combined Theories
@@ Property / cites work: Invariant Synthesis for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Acceleration of Ultimately Periodic Relations
+Normal rank
@@ Property / cites work @@
+Verifying Array Manipulating Programs by Tiling
@@ Property / cites work: Verifying Array Manipulating Programs by Tiling / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Array Manipulating Programs with Full-Program Induction
+Normal rank
@@ Property / cites work @@
+A parametric segmentation functor for fully automatic and scalable array content analysis
+Normal rank
@@ Property / cites work @@
+Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
+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 @@
+Predicate abstraction for software verification
@@ Property / cites work: Predicate abstraction for software verification / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for numeric analysis of array operations
+Normal rank
@@ Property / cites work @@
+Lifting abstract interpreters to quantified logical domains
+Normal rank
@@ Property / cites work @@
+Quantifiers on demand
@@ Property / cites work: Quantifiers on demand / rank @@
+Normal rank
@@ Property / cites work @@
+Putting the squeeze on array programs: loop verification via inductive rank reduction
+Normal rank
@@ Property / cites work @@
+Abstract acceleration of general linear loops
@@ Property / cites work: Abstract acceleration of general linear loops / rank @@
+Normal rank
@@ Property / cites work @@
+Array Abstractions from Proofs
@@ Property / cites work: Array Abstractions from Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+A formalization of programs in first-order logic with a discrete linear order
+Normal rank
@@ Property / cites work @@
+Abstraction of Arrays Based on Non Contiguous Partitions
+Normal rank
@@ Property / cites work @@
+Counterexample-guided prophecy for model checking modulo the theory of arrays
+Normal rank
@@ Property / cites work @@
+Cell morphing: from array programs to array-free Horn clauses
+Normal rank
@@ Property / cites work @@
+Finite Differencing of Computable Expressions
@@ Property / cites work: Finite Differencing of Computable Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+Simplifying the Verification of Quantified Array Assertions via Code Transformation
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank