Editing Abductive reasoning (section)

===Computer programming===
In [[formal methods]], logic is used to specify and prove properties of computer programs. Abduction has been used in mechanized reasoning tools to increase the level of automation of the proof activity.

A technique known as bi-abduction, which mixes abduction and the [[frame problem]], was used to scale reasoning techniques for memory properties to millions of lines of code;<ref>{{Cite journal|first1=Cristiano|last1=Calcagno|first2=Dino|last2=Distefano|last3=O'Hearn|first3=Peter W.|first4=Hongseok|last4=Yang|date=2011-12-01|title=Compositional Shape Analysis by Means of Bi-Abduction|journal=[[Journal of the ACM]]|volume=58|issue=6|pages=1–66|language=EN|doi=10.1145/2049697.2049700|s2cid=52808268|url=https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466}}</ref> logic-based abduction was used to infer pre-conditions for individual functions in a program, relieving the human of the need to do so. It led to a program-proof startup company, which was acquired by Facebook,<ref>{{Cite web |date=July 18, 2013 |title=Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics |url=https://techcrunch.com/2013/07/18/facebook-monoidics/ |access-date=2023-09-30 |website=TechCrunch |language=en-US|archive-url=https://web.archive.org/web/20240930174905/https://techcrunch.com/2013/07/18/facebook-monoidics/|archive-date=30 September 2024|url-status=live}}</ref> and the Infer program analysis tool, which led to thousands of bugs being prevented in industrial codebases.<ref>{{Cite journal|last1=Distefano|first1=Dino|last2=Fähndrich|first2=Manuel|last3=Logozzo|first3=Francesco|last4=O'Hearn|first4=Peter W.|date=2019-07-24|title=Scaling static analyses at Facebook|journal=Communications of the ACM|volume=62|issue=8|pages=62–70|language=EN|doi=10.1145/3338112|doi-access=free}}</ref>

In addition to inference of function preconditions, abduction has been used to automate inference of invariants for program loops,<ref>{{Cite book|last1=Dillig|first1=Isil|last2=Dillig|first2=Thomas|last3=Li|first3=Boyang|last4=McMillan|first4=Ken|title=Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications |chapter=Inductive invariant generation via abductive inference |date=2013-10-29|chapter-url=https://dl.acm.org/doi/abs/10.1145/2544173.2509511|series=[[ACM SIGPLAN Notices]]|volume=48|issue=10|pages=443–456|language=EN|doi=10.1145/2509136.2509511|isbn=9781450323741|s2cid=16518775}}</ref> inference of specifications of unknown code,<ref>{{Cite journal|last=Giacobazzi|first=Roberto|date=1998-08-01|title=Abductive Analysis of Modular Logic Programs|url=https://academic.oup.com/logcom/article/8/4/457/1063792|journal=Journal of Logic and Computation|language=en|volume=8|issue=4|pages=457–483|doi=10.1093/logcom/8.4.457|issn=0955-792X}}</ref> and in synthesis of the programs themselves.<ref>{{Cite journal|last1=Polikarpova|first1=Nadia|last2=Sergey, Ilya|date=2019-01-02|title=Structuring the synthesis of heap-manipulating programs|journal=Proceedings of the ACM on Programming Languages|language=EN|volume=3|pages=1–30|doi=10.1145/3290385|doi-access=free|arxiv=1807.07022}}</ref>