Code2Inv: A Deep Learning Framework for Program Verification
Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, Le Song
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.
Topics & Concepts
Computer scienceProgramming languageParameterized complexitySatisfiability modulo theoriesEmbeddingTask (project management)Model checkingSolverHorn clauseFormal verificationGrammarInvariant (physics)Theoretical computer scienceArtificial intelligenceAlgorithmEconomicsPrologLinguisticsPhilosophyMathematical physicsManagementPhysicsAdversarial Robustness in Machine LearningSoftware Testing and Debugging TechniquesSoftware Engineering Research