Skip to main content
SpringerLink
Log in

Sparse Analysis of Variable Path Predicates Based upon SSA-Form

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9952))

Included in the following conference series:

Abstract

Static Single Assignment Form benefits data flow analysis by its static guarantees on the definitions and uses of variables. In this paper, we show how to exploit these guarantees to enable a sparse data flow analysis of variable predicates, for gaining a rich predicate-based and path-oriented characterization of the values of program variables.

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

    For the complete proofs, we refer the reader to [10].

  2. 2.

    http://service-technology.org/fiona/.

References

  1. Bodík, R., Gupta, R., Soffa, M.L.: Refining data flow information using infeasible paths. In: ESEC-FSE 1997, Proceeding, pp. 361–377. ACM (1997)

    Google Scholar 

  2. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, M.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Google Scholar 

  3. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N.: Efficiently computing static single assignment form and the control dependence graph. ACM TOPLAS 13(4), 451–490 (1991)

    Article  Google Scholar 

  4. Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: PLDI 2002, Proceeding, pp. 57–68. ACM (2002)

    Google Scholar 

  5. Dhurjati, D., Das, M., Yang, Y.: Path-sensitive dataflow analysis with iterative refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 425–442. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: ESEC-FSE 2005, Proceeding, pp. 227–236. ACM (2005)

    Google Scholar 

  7. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  8. Hammer, C., Schaade, R., Snelting, G.: Static path conditions for Java. In: PLAS 2008, Proceeding, pp. 57–66. ACM (2008)

    Google Scholar 

  9. Hardekopf, B., Lin, C.: Semi-sparse flow-sensitive pointer analysis. In: POPL 2009, Proceeding, pp. 226–238. ACM (2009)

    Google Scholar 

  10. Heinze, T.S., Amme, W.: Sparse analysis of variable path predicates (2016). http://swt.informatik.uni-jena.de/swt_multimedia/SWT/PDFs/heinze16.pdf

  11. Heinze, T.S., Amme, W., Moser, S.: A restructuring method for WS-BPEL business processes based on extended workflow graphs. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 211–228. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Heinze, T.S., Amme, W., Moser, S.: Compiling more precise petri net models for an improved verification of service implementations. In: SOCA 2014, Proceeding, pp. 25–32. IEEE (2014)

    Google Scholar 

  13. Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: POPL 1980, Proceeding, pp. 68–82. ACM (1980)

    Google Scholar 

  14. Kam, J.B., Ullman, J.D.: Monotone data flow analysis frameworks. Acta Inf. 7(3), 305–317 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  15. Murphy, B.R.: Frameworks for precise program analysis. Ph.D. thesis, Stanford University (2001)

    Google Scholar 

  16. Snelting, G.: Combining slicing and constraint solving for validation of measurement software. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 332–348. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  17. Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. ACM TOPLAS 13(2), 181–210 (1991)

    Article  Google Scholar 

  18. Winter, K., Zhang, C., Hayes, I.J., Keynes, N., Cifuentes, C., Li, L.: Path-sensitive data flow analysis simplified. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 415–430. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  19. Web Services Business Process Execution Language Version 2.0. OASIS Standard (2007). http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Friedrich Schiller University Jena, Jena, Germany

    Thomas S. Heinze & Wolfram Amme

Authors
  1. Thomas S. Heinze
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wolfram Amme
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thomas S. Heinze .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Heinze, T.S., Amme, W. (2016). Sparse Analysis of Variable Path Predicates Based upon SSA-Form. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47166-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47165-5

  • Online ISBN: 978-3-319-47166-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation