Learning refinement types

No abstract is available for this paper.

• Publication year

  2015

• Venue

  ACM SIGPLAN International Conference on Functional Programming

• Publication date

  2015-08-29

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2784731.2784766
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A type-directed abstraction refinement approach to higher-order model checking

  2014cited by this paper
• From invariant checking to invariant inference using randomized search

  2014cited by this paper
• Type Targeted Testing

  2014cited by this paper
• Relatively complete counterexamples for higher-order programs

  2014cited by this paper
• ICE: A Robust Framework for Learning Invariants

  2014cited by this paper
• Abstract Refinement Types

  2013cited by this paper
• ICE: A Robust Learning Framework for Synthesizing Invariants

  2013cited by this paper
• Verifying higher-order programs with the dijkstra monad

  2013cited by this paper
• Compositional and Lightweight Dependent Type Inference for ML

  2013cited by this paper
• Automating relatively complete verification of higher-order functional programs

  2013cited by this paper
• Verification as Learning Geometric Concepts

  2013cited by this paper
• Beautiful Interpolants

  2013cited by this paper
• A Data Driven Approach for Algebraic Loop Invariants

  2013cited by this paper
• Hasochism: the pleasure and pain of dependently typed haskell programming

  2013cited by this paper
• Nested refinements: a logic for duck typing

  2012cited by this paper
• Using dynamic analysis to discover polynomial and array invariants

  2012cited by this paper
• Interpolants as Classifiers

  2012cited by this paper
• Testing Container Classes: Random or Systematic?

  2011cited by this paper
• Integrating Testing and Interactive Theorem Proving

  2011cited by this paper
• Predicate abstraction and CEGAR for higher-order model checking

  2011influential reference
• HMC: Verifying Functional Programs Using Abstract Interpreters

  2010cited by this paper
• Dependent types from counterexamples

  2010cited by this paper
• CPAchecker: A Tool for Configurable Software Verification

  2009cited by this paper
• Type-based data structure verification

  2009cited by this paper
• Dependent type inference with interpolants

  2009cited by this paper
• Types and higher-order recursion schemes for verification of higher-order programs

  2009cited by this paper
• Ynot

  2008cited by this paper
• Liquid types

  2008influential reference
• The Daikon system for dynamic detection of likely invariants

  2007cited by this paper
• SYNERGY: a new algorithm for property checking

  2006cited by this paper
• An interpolating theorem prover

  2005cited by this paper
• Abstractions from proofs

  2004cited by this paper
• Counterexample-guided abstraction refinement for symbolic model checking

  2003cited by this paper
• Faking it Simulating dependent types in Haskell

  2002cited by this paper
• Library

  2002cited by this paper
• Korat: automated testing based on Java predicates

  2002cited by this paper
• Houdini, an Annotation Assistant for ESC/Java

  2001cited by this paper
• QuickCheck: a lightweight tool for random testing of Haskell programs

  2000influential reference
• Dependent types in practical programming

  1999cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• Techniques for program verification

  1979cited by this paper
• Minimization of Boolean Functions

  1971cited by this paper

• Practical Refinement Session Type Inference (Extended Version)

  2026cites this paper
• LLM For Loop Invariant Generation and Fixing: How Far Are We?

  2025cites this paper
• Solvable Tuple Patterns and Their Applications to Program Verification

  2025cites this paper
• Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference

  2025cites this paper
• Counterexample-Guided Inference of Modular Specifications

  2025cites this paper
• LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference

  2024cites this paper
• HFL(Z) Validity Checking for Automated Program Verification

  2023cites this paper
• Higher-Order Property-Directed Reachability

  2023cites this paper
• Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning

  2023cites this paper
• Automatic HFL(Z) Validity Checking for Program Verification

  2022cites this paper
• Constraint-based Relational Verification

  2021cites this paper
• Toward Neural-Network-Guided Program Synthesis and Verification

  2021cites this paper
• Observational Abstract Interpreters

  2020cites this paper
• Program Verification via Predicate Constraint Satisfiability Modulo Theories

  2020cites this paper
• A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

  2020cites this paper
• Interval counterexamples for loop invariant learning

  2020cites this paper
• Data flow refinement type inference

  2020cites this paper
• Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking

  2020cites this paper
• Declarative and Algorithmic Implementation of Refinement Types

  2019cites this paper
• ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

  2018cites this paper
• A Fixpoint Logic and Dependent Effects for Temporal Property Verification

  2018cites this paper
• Relatively complete refinement type system for verification of higher-order non-deterministic programs

  2017cites this paper
• Horn-ICE learning for synthesizing invariants and contracts

  2017cites this paper
• Abduction by Non-Experts

  2017cites this paper
• Modular Verification of Higher-Order Functional Programs

  2017influential citation
• Automatically generating features for learning program analysis heuristics for C-like languages

  2017cites this paper
• Invariant Synthesis for Incomplete Verification Engines

  2017cites this paper
• Local refinement typing

  2017cites this paper
• Higher-Order Program Verification via HFL Model Checking

  2017cites this paper
• Automatically learning shape specifications

  2016influential citation
• Learning Program Specifications from Sample Runs

  2016cites this paper
• Automatically generating features for learning program analysis heuristics

  2016cites this paper
• Automatically disproving fair termination of higher-order functional programs

  2016cites this paper