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 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Thu 8 Nov
Displayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:00 | |||
10:30 22mTalk | 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 22mTalk | Gradual Liquid Type Inference OOPSLA Niki Vazou IMDEA Software Institute, Éric Tanter University of Chile & Inria Paris, David Van Horn University of Maryland, USA | ||
11:15 22mTalk | 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 22mTalk | 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 |