Verifying Array Manipulating Programs with Full-Program Induction (Q5039501): Difference between revisions

@@ Property / describes a project that uses @@
+FunArray
@@ Property / describes a project that uses: FunArray / 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 / describes a project that uses @@
+Houdini
@@ Property / describes a project that uses: Houdini / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VeriFast
@@ Property / describes a project that uses: VeriFast / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Daikon
@@ Property / describes a project that uses: Daikon / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Aligators
@@ Property / describes a project that uses: Aligators / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3013666522
@@ Property / OpenAlex ID: W3013666522 / 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 @@
+Verifying Array Manipulating Programs by Tiling
@@ Property / cites work: Verifying Array Manipulating Programs by Tiling / rank @@
+Normal rank
@@ Property / cites work @@
+Bounded model checking using satisfiability solving
+Normal rank
@@ Property / cites work @@
+A parametric segmentation functor for fully automatic and scalable array content analysis
+Normal rank
@@ Property / cites work @@
+The Daikon system for dynamic detection of likely invariants
+Normal rank
@@ Property / cites work @@
+The program dependence graph and its use in optimization
+Normal rank
@@ Property / cites work @@
+Q2763999
@@ Property / cites work: Q2763999 / 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 @@
+Aligators for Arrays (Tool Paper)
@@ Property / cites work: Aligators for Arrays (Tool Paper) / rank @@
+Normal rank
@@ Property / cites work @@
+Array Abstractions from Proofs
@@ Property / cites work: Array Abstractions from Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Abstraction of Arrays Based on Non Contiguous Partitions
+Normal rank
@@ Property / cites work @@
+Cell morphing: from array programs to array-free Horn clauses
+Normal rank
@@ Property / cites work @@
+Simplifying the Verification of Quantified Array Assertions via Code Transformation
+Normal rank