Markus Müller-Olm
Institut für Informatik
Westfälische Wilhelms-Universität Münster
Germany
Program Analysis of Sequential and Parallel Programs
Abstract
For various reasons, computer programs must be analyzed and processed after or during their construction. A particular challenge for automatic program analyses are aspects that induce an unbounded or even infinite state space. Examples include data aspects like unrestricted value domains as well as control aspects like call/return behavior of (potentially recursive) procedures or thread creation.
These lectures present techniques for constructing automatic program analyses and arguing about their soundness and optimality. It will cover fixpoint-based as well as automata-based approaches. Special emphasis will be given to techniques for analyzing infinity aspects of program behavior. In particular, I will consider analysis of parallel programs.
The literature on program analysis is vast such that it is impossible to give a representative or even complete reference list here. Below I cite only some of my own, more recent papers. These and further articles relevant to these lectures can be downloaded from my homepage. References to work of other authors can be found in these papers.
Course materials
- M. Müller-Olm. Program analysis of sequential and parallel programs. Lecture slides for EWSCS 2009. 2009. [pdf]
- M. Müller-Olm, H. Seidl.
Precise interprocedural analysis through linear algebra.
In Proc. of 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages,
POPL '04 (Venice, Jan. 2004), pp. 330-341. ACM Press, 2004.
[pdf] © ACM - Peter Lammich, M. Müller-Olm.
Precise fixpoint-based analysis of programs with thread-creation and procedures.
In L. Caires, V. T. Vasconcelos, eds.,
Proc. of 18th Int. Conf. on Concurrency Theory, CONCUR 2007 (Lisbon, Sept. 2007),
v. 4703 of Lect. Notes in Comput. Sci., pp. 287-302.
Springer, 2007.
[pdf] © Springer
Version with appendix: [pdf] - A. Bouajjani, M. Müller-Olm, T. Touili.
Regular symbolic analysis of dynamic networks of pushdown systems.
In M. Abadi, L. de Alfaro, eds.,
Proc. of 16th Int. Conf. on Concurrency Theory, CONCUR 2005 (San Francisco, CA, Aug. 2005),
v. 3653 of Lect. Notes in Comput. Sci., pp. 473-487. Springer, 2005.
[pdf] © Springer
Further reading
- P. Lammich, M. Müller-Olm. Conflict analysis of programs with
procedures, dynamic thread creation, and monitors.
In M. Alpuente, G. Vidal, eds.,
Proc. of 15th Int. Static Analysis Symp., SAS 2008 (Valencia, July 2008),
v. 5079 of Lect. Notes in Comput. Sci., pp. 205-220, Springer, 2008.
[pdf] © Springer
Technical Report version with appendices, March 2008: [pdf] - M. Müller-Olm, H. Seidl.
Analysis of modular arithmetic.
ACM Trans. on Program. Lang. and Syst., v. 29, n. 5, article 29, 2007.
[pdf] - M. Müller-Olm, H. Seidl.
A note on Karr's algorithm.
In J. Diaz, J. Karhumäki, A. Lepistö, D. Sannella, eds., Proc. of 31st Int. Coll. on Automata, Languages, and
Programming, ICALP 2004 (Turku, July 2004), v. 3142 of Lect. Notes in Comput. Sci., pp. 1016-1028. Springer, 2004.
[pdf] © Springer - M. Müller-Olm. Variations on Constants: Flow Analysis of Sequential and Parallel Programs, v. 3800 of Lect. Notes in Comput. Sci.. Springer, 2006.
Last changed
March 7, 2009 17:18 EET
by
local organizers, ewscs09(at)cs.ioc.ee
EWSCS'09 page:
http://cs.ioc.ee/ewscs/2009/