Formal method

This article or the following section is not adequately provided with supporting documents ( e.g. individual evidence ). Information without sufficient evidence could be removed soon. Please help Wikipedia by researching the information and including good evidence.

In computer science, the term formal method refers to a large number of natural and engineering techniques for modeling and mathematically rigorous testing of computer systems. The application of formal methods for the analysis of software and hardware is motivated by the expectation that, as in other engineering disciplines, an appropriate mathematical analysis can contribute to the reliability and stability of a system.

Formal methods build on a very broad basis of concepts from theoretical computer science , such as B. Logic , Formal Languages , Automata Theory , Formal Semantics and Type Systems .

relevance

Formal methods have seen an upswing in recent years. Static program analysis is used , for example, at Airbus and Microsoft . Microsoft itself maintains a number of research groups at Microsoft Research that deal with formal methods. B. Drivers are regularly checked using formal methods. Amazon also uses formal methods in the field of web services. Also, Google shows it interest. There is a conference that only deals with this topic.

There are also some researchers from the field of formal methods among the Turing Award winners , e.g. B. Tony Hoar for his contribution to the formal specification of programming languages, Robin Milner for his general theory of concurrency , Amir Pnueli for his contribution to temporal logic, and Edmund M. Clarke , E. Allen Emerson and Joseph Sifakis for their contribution to model checking.

See also

• Formal semantics
• Formal specification
• Formal verification
• Theorem Proof
• Model checking ( model checking )

Web links

• Peter Padawitz: Formal Methods of System Design . Dortmund 2010 ( uni-dortmund.de [PDF] lecture notes).
• Christel Baier , Joost-Pieter Katoen : Principles of model checking . MIT press, 2008.

Individual evidence

1. ↑ Jean Souyris: Industrial Experience of abstract interpretation-Based Static Analyzer . In: Building the Information Society (=  IFIP International Federation for Information Processing ). Springer US, Boston, MA 2004, ISBN 978-1-4020-8157-6 , pp. 393-400 , doi : 10.1007 / 978-1-4020-8157-6_31 ( springer.com [accessed April 20, 2020]).
2. ↑ SLAM. In: Microsoft Research. Retrieved April 20, 2020 (American English). 
3. ^ Byron Cook: Formal Reasoning About the Security of Amazon Web Services . In: Computer Aided Verification (=  Lecture Notes in Computer Science ). Springer International Publishing, Cham 2018, ISBN 978-3-319-96145-3 , p. 38–47 , doi : 10.1007 / 978-3-319-96145-3_3 ( springer.com [accessed April 20, 2020]).
4. ↑ Edward Aftandilian, Raluca Sauciuc, Siddharth Priya Krishnan Sundaresan: Building Useful Program Analysis Tools Using drop Extensible Java compiler. 2012, accessed April 20, 2020 . 
5. ^ Formal Methods in Industry. In: floc2018.org. Retrieved April 20, 2020 (American English).