Guest lecture: Maximizing Branch Coverage with Constrained Horn Clauses

Thursday, June 15, 2023 1:00 pm - 1:00 pm EDT (GMT -04:00)

Guest Speaker: Grigory Fedyukovich, Assistant Professor, Florida State University, and Visiting Academic at Amazon

Date: Thursday, June 15, 2023

Time: 1:00pm

Location: E5 4047

Hosted by: Professor Arie Gurfinkel

Abstract: State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this talk, I will present a new application of CHCs to test-case generation, a problem of finding a set of tuples of input values to a program under which the program visits as many branches as possible. However, if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called HORNTINUUM exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art based on bounded model checking, concolic execution, and/or fuzzing.

Biography: Grigory Fedyukovich is an Assistant Professor at Florida State University and a Visiting Academic at Amazon. He completed his Ph.D. at the University of Lugano under the supervision of Prof Natasha Sharygina and then a postdoc at the University of Washington with Prof Rastislav Bodik and at Princeton University with Prof Aarti Gupta. His main research interests are in the fields of automated reasoning, software verification, and synthesis.