Skip to main content
SpringerLink
Log in

JTDec: A Tool for Tree Decompositions in Soot

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2017)

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

Abstract

The notion of treewidth of graphs has been exploited for faster algorithms for several problems arising in verification and program analysis. Moreover, various notions of balanced tree decompositions have been used for improved algorithms supporting dynamic updates and analysis of concurrent programs. In this work, we present a tool for constructing tree-decompositions of CFGs obtained from Java methods, which is implemented as an extension to the widely used Soot framework. The experimental results show that our implementation on real-world Java benchmarks is very efficient. Our tool also provides the first implementation for balancing tree-decompositions. In summary, we present the first tool support for exploiting treewidth in the static analysis problems on Java programs.

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

Institutional subscriptions

References

  1. Blackburn, S.M., Garner, R., Hoffmann, C., Khang, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z.: The DaCapo benchmarks: Java benchmarking development and analysis. ACM SIGPLAN Not. 41(10), 169–190 (2006)

    Article  Google Scholar 

  2. Bodlaender, H., Gustedt, J., Telle, J.A.: Linear-time register allocation for a fixed number of registers. In: SODA 1998, pp. 574-583 (1998)

    Google Scholar 

  3. Bodlaender, H.L.: A tourist guide through treewidth. Acta Cybern. 11, 1 (1993)

    MathSciNet  MATH  Google Scholar 

  4. Bodlaender, H.L.: Discovering treewidth. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 1–16. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30577-4_1

    Chapter  Google Scholar 

  5. Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for quantitative verification in constant treewidth graphs. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 140–157. Springer, Cham (2015). doi:10.1007/978-3-319-21690-4_9

    Chapter  Google Scholar 

  6. Chatterjee, K., Lacki, J.: Faster Algorithms for markov decision processes with low treewidth. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 543–558. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_36

    Chapter  Google Scholar 

  7. Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A.: Optimal reachability and a space-time tradeoff for distance queries in constant-treewidth graphs. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 57. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  8. Chatterjee, K., Goharshady, A.K., Ibsen-Jensen, R., Pavlogiannis, A.: Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: ACM SIGPLAN Notices. vol. 51(1), pp. 733-747. ACM (2016)

    Google Scholar 

  9. Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., Goyal, P.: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: POPL. ACM (2015)

    Google Scholar 

  10. Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  11. Dendris, N.D., Kirousis, L.M., Thilikos, D.M.: Fugitive-search games on graphs and related parameters. Theoret. Comput. Sci. 172(1–2), 233–254 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  12. Elberfeld, M., Jakoby, A., Tantau, T.: Logspace versions of the theorems of Bodlaender, Courcelle. In: 2010 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 143-152. IEEE (2010)

    Google Scholar 

  13. Gustedt, J., Mæhle, O., Telle, J.: The treewidth of Java programs. Algorithm Eng. Exp. pp. 57–59 (2002)

    Google Scholar 

  14. Halin, R.: S-functions for graphs. J. Geom. 8(1–2), 171–186 (1976)

    Article  MATH  Google Scholar 

  15. Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_7

    Chapter  Google Scholar 

  16. Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J. Comb. Theor. Ser. B 36(1), 49–64 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  17. Thorup, M.: All structured programs have small tree width and good register allocation. Inf. Comput. 142(2), 159–181 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  18. Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, p. 13. IBM Press (1999)

    Google Scholar 

Download references

Acknowledgements

We thank all reviewers for their helpful comments which led to considerable improvements in presentation. The research is partially supported by Vienna Science and Technology Fund (WWTF) ICT15-003, Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE) and ERC Start grant (279307: Graph Games).

Author information

Authors and Affiliations

  1. IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400, Klosterneuburg, Austria

    Krishnendu Chatterjee, Amir Kafshdar Goharshady & Andreas Pavlogiannis

Authors
  1. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Kafshdar Goharshady
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andreas Pavlogiannis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Amir Kafshdar Goharshady .

Editor information

Editors and Affiliations

  1. Indian Institute of Science, Bangalore, India

    Deepak D'Souza

  2. Chennai Mathematical Institute, Kelambakkam, India

    K. Narayan Kumar

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Chatterjee, K., Goharshady, A.K., Pavlogiannis, A. (2017). JTDec: A Tool for Tree Decompositions in Soot. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68167-2_4

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation