Learn Your Program

We introduce a synthesis framework for quantifierfree first-order LTL formulas over program variables. Such formulas are natural for specifying security requirements. Our framework uses automata learning to construct the program, as well as Hoare logic in order to reason about the program semantics and abstract the program states. Hoare logic also supply us with a proof of correctness for the program. We aim to learn not only the program, that is, the program states and transitions, but also to infer the program statements using abduction. Since this is an ongoing work, We discuss problems of termination, inference of Hoare predicates, and inference of new program statements. Our algorithm will allow automatically elimination of security vulnerabilities by constructing safe programs.