Abstract
We propose a general end-to-end deep learning framework Code2Inv, which takes a verification task and a proof checker as input, and automatically learns a valid proof for the verification task by interacting with the given checker. Code2Inv is parameterized with an embedding module and a grammar: the former encodes the verification task into numeric vectors while the latter describes the format of solutions Code2Inv should produce. We demonstrate the flexibility of Code2Inv by means of two small-scale yet expressive instances: a loop invariant synthesizer for C programs, and a Constrained Horn Clause (CHC) solver.
Cite
CITATION STYLE
Si, X., Naik, A., Dai, H., Naik, M., & Song, L. (2020). Code2Inv: A Deep Learning Framework for Program Verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12225 LNCS, pp. 151–164). Springer. https://doi.org/10.1007/978-3-030-53291-8_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
