Learning Invariants using Decision Trees and Implication Counterexamples

Garg, Pranav; Neider, Daniel; Madhusudan, P.; Roth, Dan

Permalink

https://hdl.handle.net/2142/77025 Copy

Description

Title

Learning Invariants using Decision Trees and Implication Counterexamples

Author(s)

• Garg, Pranav
• Neider, Daniel
• Madhusudan, P.
• Roth, Dan

Issue Date

2015

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/77025

Owning Collections