4541.664A Program Analysis: Theories and Practices

À̱¤±Ù Kwangkeun Yi
(¼ÒÇÁÆ®¿þ¾î¹«°áÁ¡ ¿¬±¸¼¾ÅÍ)/ ÇÁ·Î±×·¡¹Ö ¿¬±¸½Ç/CSE/Seoul National University

°­ÀÇ: È­/¸ñ 15:30-14:45 @ 302µ¿ 309-1È£

¸ñÇ¥ Objectives

Á¦´ë·Î ÀÛµ¿ÇÒ Áö¸¦ ¹Ì¸® °ËÁõÇÒ ¼ö ¾ø´Â ±â°è¼³°è´Â ¾ø´Ù. Á¦´ë·Î ¼­ÀÖÀ» Áö¸¦ ¹Ì¸® °ËÁõÇÒ ¼ö ¾ø´Â °ÇÃ༳°è´Â ¾ø´Ù. Àΰø¹°µéÀÌ ÀÚ¿¬¼¼°è¿¡¼­ ¹®Á¦ ¾øÀÌ ÀÛµ¿ÇÒ Áö¸¦ ¹Ì¸® ¾ö¹ÐÇÏ°Ô ºÐ¼®ÇÏ´Â ¼öÇÐÀû ±â¼úµéÀº Àß ¹ß´ÞÇØ ¿Ô´Ù. ´ºÆ° ¿ªÇÐ, ¹ÌÀûºÐ ¹æÁ¤½Ä, Åë°è ¿ªÇеîÀÌ ±×·¯ÇÑ ±â¼úµéÀÏ °ÍÀÌ´Ù.

¼ÒÇÁÆ®¿þ¾î¿¡ ´ëÇؼ­´Â ¾î¶²°¡? ÀÛ¼ºÇÑ ¼ÒÇÁÆ®¿þ¾î°¡ Á¦´ë·Î ½ÇÇàµÉ Áö¸¦ ¹Ì¸® ¾ö¹ÐÇÏ°Ô È®ÀÎÇØ ÁÖ´Â ±â¼úµéÀº Àִ°¡? ÀÌ¿¡ ´ëÇÑ ´äÀÌ ÇÁ·Î±×·¥ ºÐ¼®(static program analysis)±â¼ú À̶ó´Â À̸§À¸·Î ¸ð¿©Áö´Â ±â¼úµéÀÌ´Ù. ±×µ¿¾È ´Ù¾çÇÑ À̸§À¸·Î ´Ù¾çÇÑ ¼öÁØ¿¡¼­ ´Ù¾çÇÑ ÇÊ¿ä¿¡ ¸ÂÃß¾î ºÒ¸®¿öÁö´Â ±â¼úµéÀ» ¸ðµÎ Æ÷¼·ÇÑ´Ù: "static analysis", "abstract interpretation", "type system", "software model checking", "data-flow analysis", "program logics and proof system" µî.

ÀÌ °­Á¿¡¼­´Â Á¤Àû ÇÁ·Î±×·¥ ºÐ¼® ±â¼úµéÀÇ À̷аú ½ÇÁ¦¸¦ ÀÍÈù´Ù.

  • °­ÀÇ
    • À§ÀÇ ¸ðµç ±â¼úµéÀ» Æ÷¼·ÇÏ´Â ÀÏ¹Ý Á¤ÀûºÐ¼® µðÀÚÀΠƲÀÎ ¿ä¾àÇؼ®(abstract interpretation)°ú ±× ¹è°æÀÌ·ÐÀ» ÀÍÈù´Ù.
    • ¿ä¾àÇؼ®¸¸Å­ ÀϹÝÀûÀÌÁö´Â ¾ÊÁö¸¸ Á¦ÇÑµÈ °æ¿ì¿¡ °£ÆíÇÏ°Ô »ç¿ëÇÒ ¼ö Àִ ƯȭµÈ Á¤ÀûºÐ¼® µðÀÚÀΠƲ ¼¼ °¡Áö(analysis by equation, by monotonic closure, and by proof construction)¸¦ ÀÍÈù´Ù.
    • Á¤ÀûºÐ¼®±âÀÇ ½ÇÇà ºñ¿ëÀ» ÁÙÀÌ´Â ´ëÇ¥ÀûÀÎ ±â¼úµéÀ» ÀÍÈù´Ù.
  • ¼÷Á¦
    • Á¤ÀûºÐ¼®±â µðÀÚÀο¡ ÇÊ¿äÇÑ °³³ä ÈÆ·ÃÇϱâ.
    • ¿ä¾àÇؼ® Ʋ(ÀÌ·Ð)À» ÀÌ¿ëÇؼ­ Á¤ÀûºÐ¼®±â¸¦ µðÀÚÀÎÇÏ°í µðÀÚÀÎÇÑ ºÐ¼®±â°¡ ¾ÈÀüÇÔÀ» Áõ¸íÇϱâ.
    • µðÀÚÀÎÀ» ½ÇÁ¦ ÇÁ·Î±×·¥À¸·Î ±¸ÇöÇÏ°í ½ÇÇàÇØ º¸±â.

³»¿ë Contents

  • Preliminaries: abstract syntax, semantics, inductive definitions, logics and inference, fixpoints
  • Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, denotational semantics
  • General framework: abstract interpretation, transitional approach, compositional approach, abstraction, concretization, galois connection, correctness, fixpoint algorithms
  • Specialized frameworks: analysis by equations, analysis by monotonic closure, analysis by proof construction, data flow analysis, constraint-based analysis, monomorphic type system, polymorphic type system, effect system
  • Implementations: algorithms, worklist, sparse analysis
  • Exercises: design and development of static analyzers

±ÔÁ¤ Policy

  ¼÷Á¦ 90%. ±âŸ 10%. ¼ºÀûÀº Àý´ëÆò°¡.

¼÷Á¦ Homeworks

  • ÇÁ·Î±×·¥ ¼÷Á¦´Â À̸ÞÀÏ·Î Á¶±³¿¡°Ô Á¦ÃâÇÕ´Ï´Ù.
  • Á¦Ãâ±âÇÑÀ» Áö³ª 48½Ã°£ À̳»·Î ´Ê¾îÁö¸é 10% °¨Á¡. ±× ÀÌÈÄÀÇ ¼÷Á¦´Â ¹ÞÁö ¾Ê½À´Ï´Ù.
  • ÇÁ·Î±×·¥ ¼÷Á¦´Â OCaml·Î ÀÛ¼ºÇÕ´Ï´Ù.
  • HW1 due 10/11 in class. Basic concepts, semantic exercises, induction proof about semantics.
  • HW2 due 10/27+10/31. Compositional-style static analysis design & implementation exercises. KX-22·ÎÄÏ ¸ðµâ °ËÁõ±â.
  • HW3 due 11/15 in class. Transitional-style static analysis designs. daVinci ÄÚµå °ËÁõ±â + SW¸Å¿¬ Àú°¨ÀåÄ¡ °ËÁõ±â.

Áøµµ¹× ÀÚ·á Slides & Resources

Textbook: Introduction to Static Analysis: an Abstract Interpretation Perspective, MIT Press, February 2020.

  
To view/print PDF files: Acrobat Reader
© Copyright 2013, ÀÌ ±¤±Ù Kwangkeun Yi