Gastvortrag: Daniel Neider: Horn-ICE Learning: An Inductive Approach to Deductive Software Verification
Dienstag, 15.06.2021, 17.00 Uhr
Ort: Online Session
Meeting-ID: 215 989 3416
Vortragender: Daniel Neider
Abstract:
Automated software verification has made impressive progress over the last two decades, mainly fueled by advanced in Satisfiability Modulo Theories (SMT) solvers. This has shifted the research focus to problems that have eluded automation so far. Among the most important (and arguably most difficult) ones is the synthesis of (loop) invariants and method contracts, which are a critical mechanism required to guide the overall verification process.
In this talk, I will present Horn-ICE, a learning-based framework for synthesizing invariants and contracts. In particular, I will describe how invariant synthesis can be phrased as a machine-learning task and present various learning algorithm for the Horn ICE setting. The result is a fully automated verification framework, capable of verifying programs in a host of challenging settings, including recursive programs, concurrent programs, and programs over dynamically allocated data structures. Throughout the talk, we will see Horn-ICE in action and discuss its various features through examples.