Kwangkeun Yi
School of Computer Science and Engineering
Seoul National University
Republic of Korea
Collage of static analyses in practice and theory
Abstract
This course will consist of three parts about static analysis. First, I will summarize the abstract interpretation framework, the most powerful design theory of static analysis. Then I will explain how we can engineer a realistic, industrial-strength global static analyzer to make it scalable up to million lines of C code. Building a sound, global, yet scalable semantic analysis for C is an elusive goal. The key technique is how to make the analysis sparse in terms of space, time, and context. Finally, I will introduce a theoretical static analysis framework for multi-staged (a.k.a. meta-programming) calculus that treats program code as value. Multi-staged calculus is a model for run-time code generation that frequently occurs in script or web programming.
Course materials
- K. Yi. Collage of static analyses in practice and theory. Lecture slides for EWSCS '12, 2012. part 1 [pdf], part 2 [pdf], part 3 [pdf], part 4 [pdf]
- P. Cousot. Abstract interpretation based formal methods and future challenges. In R. Wilhelm, ed., Informatics - 10 Years Back, 10 Years Ahead, v. 2000 of Lect. Notes in Comput. Sci., pp. 138-156 Springer, 2001. [doi: 10.1007/3-540-44577-3_10]
- H. Oh, K. Heo, W. Lee, W. Lee, K. Yi. Design and implementation of sparse global analyses for C-like languages. In Proc. of 33rd ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI 2012 (Beijing, June 2012), ACM Press, to appear.
- H. Oh, L. Brutschy, K. Yi. Access analysis-based tight localization of abstract memories. In R. Jhala, D. A. Schmidt, eds., Proc. of 12th Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI 2011 (Austin, TX, Jan. 2011), v. 6538 of Lect. Notes in Comput. Sci., pp. 356-370. Springer, 2011. [doi: 10.1007/978-3-642-18275-4_25]
- H. Oh, K. Yi. Access-based localization with bypassing. In H. Yang, ed., Proc. of 9th Asian Symp. on Programming Languages and Systems, APLAS 2011 (Kenting, Dec. 2011), v. 7078 of Lect. Notes in Comput. Sci., pp. 50-65. Springer, 2011. [doi: 10.1007/978-3-642-25318-8_7]
- W. Lee, W. Lee, K. Yi. Sound non-statistical clustering of static analysis alarms. In V. Kuncak, A. Rybalchenko, eds., Proc. of 13th Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI 2012 (Philadelphia, PA, Jan. 2012), v. 7148 of Lect. Notes in Comput. Sci., pp. 299-314. Springer, 2012. [doi: 10.1007/978-3-642-27940-9_20]
- W. Choi, B. Aktemur, K. Yi, M. Tatsuta. Static analysis of multi-staged programs via unstaging translation. In Proc. of 38th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, POPL 2011 (Austin, TX, Jan. 2011), pp. 81-92. ACM Press, 2011. [doi: 10.1145/1926385.1926397]
- H. Kim, Y. Jung, S. Kim, K. Yi. MeCC: memory comparison-based clone detector. In Proc. of 33rd Int. Conf. on Software Engineering, ICSE 2011 (Honolulu, HI, May 2011), pp. 301-310. ACM Press, 2011. [doi: 10.1145/1985793.1985835]
Last changed
March 4, 2012 15:01 EET
by
local organizers, ewscs12(at)cs.ioc.ee
EWSCS'12 page:
http://cs.ioc.ee/ewscs/2012/