Skip to main content
SpringerLink
Log in

Formal Methods: Techniques, Applications, Thrust Areas and Future Prospects

  • Chapter
  • First Online:
Formal Methods for Safety and Security

  • 743 Accesses

Abstract

Formal methods are one of the oldest techniques of proving correctness of programs. Along with its contemporaries like Boolean Satisfiability and Theorem Proving it is also one of the areas which is still being actively researched. This in itself is a manifestation of the potential of the underlying techniques and the wide spectrum of applications it can positively impact. In this survey, we shall explore the most popular techniques, with an emphasis on industrial application of such techniques, and the various applications for which they are employed. We will then see some of the current and rapidly developing areas where formal methods could be invaluable, and we shall speculate some the future prospects of research and advancement in this field.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 129.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Berry G, Gonthier G (1992) The Esterel synchronous programming language: design, semantics, implementation. Sci Comput Programm 19(2):87–152

    Google Scholar 

  2. Caspi P, Pilaud D, Halbwachs N, Plaice JA (1987) LUSTRE: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL ’87, pp 178–188

    Google Scholar 

  3. Abrial J-R, Lee MKO, Neilson DS, Scharbach PN, Ib Holm Sørensen (1991) The B-method. In VDM ’91 formal software development methods, pp 398–405. Springer, Berlin

    Google Scholar 

  4. Baudin P, Filliâtre JC, Hubert T, Marche C, Monate B, Moy Y, Prevosto V (2012) ACSL: ANSI/ISO C specification language

    Google Scholar 

  5. Lamport L (2002) Specifying systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley Inc, Longman Publishing Co., Boston, MA

    Google Scholar 

  6. Filliatre J-C (2013) One logic to use them all. In: Proceedings of the 24th international conference on automated deduction, CADE ’13, pp 1–20

    Google Scholar 

  7. Jackson D (2002) Alloy: a new technology for software modelling. In: Tools and algorithms for the construction and analysis of systems, pp 20–20. Springer

    Google Scholar 

  8. Behm P, Benoit P, Faivre A, Meynadier J-M (1999) Météor: a successful application of B in a large project. In: Proceedings of the wold congress on formal methods in the development of computing systems—Volume I–Volume I, FM ’99, pp 369–387

    Google Scholar 

  9. Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M (2015) How amazon web services uses formal methods. Commun ACM 58(4):66–73

    Article  Google Scholar 

  10. Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5(7)

    Google Scholar 

  11. Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3)

    Google Scholar 

  12. Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 100(8):677–691

    Article  MATH  Google Scholar 

  13. Cavada R, Cimatti A, Franzén A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: Formal methods in computer-aided design, 7th international conference, FMCAD 2007, Austin, Texas, pp 69–76, 11–14 Nov 2007

    Google Scholar 

  14. Manna Z, Zarba CG (2002) Combining decision procedures. In: Formal methods at the crossroads. From Panacea to Foundational Support, 10th anniversary colloquium of UNU/IIST, the international institute for software technology of The United Nations University, Lisbon, Portugal, 18–20 March 2002, Revised Papers, pp 381–422

    Google Scholar 

  15. Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for construction and analysis of systems TACAS ’99, pp 193–207

    Google Scholar 

  16. Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Computer aided verification, 11th international conference, CAV ’99, Trento, Italy, pp 495–499, 6–10 July 1999

    Google Scholar 

  17. Holzmann GJ, Peled D (1996) The state of SPIN. In: Computer Aided Verification, pp 383–389. Springer

    Google Scholar 

  18. Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Tools and algorithms for the construction and analysis of systems, pp 168–176. Springer

    Google Scholar 

  19. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp 238–252

    Google Scholar 

  20. Graf S, Hassen Saidi S (1997) Construction of abstract state graphs with PVS. In: CAV, pp 72–83

    Google Scholar 

  21. Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T, Schmidt DA, Sudborough IH (eds) The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D. Jones, vol 2566. LNCS, pp 85–108. Springer-Verlag

    Google Scholar 

  22. Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. SIGPLAN Not 37(1):1–3

    Article  Google Scholar 

  23. Bessey Al, Block K, Chelf B, Chou A, Fulton B, Hallem S, Henri-Gros C, Kamsky A, McPeak S, Engler D (2010) A few billion lines of code later: using static analysis to find bugs in the real World. Commun ACM 53(2):66–75

    Article  Google Scholar 

  24. Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B, Frama-C: a software analysis perspective, vol 27, pp 573–609. Springer

    Google Scholar 

  25. Weiß B (2009) Predicate abstraction in a program logic calculus. In Leuschel M, Wehrheim H (eds) Proceedings, 7th international conference on integrated formal methods (iFM 2009), vol 5423 of LNCS, pp 136–150. Springer

    Google Scholar 

  26. Flanagan C, Qadeer S (2002) Predicate abstraction for software verification. In: POPL ’02: proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 191–202

    Google Scholar 

  27. Filliâtre J-C, Claude Marché (2007) The Why/Krakatoa/caduceus platform for deductive program verification. In: Computer aided verification, pp 173–177. Springer

    Google Scholar 

  28. Beyer D, Henzinger TA, Théoduloz G (2007) Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proceedings of the 19th international conference on computer aided verification, CAV ’07. Springer-Verlag, Berlin, pp 504–518

    Google Scholar 

  29. Koelbl A, Jacoby R, Jain H, Pixley C (2009) Solver technology for system-level to rtl equivalence checking. In: Design, automation & test in Europe conference and exhibition. DATE ’09., pp 196–201. IEEE

    Google Scholar 

  30. Harrison J (1995) Floating point verification in HOL. In: Higher order logic theorem proving and its applications, pp 186–199. Springer

    Google Scholar 

  31. Calcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, OHearn P, Papakonstantinou I, Purbrick J, Rodriguez D (2015) Moving fast with software verification. In: NASA formal methods. Springer, pp 3–11

    Google Scholar 

  32. O’Hearn PW (2012) A primer on separation logic (and automatic program verification and analysis)

    Google Scholar 

  33. How to Cut Verification Costs for IoT. http://semiengineering.com/how-to-cut-verification-costs-for-iot/. 2014

  34. Bertoli P, Cimatti A, Roveri M, Traverso P (2006) Strong planning under partial observability. Artif Intell 170(4):337–384

    Article  MATH  MathSciNet  Google Scholar 

  35. Cimatti A, Roveri M (1999) Conformant planning via model checking. In: Biundo S, Fox M (eds) Recent advances in AI planning, 5th european conference on planning, ECP ’99, Durham, Springer, pp 21–34, 8–10 Sept 1999

    Google Scholar 

  36. Bartocci E, Lío P (2016) Computational modeling, formal analysis, and tools for systems biology. PLoS Comput Biol 12(1)

    Google Scholar 

  37. Wang Q, Miskov-Zivanov N, Telmer C, Clarke EM (2015) Formal analysis provides parameters for guiding hyperoxidation in Bacteria using phototoxic proteins. In: Proceedings of the 25th edition on Great Lakes symposium on VLSI, GLSVLSI ’15, pp 315–320

    Google Scholar 

  38. Cimatti A, Franzen A, Griggio A, Kalyanasundaram K, Roveri M (2010) Tighter integration of BDDs and SMT for predicate abstraction. In: Proceedings of the conference on design, automation and test in Europe, DATE ’10, pp 1707–1712

    Google Scholar 

  39. Van Dijk T, Laarman A, Van De Pol J (2013) Multi-core BDD operations for symbolic reachability, electron. Notes Theor Comput Sci 296:127–143

    Article  Google Scholar 

  40. Conchon S, Goel A, Krstić S, Mebsout A, Zaïdi F (2012) Cubicle: a parallel SMT-based model checker for parameterized systems. In: Computer aided verification, pp 718–724. Springer

    Google Scholar 

  41. Filliatre J-C, Kalyanasundaram K (2011) Functory: a distributed computing library for objective Caml. In: Trends in functional programming, pp 65–81. Springer

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Nvidia Corporation, Santa Clara, CA, USA

    Krishnamani Kalyan

Authors
  1. Krishnamani Kalyan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Krishnamani Kalyan .

Editor information

Editors and Affiliations

  1. Aerospace Electronics and Systems Division, CSIR-National Aerospace Laboratories, Bangalore, Karnataka, India

    Manju Nanda

  2. Electronic CoE, Honeywell Technology Solutions, Bangalore, Karnataka, India

    Yogananda Jeppu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Kalyan, K. (2018). Formal Methods: Techniques, Applications, Thrust Areas and Future Prospects. In: Nanda, M., Jeppu, Y. (eds) Formal Methods for Safety and Security. Springer, Singapore. https://doi.org/10.1007/978-981-10-4121-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-981-10-4121-1_8

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-10-4120-4

  • Online ISBN: 978-981-10-4121-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation