Skip to main content
SpringerLink
Log in
Book cover

Working Conference on Verified Software: Theories, Tools, and Experiments

VSTTE 2018: Verified Software. Theories, Tools, and Experiments pp 1–16Cite as

A Tree-Based Approach to Data Flow Proofs

  • Conference paper
  • First Online:

  • 575 Accesses

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

Abstract

In this paper, we investigate the theoretical foundation for the cost/precision trade-off of data flow graphs for verification. We show that one can use the theory of tree automata in order to characterize the loss of precision inherent in the abstraction of a program by a data flow graph. We also show that one can transfer a result of Oh et al. and characterize the power of the proof system of data flow proofs (through a restriction on the assertion language in Floyd-Hoare proofs).

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    Note the subtle difference between Floyd-style proofs [8] and Hoare-style proofs [10]: The former are annotations of the control flow graph while the latter are annotations of the program’s source code.

References

  1. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  2. Comon, H., et al.: Tree automata techniques and applications (2007)

    Google Scholar 

  3. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does astrée scale up? Formal Methods Syst. Des. 35(3), 229–264 (2009)

    Article  Google Scholar 

  4. Denaro, G., Pezzè, M., Vivanti, M.: On the right objectives of data flow testing. In: ICST, pp. 71–80. IEEE Computer Society (2014)

    Google Scholar 

  5. Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: POPL, pp. 297–308. ACM (2012)

    Google Scholar 

  6. Farzan, A., Kincaid, Z.: Duet: static analysis for unbounded parallelism. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 191–196. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_12

    Chapter  Google Scholar 

  7. Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL, pp. 129–142. ACM (2013)

    Google Scholar 

  8. Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19–32 (1967)

    Article  MathSciNet  Google Scholar 

  9. Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03237-0_7

    Chapter  Google Scholar 

  10. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  11. Martens, W., Neven, F., Schwentick, T.: Deterministic top-down tree automata: past, present, and future. In: Logic and Automata, volume 2 of Texts in Logic and Games, pp. 505–530. Amsterdam University Press (2008)

    Google Scholar 

  12. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6

    Book  MATH  Google Scholar 

  13. Oh, H., et al.: Global sparse analysis framework. ACM Trans. Program. Lang. Syst. (TOPLAS) 36, 8:1–8:44 (2014)

    Article  Google Scholar 

  14. Oh, H., Heo, K., Lee, W., Lee, W., Yi, K.: Design and implementation of sparse global analyses for C-like languages. In: PLDI, pp. 229–238. ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Freiburg, Freiburg im Breisgau, Germany

    Jochen Hoenicke, Alexander Nutz & Andreas Podelski

Authors
  1. Jochen Hoenicke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Nutz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andreas Podelski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Nutz .

Editor information

Editors and Affiliations

  1. Yale University, New Haven, CT, USA

    Ruzica Piskac

  2. Uppsala University, Uppsala, Sweden

    Philipp Rümmer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hoenicke, J., Nutz, A., Podelski, A. (2018). A Tree-Based Approach to Data Flow Proofs. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science(), vol 11294. Springer, Cham. https://doi.org/10.1007/978-3-030-03592-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03592-1_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03591-4

  • Online ISBN: 978-3-030-03592-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation