Skip to main content
SpringerLink
Log in
Book cover

Semantics, Logics, and Calculi pp 88–110Cite as

An Automata-Based Approach to Trace Partitioned Abstract Interpretation

  • Chapter
  • First Online:

  • 935 Accesses

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

Abstract

Trace partitioning is a technique for retaining precision in abstract interpretation, by partitioning all traces into a number of classes and computing an invariant for each class. In this work we present an automata-based approach to trace partitioning, by augmenting the finite automaton given by the control-flow graph with abstract transformers over a lattice. The result is a lattice automaton, for which efficient model-checking tools exist. By adding additional predicates to the automaton, different classes of traces can be distinguished.

This shows a very practical connection between abstract interpretation and model checking: a formalism encompassing problems from both domains, and accompanying machinery that can be used to solve problems from both domains efficiently.

This practical connection has the advantage that improvements from one domain can very easily be transferred to the other. We exemplify this with the use of multi-core processors for a scalable computation. Furthermore, the use of a modelling formalism as intermediary format allows the program analyst to simulate, combine and alter models to perform ad-hoc experiments.

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.

    Experiments were performed on a 8-core Intel Xeon X5570 machine, with 74Gb of RAM.

  2. 2.

    E.g. increased usage of the dynamic memory allocator: APRON uses dynamic resizing of some data structures, whereas the uppaal DBM library does not. In general dynamic memory allocation is more expensive in a multi-core shared-memory setting, because it potentially requires synchronisation.

References

  1. Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, New York (2008)

    MATH  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-73368-3_51

    Chapter  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  6. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252 (1977)

    Google Scholar 

  7. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does ASTRÉE scale up? Formal Meth. Syst. Des. 35(3), 229–264 (2009)

    Article  MATH  Google Scholar 

  8. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press, San Antonio (1979). http://dblp.org/db/conf/popl/popl79.html#CousotC79

  9. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  10. Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6, 69–95 (1999). http://dblp.org/db/journals/ase/ase6.html#CousotC99

    Article  Google Scholar 

  11. Dalsgaard, A.E., Hansen, R.R., Jørgensen, K.Y., Larsen, K.G., Olesen, M.C., Olsen, P., Srba, J.: opaal: a lattice model checker. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 487–493. Springer, Heidelberg (2011). http://dblp.org/db/conf/nfm/nfm2011.html#DalsgaardHJLOOS11

  12. Dalsgaard, A.E., Laarman, A., Larsen, K.G., Olesen, M.C., van de Pol, J.: Multi-core reachability for timed automata. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 91–106. Springer, Heidelberg (2012). http://dblp.org/db/conf/formats/formats2012.html#DalsgaardLLOP12

    Chapter  Google Scholar 

  13. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  15. Geeraerts, G., Raskin, J.F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180 (2006)

    Article  MATH  Google Scholar 

  16. Gopan, D., Reps, T.: Guided static analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349–365. Springer, Heidelberg (2007). http://dl.acm.org/citation.cfm?id=2391451.2391475

    Chapter  Google Scholar 

  17. Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 200–214. Springer, Heidelberg (1998). http://dblp.org/db/conf/sas/sas98.html#HandjievaT98

    Chapter  Google Scholar 

  18. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 58–70. ACM (2002)

    Google Scholar 

  19. Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39–50. Springer, Heidelberg (1999). http://dblp.org/db/conf/sas/sas99.html#JeannetHR99

    Chapter  Google Scholar 

  20. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). http://dblp.org/db/conf/sas/sas99.html#JeannetHR99

    Chapter  Google Scholar 

  21. Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Laarman, A.: Scalable multi-core model checking. Ph.D. thesis, University of Twente (2014)

    Google Scholar 

  23. Laarman, A., van de Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011). http://dblp.org/db/conf/nfm/nfm2011.html#LaarmanPW11

    Chapter  Google Scholar 

  24. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer (STTT) 1(1), 134–152 (1997)

    Article  MATH  Google Scholar 

  25. del Mar Gallardo, M., Martinez, J., Merino, P., Pimentel, E.: aSPIN: Extending SPIN with abstraction. In: Model Checking Software, pp. 241–252 (2002)

    Google Scholar 

  26. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  27. Miné, A.: The octagon abstract domain. High. Order Symbolic Comput. (HOSC) 19(1), 31–100 (2006)

    Article  MATH  Google Scholar 

  28. Monniaux, D.: The parallel implementation of the Astrée static analyzer. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 86–96. Springer, Heidelberg (2005). http://dx.doi.org/10.1007/11575467_7

    Chapter  Google Scholar 

  29. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York Inc., Secaucus (1999)

    Book  MATH  Google Scholar 

  30. Nielson, F., Nielson, H.R.: Model checking Is static analysis of modal logic. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 191–205. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  31. Olesen, M.C.: Program analysis as model checking. Ph.D. thesis, Aalborg University (defended December 2013)

    Google Scholar 

  32. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), 26 (2007). http://dblp.org/db/journals/toplas/toplas29.html#RivalM07

    Article  Google Scholar 

  33. Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  34. Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–365. Springer, Heidelberg (1991). http://dx.doi.org/10.1007/3-540-54415-1_54

    Chapter  Google Scholar 

  35. Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115–139 (1993). http://dx.doi.org/10.1016/0167-6423(93)90003-8

    Article  MATH  Google Scholar 

  36. Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 22–41. Springer, Heidelberg (1996). http://dblp.org/db/conf/sas/sas96.html#Steffen96

    Chapter  Google Scholar 

  37. Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995). http://dblp.org/db/conf/concur/concur1995.#htmlSteffenCKKM95

    Chapter  Google Scholar 

Download references

Acknowledgments

We would like to thank the LTSmin and APRON developers for making their excellent code available to others in the research community.

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Mads Christian Olesen, René Rydhof Hansen & Kim Guldstrand Larsen

Authors
  1. Mads Christian Olesen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. René Rydhof Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to René Rydhof Hansen .

Editor information

Editors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Christian W. Probst

  2. Imperial College London, London, United Kingdom

    Chris Hankin

  3. Aalborg University, Aalborg, Denmark

    René Rydhof Hansen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Olesen, M.C., Hansen, R.R., Larsen, K.G. (2016). An Automata-Based Approach to Trace Partitioned Abstract Interpretation. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27810-0_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27809-4

  • Online ISBN: 978-3-319-27810-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation