Skip to main content
SpringerLink
Log in

Developer-Oriented Correctness Proofs

A Case Study of Cheney’s Algorithm

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2011)

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

Included in the following conference series:

  • 869 Accesses

Abstract

This paper examines the problem of structuring proofs in functional software verification from a novel perspective. By aligning the proofs with the operational behaviour of the program, we allow the formalization of the underlying concepts and their properties to reflect informal correctness arguments. By splitting the proof along the different aspects of the code, we achieve re-use of both theories and proof strategies across algorithms, thus enabling reasoning by analogy as employed in software construction. We demonstrate the viability and usefulness of the approach using a low-level C implementation of Cheney’s algorithm.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Banerjee, A., Barnett, M., Naumann, D.A.: Boogie meets regions: A verification experience report. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 177–191. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. SIGPLAN Not. 44(1), 441–453 (2009)

    Article  MATH  Google Scholar 

  3. Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. SIGPLAN Not. 43(6), 349–361 (2008)

    Article  Google Scholar 

  4. Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) SMT 2009: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories. ACM, New York (2009)

    Google Scholar 

  5. Böhme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie–An interactive prover-backend for the Verifying C Compiler. J. Autom. Reason. 44, 111–144 (2010)

    Article  MATH  Google Scholar 

  6. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1-2), 200–227 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Myreen, M.O.: Reusable verification of a copying collector. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 142–156. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Marti, N., Affeldt, R.: Formal verification of the heap manager of an operating system using separation logic. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400–419. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. McCreight, A.: The Mechanized Verification of Garbage Collector Implementations. PhD thesis, Department of Computer Science, Yale University (2008)

    Google Scholar 

  10. Hubert, T., Marché, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: Aichernig, B.K., Beckert, B. (eds.) SEFM. IEEE, Los Alamitos (2005)

    Google Scholar 

  11. Cheney, C.J.: A nonrecursive list compacting algorithm. Commun. ACM 13, 677–678 (1970)

    Article  MATH  Google Scholar 

  12. Gast, H.: Reasoning about memory layouts. Formal Methods in System Design 37(2-3), 141–170 (2010)

    Article  MATH  Google Scholar 

  13. Gast, H., Trieflinger, J.: High-level Reasoning about Low-level Programs. In: Roggenbach, M. (ed.) Automated Verification of Critical Systems 2009. Electronic Communications of the EASST, vol. 23 (2009)

    Google Scholar 

  14. Gast, H.: Verifying the L4 kernel allocator in lightweight separation (2010), http://www-pu.informatik.uni-tuebingen.de/users/gast/proofs/kalloc.pdf

  15. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Gast, H.: Lightweight separation. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 199–214. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Gast, H.: A developer-oriented proof of Cheney’s algorithm (2011), http://www-pu.informatik.uni-tuebingen.de/users/gast/proofs/cheney.pdf

  18. Torp-Smith, N., Birkedal, L., Reynolds, J.C.: Local reasoning about a copying garbage collector. ACM Trans. Program. Lang. Syst. 30(4), 1–58 (2008)

    Article  MATH  Google Scholar 

  19. Dawson, J.E.: Isabelle theories for machine words. In: 7th International Workshop on Automated Verification of Critical Systems (AVOCS 2007). ENTCS, vol. 250 (2009)

    Google Scholar 

  20. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales - A sectioning concept for isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–166. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Burstall, R.: Some techniques for proving correctness of programs which alter data stuctures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7. Edinburgh University Press, Edinburgh (1972)

    Google Scholar 

  22. McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. SIGPLAN Not. 42(6), 468–479 (2007)

    Article  Google Scholar 

  23. Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle/HOLCF. Electron. Notes Theor. Comput. Sci. 218, 371–389 (2008)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Wilhelm-Schickard-Institut für Informatik, University of Tübingen, Germany

    Holger Gast

Authors
  1. Holger Gast
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Teesside University, UK

    Shengchao Qin

  2. LMAM and Department of Informatics, School of Mathematical Sciences,, Peking University, China

    Zongyan Qiu

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gast, H. (2011). Developer-Oriented Correctness Proofs. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24559-6_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24558-9

  • Online ISBN: 978-3-642-24559-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation