Editing Formal verification (section)

== Automated program repair ==
{{main|Automatic bug fixing}}

Program repair is performed with respect to an [[Oracle (computability)|oracle]], encompassing the desired functionality of the program which is used for validation of the generated fix. A simple example is a test-suite—the input/output pairs specify the functionality of the program. A variety of techniques are employed, most notably using [[satisfiability modulo theories]] (SMT) solvers, and [[genetic programming]],<ref>{{cite journal |last1=Le Goues |first1=Claire |author1-link=Claire Le Goues|last2=Nguyen |first2=ThanhVu |last3=Forrest |first3=Stephanie |last4=Weimer |first4=Westley |title=GenProg: A Generic Method for Automatic Software Repair |journal=IEEE Transactions on Software Engineering |date=January 2012 |volume=38 |issue=1 |pages=54–72 |doi=10.1109/TSE.2011.104 |s2cid=4111307 |url = https://www.proquest.com/openview/f837f11066e9c9552df9e497064d6d80/1?pq-origsite=gscholar&cbl=21418&casa_token=X2fQSRNgLNwAAAAA:CBjvmrcBLZRqV7kjC-MY74s0wF68lhBvLF6rV4DWZkalzo2KdlUUzuMU38YgSmXGbwEL2NAr4w}}</ref> using evolutionary computing to generate and evaluate possible candidates for fixes. The former method is deterministic, while the latter is randomized.

Program repair combines techniques from formal verification and [[program synthesis]]. Fault-localization techniques in formal verification are used to compute program points which might be possible bug-locations, which can be targeted by the synthesis modules. Repair systems often focus on a small pre-defined class of bugs in order to reduce the search space. Industrial use is limited owing to the computational cost of existing techniques.