핵심 개념
CHC-COMP 2023は、制約付きホーンクローズ解決器の競争の6回目の開催です。この競争では、7つのソルバー(6つの競争参加ソルバーと1つのhors concours)と6つのトラックが特徴でした。
초록
CHC-COMP 2023は、制約付きホーンクローズ(CHC)解決器の競争の6回目の開催です。この競争は2023年4月に行われ、その結果は4月23日にパリで開催された第10回ホーンクローズ検証・合成ワークショップ(HCVS 2023)で発表されました。
この版では、7つのソルバー(6つの競争参加ソルバーと1つのhors concours)と6つのトラックが特徴でした。各トラックは、線形整数算術、配列、非再帰/再帰的代数的データ型、およびそれらの組み合わせに関する制約付きホーンクローズのクラスを扱っています。
報告書では、CHC-COMP 2023の組織、ベンチマークの選択、参加ソルバーの説明、競争の結果を説明しています。また、今後の課題と新しい提案についても議論しています。
통계
線形整数算術のみのベンチマーク(LIA-lin)で、Golemが1位、Eldaricaが2位、Thetaが3位
線形整数算術の非線形ベンチマーク(LIA-nonlin)で、Eldaricaが1位、Golemが2位、Ultimate Unihornが3位
線形整数算術と配列のベンチマーク(LIA-lin-Arrays、LIA-nonlin-Arrays)で、Eldaricaが1位
線形整数算術、配列、非再帰的代数的データ型のベンチマーク(LIA-nonlin-Arrays-nonrecADT)で、Eldaricaが1位
代数的データ型と線形整数算術の非線形ベンチマーク(ADT-LIA-nonlin)で、Eldaricaが1位