SHF: Small: Driving Learning for Program Verification

Princeton University, Princeton NJ

Investigators

Abstract

Program verification has broad applications, from ensuring safety of mission-critical software to improving program robustness and programmer productivity. Automatic program verification techniques employ various forms of learning to enhance scalability on large programs. These include deductive learning in modern logic-based solvers and learning from counterexamples in abstraction refinement procedures. Modular verification is essential for scaling verification to large software, and concurrent program verification is critical due to the wide prevalence of multi-core hardware. This project develops techniques for learning inductive invariants for modular verification in a teacher-learner setting. The research objectives include studying suitable languages of invariants at procedure boundaries, identifying requirements for progress in learning, and developing effective techniques for guiding the learner. The project also addresses verification of concurrent programs, where learning over different event sequences is performed by dynamic and predictive analysis over program traces. The goal is to drive the learning toward unexplored program behaviors by automatically generating test inputs. The research objectives include studying new trace abstractions and coverage metrics for concurrent programs, and developing techniques for coverage-guided test generation. The methods for driving learning include directed testing to target specific scenarios relevant for learning. Beyond these specific contributions, the results will provide insights on applying machine learning techniques in combination with static and dynamic analysis for advancing program verification. The project includes development of educational material, tools, and benchmarks that will be made publicly available.