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 will be announced in the HCVS workshop
affiliated with CAV,
ICLP
and IJCAR at FLoC 2018. |
Eldarica, Philipp Rümmer
Hoice, Adriene Champion
PECOS, John Gallagher
TransfHORNer, Fabio Fioravanti
Ultimate TreeAutomizer, Alexander Nutz
Ultimate Unihorn Automizer, Alexander Nutz
spacer, Arie Gurfinkel (Hors Concours)
Report (announced on Jul 13 2018)
Linear Real Arithmetic: lra_results.txt | StarExec Job log | summarize.py
Linear Integer Arithmetic: lia_results.txt | StarExec Job log | summarize.py
Arie Gurfinkel, University of Waterloo, Canada
Philipp Ruemmer, Uppsala University, Sweden
Grigory Fedyukovich, Princeton University, USA
Adrien Champion, University of Tokyo, Japan
Last updated: 2024-05-16 19:57:10 +0000