Formal methods: Practice and experience

By Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John S. Fitzgerald. CSUR, 2009

775 citations recorded by the source corpus.

Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/593201530ad7146132313ad254b023dab71643af

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Yaodong Yang
2. Jun Wang
3. Shangding Gu
4. Yali Du
5. Alois C. Knoll
6. Guang Chen
7. Florian Walter
8. Longyu Yang

In Computational Theory and Mathematics

1. Shangding Gu
2. Yali Du
3. Alois C. Knoll
4. Guang Chen
5. Florian Walter
6. Jun Wang
7. Yaodong Yang

Citations in the corpus

• The State of Practice in Model-Driven Engineering (2014, background): “Although there have been a few prior surveys of modeling in industry, they have each focused on only one aspect of modeling, such as the use of UML [2] or the use of formal models [3].”
• A Review of Safe Reinforcement Learning: Methods, Theory and Applications (2022, methodology): “Based on formal methods [296], Safe MARL via shielding is proposed[80], in which they study safe MARL problem by one of formal methods, Linear Temporal Logic (LTL) [217] that is already adopted in safe single agent settings [8].”