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.
Keywords
- Path Predicate
- Sparse Analysis
- Predicate Variables
- Static Single Assignment Form
- Single Assignment Property
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
For the complete proofs, we refer the reader to [10].
- 2.
References
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)
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)
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)
Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: PLDI 2002, Proceeding, pp. 57–68. ACM (2002)
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)
Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: ESEC-FSE 2005, Proceeding, pp. 227–236. ACM (2005)
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)
Hammer, C., Schaade, R., Snelting, G.: Static path conditions for Java. In: PLAS 2008, Proceeding, pp. 57–66. ACM (2008)
Hardekopf, B., Lin, C.: Semi-sparse flow-sensitive pointer analysis. In: POPL 2009, Proceeding, pp. 226–238. ACM (2009)
Heinze, T.S., Amme, W.: Sparse analysis of variable path predicates (2016). http://swt.informatik.uni-jena.de/swt_multimedia/SWT/PDFs/heinze16.pdf
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)
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)
Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: POPL 1980, Proceeding, pp. 68–82. ACM (1980)
Kam, J.B., Ullman, J.D.: Monotone data flow analysis frameworks. Acta Inf. 7(3), 305–317 (1977)
Murphy, B.R.: Frameworks for precise program analysis. Ph.D. thesis, Stanford University (2001)
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)
Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. ACM TOPLAS 13(2), 181–210 (1991)
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)
Web Services Business Process Execution Language Version 2.0. OASIS Standard (2007). http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)