This book constitutes the refereed proceedings of the 13th International Symposium on Static Analysis, SAS 2006, held in Seoul, Korea in August 2006.

The 23 revised full papers presented together with the abstracts of 3 invited talks were carefully reviewed and selected from 80 submissions. The papers address all aspects of static analysis including program and systems verification, shape analysis and logic, termination analysis, bug detection, compiler optimization, software maintenance, security and safety, abstract interpretation and algorithms, abstract domain and data structures, pointer analysis, shape analysis, and data flow analysis.

APLAS 2005 was the Asian Symposium on Programming Languages and S- tems, held in Tsukuba, Japan in November 2 5, 2005. It was the latest event in the series of annual meetings started in 2000 by Asian researchers in the ?eld of programming languages and systems. The ?rst three were organized as wo- shops, and were held in Singapore(2000), Daejeon (2001), and Shanghai (2002). Theenthusiasmthere, encouragedbytherichproductionoforiginalresearch- pers, and the support of the internationalresearchcommunities in programming languagesandsystems, ledtothe?rstAPLASasasymposiuminBeijing(2003), followed by the one in Taipei (2004). APLAS 2005 was the third symposium in the series. In the past ?ve yearswe havewitnessed the growing role of APLAS as one of thekeyresearchcommunitiesoftheworld.ThisisnotonlybecauseAsia andthe Paci?c Rim is a fast-growing region of IT industries, but because it is a region of highly cultivated human resources. We are con?dent that forums like APLAS will further engender interaction among Asian researchers and with the rest of the world. As for the scope of APLAS, from the very beginning we have been striving to achieve the cross-fertilization of theories and system developments of p- gramming and programming languages. The papers selected for the publication of this volume of the proceedings are the evidence of our e?orts. We are very grateful to the contributors of the submitted papers; they came not only from Asia and Australia but from Europe and North America.

A self-contained introduction to abstract interpretation-based static analysis, an essential resource for students, developers, and users. Static program analysis, or static analysis, aims to discover semantic properties of programs without running them. It plays an important role in all phases of development, including verification of specifications and programs, the synthesis of optimized code, and the refactoring and maintenance of software applications. This book offers a self-contained introduction to static analysis, covering the basics of both theoretical foundations and practical considerations in the use of static analysis tools. By offering a quick and comprehensive introduction for nonspecialists, the book fills a notable gap in the literature, which until now has consisted largely of scientific articles on advanced topics. The text covers the mathematical foundations of static analysis, including semantics, semantic abstraction, and computation of program invariants; more advanced notions and techniques, including techniques for enhancing the cost-accuracy balance of analysis and abstractions for advanced programming features and answering a wide range of semantic questions; and techniques for implementing and using static analysis tools. It begins with background information and an intuitive and informal introduction to the main static analysis principles and techniques. It then formalizes the scientific foundations of program analysis techniques, considers practical aspects of implementation, and presents more advanced applications. The book can be used as a textbook in advanced undergraduate and graduate courses in static analysis and program verification, and as a reference for users, developers, and experts.