Skip to main content

On Formal Definition and Analysis of Formal Verification Processes

  • Chapter
  • 723 Accesses

Part of the Lecture Notes in Computer Science book series (LNTCS,volume 8373)


This paper suggests that there is considerable value in creating precise and formally-defined specifications of processes for carrying out formal verification, and in then subjecting those processes to rigorous analysis, and using the processes to guide the actual performance of formal verification. The paper suggests that some of the value could derive from widening the community of verifiers by having a process definition guide the performance of formal verification by newcomers or those who may be overawed by the complexities of formal verification. The paper also suggests that formally-defined process definitions can be of value both to novices and more experienced verifiers by serving as subjects of both dynamic and static analyses, with these analyses helping to build the confidence of various stakeholder groups (including the verifiers themselves) in the correct performance of the process and hence the correctness of the verification results. This paper is a status report on early work aimed at developing such processes, and demonstrating the feasibility and value of such analyses. The paper provides an example of a formally-defined verification process and suggests some kinds of dynamic and static analyses of the process. The process incorporates specification of both the nominal, ideal process as well as how the process must be iterated in response to such verification contingencies as incorrect assertions, incorrectly stated lemmas, and failed proofs of lemmas. In demonstrating how static analyses of this process can demonstrate that it assures certain kinds of desirable behaviors, the paper demonstrates an approach to providing effective verification guidance that assures sound verification results.


  • Formal Definition
  • Finite State Machine
  • Formal Verification
  • Verification Process
  • Proof Assistant

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.

This is a preview of subscription content, access via your institution.

Buying options

USD   29.95
Price excludes VAT (USA)
  • DOI: 10.1007/978-3-642-54624-2_2
  • Chapter length: 18 pages
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
USD   79.99
Price excludes VAT (USA)
  • ISBN: 978-3-642-54624-2
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
Softcover Book
USD   99.99
Price excludes VAT (USA)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  2. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  3. Dwyer, M.B., Clarke, L.A., Cobleigh, J.M., Naumovich, G.: Flow Analysis for Verifying Properties of Concurrent Software Systems. ACM Transactions on Software Engineering and Methodology 13(4), 359–430 (2004)

    CrossRef  Google Scholar 

  4. Floyd, R.W.: Assigning Meanings to Programs. In: Schwartz, J.T. (ed.) Proceedings of a Symposium on Applied Mathematics, vol. 19, pp. 19–31 (1967)

    Google Scholar 

  5. Futatsugi, K.: Verifying Specifications with Proof Scores in CafeOBJ. In: Intl. Conf. on Automated Software Engineering, Tokyo, Japan, pp. 3–10 (2006)

    Google Scholar 

  6. Futatsugi, K.: Fostering Proof Scores in CafeOBJ. In: Intl. Conference on Formal Engineering Methods, Shanghai, China, pp. 1–20 (2010)

    Google Scholar 

  7. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580 (1976)

    CrossRef  MATH  Google Scholar 

  8. King, J.C.: A Program Verifier., PhD Thesis, Carnegie Mellon University (1969)

    Google Scholar 

  9. Osterweil, L.J.: Software Processes are Software Too. In: ACM SIGSOFT/IEEE 9th International Conference on Software Engineering (ICSE 1987), Monterey, CA, pp. 2–13 (March 1987)

    Google Scholar 

  10. Osterweil, L.J.: Software Processes Are Software Too, Revisited. In: ACM SIGSOFT/IEEE 19th International Conference on Software Engineering (ICSE 1997), Boston, MA, pp. 540–548 (May 1997)

    Google Scholar 

  11. Osterweil, L.J., Clarke, L.A., Podorozhny, R., Wise, A., Boose, E., Ellison, A.M., Hadley, J.: Experience in Using a Process Language to Define Scientific Workflow and Generate Dataset Provenance. In: Proceedings of the ACM SIGSOFT 16th International Symposium on Foundations of Software Engineering, Atlanta, GA, pp. 319–329 (2008)

    Google Scholar 

  12. Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning 5(3), 363–397 (1989)

    MathSciNet  CrossRef  MATH  Google Scholar 

  13. Wise, A.: Little-JIL 1.5 Language Report. Department of Computer Science, University of Massachusetts, Amherst, UM-CS-2006-51 (2006)

    Google Scholar 

  14. Wise, A., Cass, A.G., Lerner, B.S., McCall, E.K., Osterweil, L.J., Sutton Jr., S.M.: Using Little-JIL to coordinate agents in software engineering. In: Proceedings of the Automated Software Engineering Conference (ASE 2000), Grenoble, France (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations


Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Osterweil, L.J. (2014). On Formal Definition and Analysis of Formal Verification Processes. In: Iida, S., Meseguer, J., Ogata, K. (eds) Specification, Algebra, and Software. Lecture Notes in Computer Science, vol 8373. Springer, Berlin, Heidelberg.

Download citation

  • DOI:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54623-5

  • Online ISBN: 978-3-642-54624-2

  • eBook Packages: Computer ScienceComputer Science (R0)