Verification as learning geometric concepts

57Citations
Citations of this article
34Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification explains why a program's set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states and by applying well known machine learning algorithms for classification, we are able to generate inductive assertions. By relaxing the search for an exact proof to classifiers, we obtain complexity theoretic improvements. Further, we extend the learning algorithm to obtain a sound procedure that can generate proofs containing invariants that are arbitrary boolean combinations of polynomial inequalities. We have evaluated our approach on a number of challenging benchmarks and the results are promising. © 2013 Springer-Verlag.

Cite

CITATION STYLE

APA

Sharma, R., Gupta, S., Hariharan, B., Aiken, A., & Nori, A. V. (2013). Verification as learning geometric concepts. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7935 LNCS, pp. 388–411). https://doi.org/10.1007/978-3-642-38856-9_21

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free