Skip to main content
SpringerLink
Log in

An Algebraic Approach to the Static Analysis of Concurrent Software

  • Conference paper
  • First Online:
Static Analysis (SAS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2477))

Included in the following conference series:

  • 666 Accesses

Abstract

In the last years a group of colleagues and I have developed a new approach to interprocedural program analysis based on ideas born in the model-checking community [2,3,4,6]. The Moped tool [8] is an implementation of most of this work. In interaction with the SLAM toolkit [1], Moped has been applied to the analysis of programs with thousands of lines of C code.

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 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. T. Ball and S. Rajamani: The SLAM Project: Debugging System Software via Static Analysis Conference Record of POPL’ 02, 1–3, ACM Press (2002).

    Google Scholar 

  2. A. Bouajjani, J. Esparza and O. Maler: Reachability Analysis of Pushdown Automata: Application to Model-Checking. Proceedings of CONCUR’ 97, LNCS 1243, 135–150 (1997).

    Google Scholar 

  3. J. Esparza, D. Hansel, P. Rossmanith and S. Schwoon: Efficient Model Checking Algorithms for Pushdown Systems. Proceedings of CAV’ 00, LNCS 1855, 232–247 (2000).

    Google Scholar 

  4. J. Esparza and J. Knoop: An Automata-theoretic Approach to Interprocedural Dataflow Analysis. Proceedings of FOSSACS’ 99, LNCS 1578, 14–30 (1999).

    Google Scholar 

  5. J. Esparza and A. Podelski: Efficient algorithms for pre* and post* on Interprocedural Parallel Flow Graphs. Conference Record of POPL’ 00, 1–11, ACM Press (2000).

    Google Scholar 

  6. J. Esparza and S. Schwoon: A BBD-Based Model Checker for Recursive Programs. Proceedings of CAV’ 01, LNCS 2102, 324–336 (2001).

    Google Scholar 

  7. M.W. Hopkins and D.C. Kozen: Parikh’s Theorem in Commutative Kleene Algebra Proceedings of LICS’99, IEEE, 394–401 (1999)

    Google Scholar 

  8. Moped-A Model-Checker for Pushdown Systems. Writen and maintained by Stefan Schwoon. Code available at http://www7.in.tum.de~schwoon/moped.

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, University of Edinburgh, Germany

    Javier Esparza

Authors
  1. Javier Esparza
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science Facultad de Informática, Technical University of Madrid, Campus de Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Manuel V. Hermenegildo  & Germán Puebla  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Esparza, J. (2002). An Algebraic Approach to the Static Analysis of Concurrent Software. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-45789-5_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44235-6

  • Online ISBN: 978-3-540-45789-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation