Prochain Exposé
Thursday April 29th, 3PM Paris/France. (Weblink)
Grigory Fedyukovich (Florida State University, FL, USA)
Quantified Invariants via Syntax-Guided Synthesis.
To guarantee the absence of bugs in programs, state-of-the-art techniques synthesize checkable proofs such as inductive invariants, ranking functions, and recurrence sets. Synthesis of these proofs necessitates exploring a usually large search space and relies on off-the-shelf constraint solvers. In this talk, I will present new methods that bias the search space with extensive use of the program's source code. Intuitively, the source code often gives useful information, e.g., of occurrences of variables, constants, arithmetic, and comparison operators. Thus, we use the source code to automatically construct a formal grammar and iteratively sample the desired proofs from it.
For programs handling arrays, proofs are likely to contain universally quantified formulas, which are difficult to find, and difficult to prove inductive. I will present an algorithm that discovers quantified invariants in stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. Finally, by applying recent advances of constraint solving, the algorithm filters out wrong hypotheses. The combination of properties is often enough to prove that the program meets a safety specification. The algorithm has been implemented in a solver for Constrained Horn Clauses, called FreqHorn, and extended to deal with multiple (possibly nested) loops. We show that FreqHorn advances state-of-the-art on a wide range of public array-handling programs.
Exposés des semaines suivantes
Vos propositions sont les bienvenues !
