Learning Invariants using Decision Trees

Siddharth Krishna, Christian Puhrsch, Thomas Wies

The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: gi…