Software engineering and formal methods

ABSTRACT

The answer to software reliability concerns may lie in formal methods.

REFERENCES

• 1: Jonathan P. Bowen , Michael G. Hinchey, Seven More Myths of Formal Methods, IEEE Software, v.12 n.4, p.34-41, July 1995 [doi>10.1109/52.391826]
• 2: Michael G. Hinchey , J. P. Bowen , S. A. Schuman, High-Integrity System Specification and Design, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 3: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 4: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Proving thread termination, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 5: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 6: Patrick COUSOT , Radhia COUSOT , Jerome FERET , Antoine MINE , Laurent MAUBORGNE , David MONNIAUX , Xavier RIVAL, Varieties of Static Analyzers: A Comparison with ASTREE, Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, p.3-20, June 06-08, 2007 [doi>10.1109/TASE.2007.55]
• 7: Delmas, D. and Souyris, J. Astrée: From research to industry. Lecture Notes in Computer Science 4634, Springer (2007), 437--451.
• 8: Ferdinand, C., Heckmann, R., and Wilhelm, R. Analyzing the worst-case execution time by abstract interpretation of executable code. Lecture Notes in Computer Science 4147, Springer (2006), 1--14.
• 9: Alexey Gotsman , Josh Berdine , Byron Cook , Mooly Sagiv, Thread-modular shape analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 10: Gray, J. Dependability in the Internet era. In Proceedings of the High Dependability Computing Consortium Conference, Santa Cruz, CA, May 7, 2001.
• 11: Anthony Hall, Seven Myths of Formal Methods, IEEE Software, v.7 n.5, p.11-19, September 1990 [doi>10.1109/52.57887]
• 12: Laprie, J.-C., ed. Dependability: Basic concepts and terminology in English, French, German, Italian and Japanese. Dependable Computing and Fault-Tolerant Systems, Vol. 5, Springer-Verlag, NY, 1992.
• 13: David Patterson , Aaron Brown , Pete Broadwell , George Candea , Mike Chen , James Cutler , Patricia Enriquez , Armando Fox , Emre Kiciman , Matthew Merzbacher , David Oppenheimer , Naveen Sastry , William Tetzlaff , Jonathan Traupman , Noah Treuhaft, Recovery Oriented Computing (ROC): Motivation, Definition, Techniques,, University of California at Berkeley, Berkeley, CA, 2002
• 14: http://research.microsoft.com/SLAyer
• 15: http://research.microsoft.com/terminator
• 16: Bernhard Steffen , Tiziana Margaria, Method engineering for real-life concurrent systems, ACM Computing Surveys (CSUR), v.28 n.4es, Dec. 1996 [doi>10.1145/242224.242296]
• 17: Wolper, P. The meaning of "formal": From weak to strong formal methods. STTT1, 1--2 (1997), 6--8. Springer Verlag.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS