Where Is the Value in a Program Verifier?

  • Colin O’Halloran
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


This paper addresses the assumption that software verification is valuable. Using experience from the assessment of safety critical software it makes observations of where the value of a Program Verifier might be and how it relates to the use of Formal Methods in requirements and design activities.


Formal Method Outer Loop Formal Verification Software Verification Program Verification 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Tudor, N., Adams, M., Clayton, P., O’Halloran, C.: Auto-coding/Auto-proving flight control software. In: Proceedings of IEEE 23rd Digital Avionics Systems Conference, Salt Lake City (2004)Google Scholar
  2. 2.
    Clark, G.D., Caseley, P.R., Powell, A.L., Murdoch, J.: Measurement of Safety Processes. In: Incose 2003, Washington, USA (2003)Google Scholar
  3. 3.
    Boulton, R.J., Gottliebsen, H., Hardy, R., Kelsy, T., Martin, U.: Design Verification for Control Engineering. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 21–35. Springer, Heidelberg (2004)Google Scholar
  4. 4.
    Boulton, R.J., Hardy, R., Martin, U.: A Hoare-Logic for Single-Input Single-Output Continuous-Time Control Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 113–125. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    RTCA Inc. and EUROCAE. DO-178B: Software Considerations in Airborne Systems and Equipment Certification (December 1992)Google Scholar
  6. 6.
    Galloway, A., Paige, R.F., Tudor, N.J., Weaver, R.A., Toyn, I., McDermid, J.: Proof Vs Testing in the context of safety standards. In: Proceedings of IEEE 24th Digital Avionics Systems Conference (2005)Google Scholar
  7. 7.
    Adams, M.M., Clayton, P.B.: CLawZ: Cost-Effective Formal Verification for Control Systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Fauquemberque, J.-L., Kahn, G., Kubbat, W., Levedag, S., Lions, J.-L., Lubeck, L., Mazzini, L., Merle, D., O’Halloran, C.: ARIANE 5 Flight 501 Failure, Report by the Inquiry Board, ESA (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Colin O’Halloran
    • 1
  1. 1.Systems Assurance GroupTrusted Information ManagementQinetiQUK

Personalised recommendations