Constrained Horn Clauses (CHC) is a fragment of First
Order Logic (FOL) that is sufficiently expressive to
describe many verification, inference, and synthesis
problems including inductive invariant inference, model
checking of safety properties, inference of procedure
summaries, regression verification, and sequential
equivalence. The CHC competition (CHC-COMP) will compare
state-of-the-art tools for CHC solving with respect to
performance and effectiveness on a set of publicly
available benchmarks. The winners among participating
solvers are recognized by measuring the number of
correctly solved benchmarks as well as the runtime. The
results of the second CHC-COMP will be announced in the HCVS workshop
affiliated with ETAPS 2019. |
PCSat, Yuki Satake
Sally, Martin Blicha
Eldarica, Philipp Rümmer
Hoice, Adrien Champion
Ultimate TreeAutomizer, Alexander Nutz
Ultimate Unihorn Automizer, Alexander Nutz
spacer, Arie Gurfinkel (Hors Concours)
Report (announced on Apr 7 2019)
Grigory Fedyukovich, Princeton University, USA
Arie Gurfinkel, University of Waterloo, Canada
Philipp Ruemmer, Uppsala University, Sweden
Adrien Champion, University of Tokyo, Japan
Last updated: 2024-05-16 19:57:10 +0000