ICE-based refinement type discovery for higher-order functional programs (Q5919002): 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 @@
+c2i
@@ Property / describes a project that uses: c2i / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Kind 2
@@ Property / describes a project that uses: Kind 2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Spacer
@@ Property / describes a project that uses: Spacer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Eldarica
@@ Property / describes a project that uses: Eldarica / 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 @@
+Princess
@@ Property / describes a project that uses: Princess / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HMC
@@ Property / describes a project that uses: HMC / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-020-09571-y
+Normal rank
@@ Property / OpenAlex ID @@
+W3046473740
@@ Property / OpenAlex ID: W3046473740 / rank @@
+Normal rank
@@ Property / cites work @@
+Computational Complexity
@@ Property / cites work: Computational Complexity / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings
+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 @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+ICE-based refinement type discovery for higher-order functional programs
+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 @@
+Solving Horn Clauses on Inductive Data Types Without Induction
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+SMT-based model checking for recursive programs
@@ Property / cites work: SMT-based model checking for recursive programs / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Termination Verification for Higher-Order Functional Programs
+Normal rank
@@ Property / cites work @@
+Q4255591
@@ Property / cites work: Q4255591 / rank @@
+Normal rank
@@ Property / cites work @@
+Low-level liquid types
@@ Property / cites work: Low-level liquid types / rank @@
+Normal rank
@@ Property / cites work @@
+From invariant checking to invariant inference using randomized search
+Normal rank
@@ Property / cites work @@
+A Data Driven Approach for Algebraic Loop Invariants
+Normal rank
@@ Property / cites work @@
+Dependent types from counterexamples
@@ Property / cites work: Dependent types from counterexamples / rank @@
+Normal rank
@@ Property / cites work @@
+Automating relatively complete verification of higher-order functional programs
+Normal rank
@@ Property / cites work @@
+Compositional and Lightweight Dependent Type Inference for ML
+Normal rank
@@ Property / cites work @@
+Dependent Array Type Inference from Tests
@@ Property / cites work: Dependent Array Type Inference from Tests / rank @@
+Normal rank
@@ Property / cites work @@
+Learning refinement types
@@ Property / cites work: Learning refinement types / rank @@
+Normal rank