Editing Formal methods (section)

==Solvers and competitions==

Many problems in formal methods are [[NP-hardness|NP-hard]], but can be solved in cases arising in practice. For example, the Boolean satisfiability problem is [[NP-completeness|NP-complete]] by the [[Cook–Levin theorem]], but [[SAT solver]]s can solve a variety of large instances. There are "solvers" for a variety of problems that arise in formal methods, and there are many periodic competitions to evaluate the state-of-the-art in solving such problems.<ref>{{Cite book |last1=Bartocci |first1=Ezio |last2=Beyer |first2=Dirk |last3=Black |first3=Paul E. |last4=Fedyukovich |first4=Grigory |last5=Garavel |first5=Hubert |last6=Hartmanns |first6=Arnd |last7=Huisman |first7=Marieke |last8=Kordon |first8=Fabrice |last9=Nagele |first9=Julian |last10=Sighireanu |first10=Mihaela |last11=Steffen |first11=Bernhard |last12=Suda |first12=Martin |last13=Sutcliffe |first13=Geoff |last14=Weber |first14=Tjark |last15=Yamada |first15=Akihisa |date=2019 |editor-last=Beyer |editor-first=Dirk |editor2-last=Huisman |editor2-first=Marieke |editor3-last=Kordon |editor3-first=Fabrice |editor4-last=Steffen |editor4-first=Bernhard |chapter=TOOLympics 2019: An Overview of Competitions in Formal Methods |title=Tools and Algorithms for the Construction and Analysis of Systems |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=3–24 |doi=10.1007/978-3-030-17502-3_1 |isbn=978-3-030-17502-3|doi-access=free }}</ref>

* The SAT competition is a yearly competition that compares SAT solvers.<ref>{{Cite journal |last1=Froleyks |first1=Nils |last2=Heule |first2=Marijn |last3=Iser |first3=Markus |last4=Järvisalo |first4=Matti |last5=Suda |first5=Martin |date=2021-12-01 |title=SAT Competition 2020 |journal=Artificial Intelligence |volume=301 |pages=103572 |doi=10.1016/j.artint.2021.103572 |issn=0004-3702|doi-access=free }}</ref> SAT solvers are used in formal methods tools such as [[Alloy (specification language)|Alloy]].<ref>{{Cite book |last=Cornejo |first=César |chapter=SAT-based arithmetic support for alloy |date=2021-01-27 |title=Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering |chapter-url=https://doi.org/10.1145/3324884.3415285 |series=ASE '20 |location=New York, NY, USA |publisher=Association for Computing Machinery |pages=1161–1163 |doi=10.1145/3324884.3415285 |isbn=978-1-4503-6768-4}}</ref>
* [[CADE ATP System Competition|CASC]] is a yearly competition of [[automated theorem prover]]s.
* [[SMT-COMP]] is a yearly competition of [[SMT solver]]s, which are applied to [[formal verification]].<ref>{{Cite journal |last1=Barrett |first1=Clark |last2=Deters |first2=Morgan |last3=de Moura |first3=Leonardo |last4=Oliveras |first4=Albert |last5=Stump |first5=Aaron |date=2013-03-01 |title=6 Years of SMT-COMP |url=https://doi.org/10.1007/s10817-012-9246-5 |journal=Journal of Automated Reasoning |language=en |volume=50 |issue=3 |pages=243–277 |doi=10.1007/s10817-012-9246-5 |issn=1573-0670}}</ref>
* [[CHC-COMP]] is a yearly competition of solvers of [[constrained Horn clauses]], which have applications to formal verification.<ref>{{Cite journal |last1=Fedyukovich |first1=Grigory |last2=Rümmer |first2=Philipp |date=2021-09-13 |title=Competition Report: CHC-COMP-21 |journal=Electronic Proceedings in Theoretical Computer Science |volume=344 |pages=91–108 |doi=10.4204/EPTCS.344.7 |issn=2075-2180|doi-access=free |arxiv=2008.02939 }}</ref>
* [[QBFEVAL]] is a biennial competition of solvers for [[true quantified Boolean formula]]s, which have applications to [[model checking]].<ref>{{Cite book |last1=Shukla |first1=Ankit |last2=Biere |first2=Armin |last3=Pulina |first3=Luca |last4=Seidl |first4=Martina |chapter=A Survey on Applications of Quantified Boolean Formulas |date=November 2019 |title=2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI) |chapter-url=https://ieeexplore.ieee.org/document/8995437 |publisher=IEEE |pages=78–84 |doi=10.1109/ICTAI.2019.00020 |isbn=978-1-7281-3798-8}}</ref><ref>{{Cite journal |last1=Pulina |first1=Luca |last2=Seidl |first2=Martina |date=2019-09-01 |title=The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) |journal=Artificial Intelligence |volume=274 |pages=224–248 |doi=10.1016/j.artint.2019.04.002 |issn=0004-3702|doi-access=free }}</ref>
* [[SV-COMP]] is an annual competition for software verification tools.<ref>{{Cite book |last=Beyer |first=Dirk |date=2022 |editor-last=Fisman |editor-first=Dana |editor2-last=Rosu |editor2-first=Grigore |chapter=Progress on Software Verification: SV-COMP 2022 |title=Tools and Algorithms for the Construction and Analysis of Systems |series=Lecture Notes in Computer Science |volume=13244 |language=en |location=Cham |publisher=Springer International Publishing |pages=375–402 |doi=10.1007/978-3-030-99527-0_20 |isbn=978-3-030-99527-0|doi-access=free }}</ref>
* [[SyGuS-COMP]] is an annual competition for [[program synthesis]] tools.<ref>{{Cite journal |last1=Alur |first1=Rajeev |last2=Fisman |first2=Dana |last3=Singh |first3=Rishabh |last4=Solar-Lezama |first4=Armando |date=2017-11-28 |title=SyGuS-Comp 2017: Results and Analysis |journal=Electronic Proceedings in Theoretical Computer Science |volume=260 |pages=97–115 |doi=10.4204/EPTCS.260.9 |issn=2075-2180|doi-access=free |arxiv=1611.07627 }}</ref>