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 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
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
Comon, H., et al.: Tree automata techniques and applications (2007)
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)
Denaro, G., Pezzè, M., Vivanti, M.: On the right objectives of data flow testing. In: ICST, pp. 71–80. IEEE Computer Society (2014)
Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: POPL, pp. 297–308. ACM (2012)
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
Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL, pp. 129–142. ACM (2013)
Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19–32 (1967)
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
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
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)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6
Oh, H., et al.: Global sparse analysis framework. ACM Trans. Program. Lang. Syst. (TOPLAS) 36, 8:1–8:44 (2014)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
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)