Abstract.
With the steady increase in computational power of general purpose computers, our ability to analyze routine software artifacts is also steadily increasing. As a result, we are witnessing a shift in emphasis from the verification of abstract hand-built models of code, towards the direct verification of implementation level code. This change in emphasis poses a new set of challenges in software verification. We explore some of them in this paper.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: Proc. PLDI 2001, f2SIGPLAN Notices, vol. 36(5), pp. 203–213 (2001)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder - A 2nd generation of a Java model checker. In: Proc. Workshop on Advances in Verification, Chicago, Ill. (July 2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (January 2000)
Corbett, J.C., Dwyer, M.B., et al.: Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd Int. Conf. on Software Engineering, June 2000, pp. 439–448 (2000)
Havelund, K., Pressburger, T.: Model Checking Java Programs Using Java PathFinder. Int. Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Henzinger, T.A., Jhala, R., et al.: Software Verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. on Software Engineering 28(4), 364–377 (2002)
Holzmann, G.J., Smith, M.H.: FeaVer 1.0 User Guide, Bell Labs, 64 pgs (December 2002), Online document http://cm.bell-labs.com/cm/cs/what/modex/
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (August 2003) ISBN 0-32122-862-6
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice Hall, Englewood Cliffs (1967)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science 1977, Providence, R.I., pp. 46–57 (1977)
Strachey, C.: An impossible program. Computer Journal 7(4), 313 (1965)
Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. In: Proc. London Mathematical Soc. Ser., vol. 2(42), pp. 230–265 (1936)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holzmann, G.J. (2003). Trends in Software Verification. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive