Editing Formal methods (section)

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