Seminar on Monday, December 2

[Jan Kofron]

Dear all,

Let me invite you to another seminar in this semester that will take 
place exceptionally on *Monday, Dec 2 at 14:00 in S6* [1]. The seminar 
will be held by Grigory Fedyukovich from Florida State University.

Please find the details of the talk below.

[1] https://d3s.mff.cuni.cz/seminar/

Thanks, best regards!
Jan

====

Maximizing Branch Coverage with Constrained Horn Clauses

Abstract: State-of-the-art solvers for constrained Horn clauses (CHC) 
are successfully used to generate reachability facts for software using 
its symbolic encoding. 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. The key insight to achieve maximality is to 
identify and skip blocks of code that are provably unreachable. The new 
approach to test case generation called HORNTINUUM uses CHC to construct 
different program unrollings incrementally 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, making the 
unrolling process more efficient. In practice, this lets HORNTINUUM 
terminate early while guaranteeing maximal coverage. HORNTINUUM exhibits 
promising performance: it generates high coverage in most cases and 
takes less time on average than state-of-the-art based on bounded model 
checking, concolic execution, and/or fuzzing.

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


-- 
Jan Kofron, Ph.D.
Associate Professor
Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University
Malostranske namesti 25
118 00 Praha 1, Czech Republic
Phone: +420 95155 4285
http://d3s.mff.cuni.cz/~kofron
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x02C6705543C83F4D.asc
Type: application/pgp-keys
Size: 896 bytes
Desc: OpenPGP public key
URL: <http://d3s.mff.cuni.cz/pipermail/seminar/attachments/20241129/8ea696a6/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 236 bytes
Desc: OpenPGP digital signature
URL: <http://d3s.mff.cuni.cz/pipermail/seminar/attachments/20241129/8ea696a6/attachment.sig>