Files in this item

FilesDescriptionFormat

application/pdf

application/pdfmain.pdf (597kB)
(no description provided)PDF

Description

Title:Learning Invariants using Decision Trees and Implication Counterexamples
Author(s):Garg, Pranav; Neider, Daniel; Madhusudan, P.; Roth, Dan
Subject(s):verification
invariant synthesis
machine learning
Abstract:Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counter-examples that are based on scalable machine learning techniques. In particular, we extend decision tree learning algorithms, building new scalable and heuristic ways to construct small decision trees using statistical measures that account for implication counterexamples. We implement the learners and an appropriate teacher, and show that they are scalable, efficient and convergent in synthesizing adequate inductive invariants in a suite of more than 50 programs.
Issue Date:2015
Genre:Article
Type:Text
URI:http://hdl.handle.net/2142/77025
Date Available in IDEALS:2015-05-12


This item appears in the following Collection(s)

Item Statistics