View source for Formal methods

{{Short description|Mathematical program specifications}}

In [[computer science]], '''formal methods''' are [[mathematics|mathematically]] rigorous techniques for the [[formal specification|specification]], development, [[Program analysis|analysis]], and [[formal verification|verification]] of [[software]] and [[computer hardware|hardware]] systems.<ref name="butler">{{cite web| first=R. W. | last=Butler | title=What is Formal Methods? | url=http://shemesh.larc.nasa.gov/fm/fm-what.html|date=2001-08-06|access-date=2006-11-16}}</ref> The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.<ref>{{cite journal| first=C. Michael | last=Holloway | title=Why Engineers Should Consider Formal Methods|url=http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|publisher=16th Digital Avionics Systems Conference (27–30 October 1997)|access-date=2006-11-16|url-status=dead|archive-url=https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|archive-date=16 November 2006}}</ref>

Formal methods employ a variety of [[theoretical computer science]] fundamentals, including [[logic in computer science|logic]] calculi, [[formal language]]s, [[automata theory]], [[control theory]], [[program semantics]], [[type systems]], and [[type theory]].<ref>Monin, pp.3-4</ref>

==Uses==

Formal methods can be applied at various points through the [[software development process|development process]].

===Specification===
{{Main|Formal specification}}
Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system. 

Alternatively, specification may be the only stage in which formal methods is used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.<ref>{{cite journal|last1=Utting|first1=Mark|last2=Reeves|first2=Steve|date=August 31, 2001|title=Teaching formal methods lite via testing|url=https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.223|journal=Software Testing, Verification and Reliability|volume=11|issue=3|pages=181–195 |doi=10.1002/stvr.223}}</ref>

The need for formal specification systems has been noted for years. In the [[ALGOL 58]] report,<ref>{{cite conference | first = J.W. | last = Backus | title = The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference | book-title = Proceedings of the International Conference on Information Processing | publisher = UNESCO | year = 1959 }}</ref> [[John Backus]] presented a formal notation for describing [[Syntax (programming languages)|programming language syntax]], later named [[Backus normal form]] then renamed [[Backus–Naur form]] (BNF).<ref>[[Donald Knuth|Knuth, Donald E.]] (1964), Backus Normal Form vs Backus Naur Form. ''[[Communications of the ACM]]'', 7(12):735–736.</ref> Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.<ref>{{cite book|last1=O'Hearn|first1=Peter W.|last2=Tennent|first2=Robert D.|title=Algol-like Languages|date=1997}}</ref>

===Synthesis===
{{Main|Program synthesis}}
Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.<ref>{{cite journal|last1=Gulwani|first1=Sumit|last2=Polozov|first2=Oleksandr|last3=Singh|first3=Rishabh|date=2017|title=Program Synthesis|url=https://www.nowpublishers.com/article/Details/PGL-010|journal=Foundations and Trends in Programming Languages|volume=4|issue=1–2|pages=1–119 |doi=10.1561/2500000010 }}</ref>

===Verification===
{{Main|Formal verification}}
Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system [[implementation]] satisfies its specification.

Once a formal specification has been developed, the specification may be used as the basis for [[mathematical proof|proving]] properties of the specification, and by inference, properties of the system implementation.

==== Sign-off verification ====
Sign-off verification is the use of a formal verification tool that is highly trusted.  Such a tool can replace traditional verification methods (the tool may even be certified).{{citation needed|date=June 2024}}

====Human-directed proof====
Sometimes, the motivation for proving the [[correctness (computer science)|correctness]] of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of [[mathematical proof]]: handwritten (or typeset) using [[natural language]], using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers.

Critics of such approaches point out that the [[ambiguity]] inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

====Automated proof====
In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:
* [[Automated theorem proving]], in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical [[axiom]]s, and a set of [[Rule of inference|inference rules]].
* [[Model checking]], in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.
* [[Abstract interpretation]], in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) [[lattice (order theory)|lattice]] representing it.

Some [[Automated theorem proving|automated theorem provers]] require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.

Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.

Critics note that some of those systems are like [[Oracle machine|oracle]]s: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "[[Quis custodiet ipsos custodes?|verifying the verifier]]"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.

The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators<ref>A. Cortesi and M. Zanioli, [http://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf Widening and Narrowing Operators for Abstract Interpretation]. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, {{ISSN|1477-8424}} (2011).</ref> to get fast convergence.

==Techniques==
{{Expand section|date=June 2024}}
Formal methods includes a number of different techniques.

===Specification languages===
{{Main|Specification language}}
The design of a computing system can be expressed using a specification language, which is a formal language that includes a proof system. Using this proof system, formal verification tools can reason about the specification and establish that a system adheres to the specification.<ref>{{cite book|last1=Bjørner|first1=Dines|last2=Henson|first2=Martin C.|date=2008|title=Logics of Specification Languages|pages=VII–XI}}</ref>

===Binary decision diagrams===
{{Main|Binary decision diagram}}
A binary decision diagram is a data structure that represents a [[Boolean function]].<ref>{{cite book|last=Bryant|first=Randal E.|chapter=Binary Decision Diagrams|title=Handbook of Model Checking|date=2018|editor1-last=Clarke|editor1-first=Edmund M.|editor2-last=Henzinger|editor2-first=Thomas A.|editor3-last=Veith|editor3-first=Helmut|editor4-last=Bloem|editor4-first=Roderick|page=191}}</ref> If a Boolean formula <math>\mathcal{P}</math> expresses that an execution of a program conforms to the specification, a binary decision diagram can be used to determine if <math>\mathcal{P}</math> is a tautology; that is, it always evaluates to TRUE. If this is the case, then the program always conforms to the specification.<ref>{{cite book|last1=Chaki|first1=Sagar|last2=Gurfinkel|first2=Arie|chapter=BDD-Based Symbolic Model Checking|title=Handbook of Model Checking|date=2018|editor1-last=Clarke|editor1-first=Edmund M.|editor2-last=Henzinger|editor2-first=Thomas A.|editor3-last=Veith|editor3-first=Helmut|editor4-last=Bloem|editor4-first=Roderick|page=191}}</ref>

===SAT solvers=== 
{{Main|SAT solver}}
A SAT solver is a program that can solve the [[Boolean satisfiability problem]], the problem of finding an assignment of variables that makes a given propositional formula evaluate to true. If a Boolean formula <math>\mathcal{P}</math> expresses that a specific execution of a program conforms to the specification, then determining that <math>\neg\mathcal{P}</math> is unsatisfiable is equivalent to determining that all executions conform to the specification. SAT solvers are often used in bounded model checking, but can also be used in unbounded model checking.<ref>{{cite journal|last1=Prasad|first1=Mukul R|last2=Biere|first2=Armin|last3=Gupta|first3=Aarti|title=A survey of recent advances in SAT-based formal verification|date=January 25, 2005|journal=International Journal on Software Tools for Technology Transfer|volume=7|issue=2 |pages=156–173 |doi=10.1007/s10009-004-0183-4}}</ref>

==Applications==
Formal methods are applied in different areas of hardware and software, including [[Router (computing)|router]]s, [[Ethernet switches]], [[routing protocol]]s, security applications, and [[operating system]] [[microkernel]]s such as [[seL4]]. There are several examples in which they have been used to verify the functionality of the hardware and software used in [[data centre]]s. [[IBM]] used [[ACL2]], a theorem prover, in the [[AMD]] x86 processor development process.{{citation needed|date=September 2015}} Intel uses such methods to verify its hardware and [[firmware]] (permanent software programmed into a [[read-only memory]]){{citation needed|date=September 2015}}. [[Dansk Datamatik Center]] used formal methods in the 1980s to develop a compiler system for the [[Ada programming language]] that went on to become a long-lived commercial product.<ref>{{cite book | first1=Dines | last1=Bjørner | first2=Christian | last2=Gram | first3=Ole N. | last3=Oest | first4=Leif | last4=Rystrøm | chapter=Dansk Datamatik Center | editor-first= John | editor-last=Impagliazzo | editor2-first=Per | editor2-last=Lundin | editor3-first=Benkt | editor3-last=Wangler | title=History of Nordic Computing 3: IFIP Advances in Information and Communication Technology | publisher=Springer | year= 2011 | pages= 350–359 }}</ref><ref>{{cite conference | contribution=40 Years of Formal Methods: Some Obstacles and Some Possibilities? | first1=Dines | last1=Bjørner | first2=Klaus | last2=Havelund | title=FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings | publisher=Springer | pages=42–61 |url=http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf}}</ref>

There are several other projects of [[NASA]] in which formal methods are applied, such as [[Next Generation Air Transportation System]]{{citation needed|date=September 2015}}, Unmanned Aircraft System integration in National Airspace System,<ref>Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</ref> and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).<ref>Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ {{Webarchive|url=https://web.archive.org/web/20160305005830/http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ |date=2016-03-05 }}</ref>
[[B-Method]] with [[Atelier B]],<ref>{{cite web| url=http://www.atelierb.eu/en/ | title=Atelier B | website=www.atelierb.eu }}</ref> is used to develop safety automatisms for the various subways installed throughout the world by [[Alstom]] and [[Siemens]], and also for [[Common Criteria]] certification and the development of system models by [[ATMEL]] and [[STMicroelectronics]].

Formal verification has been frequently used in hardware by most of the well-known hardware vendors, such as IBM, [[Intel]], and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache-coherent protocol,<ref>C. T. Chou, P. K. Mannava, S. Park, "[https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf A simple method for parameterized verification of cache coherence protocols]", Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</ref> Intel Core i7 processor execution engine validation <ref>Formal Verification in Intel Core i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 {{Webarchive|url=https://web.archive.org/web/20150503222301/http://cps-vo.org/node/1371 |date=2015-05-03 }}, accessed at September 13, 2013.</ref> (using theorem proving, [[binary decision diagram|BDDs]], and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,<ref>J. Grundy, "Verified optimizations for the Intel IA-64 architecture", In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</ref> and verification of high-performance dual-port [[gigabit Ethernet]] [[Network interface controller|controller]] with support for [[PCI Express|PCI express]] protocol and Intel advance management technology using Cadence.<ref>E. Seligman, I. Yarom, "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf Best known methods for using Cadence Conformal LEC]", at Intel.</ref> Similarly, IBM has used formal methods in the verification of power gates,<ref>C. Eisner, A. Nahir, K. Yorav, "[ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449 Functional verification of power gated designs by compositional reasoning]{{dead link|date=May 2025|bot=medic}}{{cbignore|bot=medic}}", Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</ref> registers,<ref>P. C. Attie, H. Chockler, "[https://core.ac.uk/download/pdf/82434920.pdf Automatic verification of fault-tolerant register emulations]", Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</ref> and functional verification of the IBM Power7 microprocessor.<ref>K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "[https://ieeexplore.ieee.org/abstract/document/5756329/ Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems]", IBM Journal of Research and Development, vol. 55, no 3.</ref>

==In software development==
In [[software development]], formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety-critical or security-critical software and systems, such as [[avionics software]]. Software safety assurance standards, such as [[DO-178C]] allows the usage of formal methods through supplementation, and [[Common Criteria]] mandates formal methods at the highest levels of categorization.

For sequential software, examples of formal methods include the [[B-Method]], the specification languages used in [[automated theorem proving]], [[Rigorous Approach to Industrial Software Engineering|RAISE]], and the [[Z notation]].

In [[functional programming]], [[QuickCheck|property-based testing]] has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions.

The [[Object Constraint Language]] (and specializations such as [[Java Modeling Language]]) has allowed object-oriented systems to be formally specified, if not necessarily formally verified.

For concurrent software and systems, [[Petri net]]s, [[process algebra]], and [[finite-state machine]]s (which are based on [[automata theory]]; see also [[virtual finite state machine]] or [[event driven finite state machine]]) allow executable software specification and can be used to build up and validate application behaviour.

Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of [[first-order logic]]—and then to directly execute the logic as though it were a program. The [[Web Ontology Language|OWL]] language, based on [[description logic]], is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are [[Attempto Controlled English]], and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.{{citation needed|date=June 2016}}

==Semi-formal methods==
Semi-formal methods are formalisms and languages that are not considered fully "formal". It defers the task of completing the semantics to a later stage, which is then done either by human interpretation or by interpretation through software like code or test case [[Generator (computer programming)|generators]].<ref>{{Cite book|title=X2R-2, deliverable D5.1}}</ref>

Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.<ref>[[Daniel Jackson (computer scientist)|Daniel Jackson]] and [[Jeannette Wing]], [http://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html "Lightweight Formal Methods"], ''IEEE Computer'', April 1996</ref><ref>Vinu George and Rayford Vaughn, [http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html "Application of Lightweight Formal Methods in Requirement Engineering"] {{webarchive|url=https://web.archive.org/web/20060301022259/http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html |date=2006-03-01 }}, ''Crosstalk: The Journal of Defense Software Engineering'', January 2003</ref> They contend that the [[Expressive power (computer science)|expressiveness]] of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various ''lightweight'' formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the [[Alloy language|Alloy]] object modelling notation,<ref>Daniel Jackson, [http://people.csail.mit.edu/dnj/publications/alloy-journal.pdf "Alloy: A Lightweight Object Modelling Notation"], ''ACM Transactions on Software Engineering and Methodology (TOSEM)'', Volume 11, Issue 2 (April 2002), pp. 256-290</ref> Denney's synthesis of some aspects of the [[Z notation]] with [[use case]] driven development,<ref>Richard Denney, ''Succeeding with Use Cases: Working Smart to Deliver Quality'', Addison-Wesley Professional Publishing, 2005, {{ISBN|0-321-31643-6}}.</ref> and the CSK [[Vienna Development Method|VDM]] Tools.<ref>Sten Agerholm and Peter G. Larsen, [http://home0.inet.tele.dk/pgl/fmtrends98.pdf "A Lightweight Approach to Formal Methods"] {{webarchive|url=https://web.archive.org/web/20060309041943/http://home0.inet.tele.dk/pgl/fmtrends98.pdf |date=2006-03-09 }}, In ''Proceedings of the International Workshop on Current Trends in Applied Formal Methods'', Boppard, Germany, Springer-Verlag, October 1998</ref>

==Formal methods and notations==
There are a variety of formal methods and notations available.

===Specification languages===
* [[Abstract State Machines]] (ASMs)
* [[ACL2|A Computational Logic for Applicative Common Lisp]] (ACL2)
* [[Actor model]]
* [[Alloy language|Alloy]]
* [[ANSI/ISO C Specification Language]] (ACSL)
* [[Autonomic System Specification Language]] (ASSL)
* [[B-Method]]
* [[CADP]]
* [[Common Algebraic Specification Language]] (CASL)
* [[Esterel]]
* [[Java Modeling Language]] (JML)
* [[Knowledge Based Software Assistant]] (KBSA)
* [[Lustre programming language|Lustre]]
* [[mCRL2]]
* [[Perfect Developer]]
* [[Petri nets]]
* [[Predicative programming]]
* [[Process calculi]]
** [[Communicating Sequential Processes|CSP]]
** [[Language Of Temporal Ordering Specification|LOTOS]]
** [[Pi-calculus|π-calculus]]
* [[RAISE specification language|RAISE]]
* [[Rebeca Modeling Language]]
* [[SPARK (programming language)|SPARK Ada]]
* [[Specification and Description Language]]
* [[TLA+]]
* [[Universal Systems Language|USL]]
* [[Vienna Development Method|VDM]]
** [[VDM specification language|VDM-SL]]
** VDM++
* [[Z notation]]

===Model checkers===
{{main|List of model checking tools}}
* ESBMC<ref>{{cite web| url=http://esbmc.org/ | title=ESBMC | website=esbmc.org }}</ref>
* [[MALPAS Software Static Analysis Toolset]] – an industrial-strength model checker used for formal proof of safety-critical systems
* [[PAT (model checker)|PAT]] – a free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g., shared variables, arrays, fairness)
* [[SPIN model checker|SPIN]]
* [[Uppaal Model Checker|UPPAAL]]

==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>

==Organizations==
{{main|:Category:Formal methods organizations}}
* [[BCS-FACS]]
* [[Formal Methods Europe]]
* [[Z User Group]]

==See also==
* [[Abstract interpretation]]
* [[Automated theorem proving]]
* [[Design by contract]]
* [[:Category:Formal methods people|Formal methods people]]
* [[Formal science]]
* [[Formal specification]]
* [[Formal verification]]
* [[Formal system]]
* [[Methodism]]
* [[Methodology]]
* [[Model checking]]
* [[Scientific method]]
* [[Software engineering]]
* [[Specification language]]

==References==
{{reflist}}

==Further reading==
{{refbegin}}
* [[Jonathan P. Bowen]] and Michael G. Hinchey, ''Formal Methods''. In Allen B. Tucker, Jr. (ed.), ''Computer Science Handbook'', 2nd edition, Section XI, ''Software Engineering'', Chapter 106, pages 106-1&nbsp;– 106-25, [[Chapman & Hall]] / [[CRC Press]], [[Association for Computing Machinery]], 2004.
* Hubert Garavel (editor) and Susanne Graf. [https://www.bsi.bund.de/SharedDocs/DE/Publikationen/Studien/formal_methods_study_875/study_875.html ''Formal Methods for Safe and Secure Computer Systems'']{{Dead link|date=November 2022 |bot=InternetArchiveBot |fix-attempted=yes }}. [[Federal Office for Information Security|Bundesamt für Sicherheit in der Informationstechnik]], BSI study 875, Bonn, Germany, December 2013.
* {{cite book| title=Formal Methods for Industrial Critical Systems: 25 International Conference, FMICS 2020 | pages=3–69 | chapter=The 2020 Expert Survey on Formal Methods | first1=Hubert | last1=Garavel | first2=Maurice H. | last2=ter Beek | first3=Jaco | last3=van de Pol | date=29 August 2020 | series=[[Lecture Notes in Computer Science]] (LNCS) | publisher=[[Springer Science+Business Media|Springer]] | volume=12327 | doi=10.1007/978-3-030-58298-2_1 | isbn=978-3-030-58297-5 | s2cid=221381022 | url=https://hal.inria.fr/hal-03082818/file/Garavel-terBeek-vandePol-20.pdf }}* Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, ''Formal Methods''. In Philip A. Laplante (ed.), ''Encyclopedia of Software Engineering'', [[Taylor & Francis]], 2010, pages 308–320.
* [[Marieke Huisman]], Dilian Gurov, and Alexander Malkis, [http://arxiv.org/abs/2002.07279 ''Formal Methods: From Academia to Industrial Practice – A Travel Guide''], arXiv:2002.07279, 2020.
* {{cite journal| date=9 September 2020 | title=Formal methods in dependable systems engineering: a survey of professionals from Europe and North America | first1=Mario | last1=Gleirscher | first2=Diego | last2=Marmsoler | journal=Empirical Software Engineering | volume=25 | issue=6 | pages=4473–4546 | doi=10.1007/s10664-020-09836-5 | publisher=[[Springer Nature]] | doi-access=free | arxiv=1812.08815 }}
* Jean François Monin and [[Michael G. Hinchey]], ''Understanding formal methods'', [[Springer-Verlag|Springer]], 2003, {{ISBN|1-85233-247-6}}.
{{refend}}

==External links==
* [http://www.fmeurope.org/ Formal Methods Europe] (FME)
* [https://formalmethods.wikia.org/ Formal Methods Wiki]
* [http://foldoc.org/formal+methods Formal methods] from [https://foldoc.org/ Foldoc]
;Archival material
* [https://web.archive.org/web/20130404202524/http://academic.research.microsoft.com/Keyword/14916 Formal method] keyword on [[Microsoft Academic Search]] via [[Archive.org]]
* [https://web.archive.org/web/20170713233230/http://www.fm4industry.org/index.php/Evidence_on_Formal_Methods_uses_and_impact_on_Industry Evidence on Formal Methods uses and impact on Industry] supported by the [http://www.deploy-project.eu DEPLOY] {{Webarchive|url=https://web.archive.org/web/20120608063125/http://www.deploy-project.eu/ |date=2012-06-08 }} project (EU FP7) in [[Archive.org]]

{{Computer science}}
{{Software engineering}}

{{DEFAULTSORT:Formal Methods}}
[[Category:Formal methods| ]]
[[Category:Software development philosophies]]
[[Category:Theoretical computer science]]
[[Category:Specification languages]]