CoCo 2023 Results
Combined Yes and No Results
Yes Results
No Results
Detailed results are
available. The same holds for the
LiveView
of CoCo 2023 upon completion.
Certification Results
In the CERTIFICATION category, certifiers are ranked based on the number
of certificates that are validated.
In the RELIABILITY category, tools are ranked based on the number
of generated certified proofs.
Problem Selection
The problems were selected using the following
COPS queries. Here s is the
number 068 composed of the three random digits 0 (Frédéric Blanqui),
6 (Mirai Ikebuchi), 8 (Nick Smallbone), provided by the panel members.
| categories |
queries |
| COM |
limit:100,s 1..1655 commutation !duplicate
|
| CSR |
limit:100,s 1..1655 {cstrs or cstrs} !duplicate {!confluent !non_confluent}
|
|
CTRS |
limit:100,s 1..1655 3_ctrs oriented !duplicate {!confluent !non_confluent}
limit:68,s 1..1655 3_ctrs oriented !duplicate !{!confluent !non_confluent}
|
| GCR |
limit:100,s 1..1655 !srs {trs OR mstrs} !duplicate
|
| INF |
limit:100,s 1..1655 infeasibility !duplicate {!yes !no}
limit:67,s 1..1655 infeasibility !duplicate !{!yes !no}
|
| NFP |
limit:100,s 1..1655 trs !srs !confluent !duplicate {!nfp !non_nfp}
limit:74,s 1..1655 trs !srs !confluent !duplicate !{!nfp !non_nfp}
|
| SRS |
limit:100,s 1..1655 srs !duplicate {!confluent !non_confluent}
limit:76,s 1..1155 srs !duplicate !{!confluent !non_confluent}
|
| TRS |
limit:100,s 1..1655 trs !srs !duplicate {!confluent !non_confluent}
limit:75,s 1..1155 trs !srs !duplicate !{!confluent !non_confluent}
|
| UNC |
limit:100,s 1..1655 trs !srs !nfp !duplicate {!unc !non_unc}
limit:92,s 1..1155 trs !srs !nfp !duplicate !{!unc !non_unc}
|
| UNR |
limit:100,s 1..1655 trs !srs !unc !duplicate {!unr !non_unr}
limit:84,s 1..1655 trs !srs !unc !duplicate !{!unr !non_unr}
|