Thu 8 Nov 2018 10:30 - 10:52 at Studio 2 - Types and Contracts Chair(s): Hakjoo Oh

We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from non-linear Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using nonlinear Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.

Thu 8 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Types and ContractsOOPSLA at Studio 2
Chair(s): Hakjoo Oh Korea University
10:30
22m
Talk
Horn-ICE Learning for Synthesizing Invariants and Contracts
OOPSLA
Deepak D'Souza , Ezudheen P , Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider Max Planck Institute for Software Systems, P. Madhusudan University of Illinois at Urbana-Champaign
10:52
22m
Talk
Gradual Liquid Type InferenceDistinguished Paper Award
OOPSLA
Niki Vazou IMDEA Software Institute, √Čric Tanter University of Chile & Inria Paris, David Van Horn University of Maryland, USA
11:15
22m
Talk
Collapsible Contracts: Fixing a Pathology of Gradual Typing
OOPSLA
Daniel Feltey Northwestern University, USA, Ben Greenman Northeastern University, USA, Christophe Scholliers Universiteit Gent, Belgium, Robert Bruce Findler Northwestern University, USA, Vincent St-Amour Northwestern University
11:37
22m
Talk
The Root Cause of Blame: Contracts for Intersection and Union Types
OOPSLA
Jack Williams University of Edinburgh, UK, J. Garrett Morris University of Kansas, USA, Philip Wadler University of Edinburgh, UK