Skip to main content
SpringerLink
Log in

A Verification Condition Visualizer

  • Conference paper
  • First Online:
Verified Software: Theories, Tools and Experiments (VSTTE 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8471))

Abstract

When first encountering data structures such as arrays, records and pointers programmers are often presented with pictorial representations. The use of pictures to describe data structures and their manipulation can help establish basic programming intuitions. The same is true of program proving where pictures are frequently used within the literature to describe program properties such as loop invariants. Here we report on an experimental prototype of a visualization tool that translates verification conditions arising from array based code into pictures. While initially aimed at supporting teaching, we have received positive feedback from users of program proving tools within industry.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Notes

  1. 1.

    The version based upon Ada 95.

  2. 2.

    This is a simplification of Dijkstra’s Dutch National Flag Problem which requires three colours.

  3. 3.

    FDL stands for Functional Description Language [1].

References

  1. Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)

    Google Scholar 

  2. Bergeretti, J.-F., Carré, B.A.: Information-flow and data-flow analysis of while-programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 37–61 (1985)

    Article  MATH  Google Scholar 

  3. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)

    MATH  Google Scholar 

  4. Gordon, M.J.: Programming Language Theory and its Implementation. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1988)

    Google Scholar 

  5. Le Goues, C., Leino, K.R.M., Moskal, M.: The boogie verification debugger (Tool Paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407–414. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Gries, D.: The Science of Programming. Springer, New York (1981)

    Book  MATH  Google Scholar 

  7. Hardy, V.J.: Java 2D API graphics. Sun Microsystems Press Java series. Sun Microsystems Press, Palo Alto (2000)

    Google Scholar 

  8. Hoare, C.A.R.: Proof of a program: find. CACM 14(1), 39–45 (1971)

    Article  MATH  Google Scholar 

  9. Hoare, C.A.R., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: a manifesto. ACM Comput. Surv. 41(4), 1–8 (2009)

    Google Scholar 

  10. Maclean, E., Ireland, A., Grov, G.; The core system: animation and functional correctness of pointer programs. In: Proceedings of the 16th IEEE Conference on Automated Software Engineering (ASE 2011): Tool Demonstration Paper, Lawrence, Kansas. IEEE (2011)

    Google Scholar 

  11. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)

    MATH  Google Scholar 

  13. Wirth, N.: Algorithms + Data Structures = Programs. Prentice-Hall, Engelwood Cliffs (1976)

    MATH  Google Scholar 

Download references

Acknowledgements

This research was supported by EPSRC Platform Grant EP/J001058. Our thanks go to Alan Bundy, Gudmund Grov, Paul Jackson, Jacques Fleuriot, Ewen Maclean for their feedback on the work, as well as to John Moore and Ben Gorry (BAE Systems, Warton UK) for their feedback on an early prototype of Auto-VCV. We also thank three anonymous VSTTE 2014 referees for their constructive feedback.

Author information

Authors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, EH14 4AS, UK

    Madiha Jami & Andrew Ireland

Authors
  1. Madiha Jami
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew Ireland
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrew Ireland .

Editor information

Editors and Affiliations

  1. NASA Ames Research Center, Mountain View, USA

    Dimitra Giannakopoulou

  2. University of Oxford, Oxford, United Kingdom

    Daniel Kroening

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Jami, M., Ireland, A. (2014). A Verification Condition Visualizer. In: Giannakopoulou, D., Kroening, D. (eds) Verified Software: Theories, Tools and Experiments. VSTTE 2014. Lecture Notes in Computer Science(), vol 8471. Springer, Cham. https://doi.org/10.1007/978-3-319-12154-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12154-3_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12153-6

  • Online ISBN: 978-3-319-12154-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation