4541.664A Program Analysis: Theories and Practices

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

°­ÀÇ: È­/¸ñ 15:30-16: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%. ¼ºÀûÀº Àý´ëÆò°¡.
TA:   À̵¿±Ç: {dklee} AT ropas.snu.ac.kr

¼÷Á¦ Homeworks

  • ÇÁ·Î±×·¥ ¼÷Á¦´Â ÄÄÇ»Å͸¦ ÅëÇØ Á¦ÃâÇÕ´Ï´Ù.
  • Á¦Ãâ±âÇÑÀ» Áö³ª 48½Ã°£ À̳»·Î ´Ê¾îÁö¸é 10% °¨Á¡. ±× ÀÌÈÄÀÇ ¼÷Á¦´Â ¹ÞÁö ¾Ê½À´Ï´Ù.
  • ÇÁ·Î±×·¥ ¼÷Á¦´Â OCaml·Î ÀÛ¼ºÇÕ´Ï´Ù.
  • HW1 due 9/19. OCaml programming + basic concepts
  • HW2 due 10/17. Galois connection, a static analysis design trial
  • HW3 due 11/05 & 11/09. Static analysis design & implementation (I): Spaceplane code static analyzer (compositional style)
  • HW4 due 11/20. Static analysis design & implementation (II): daVinci code static analyzer, SW¸Å¿¬ Àú°¨ÀåÄ¡ ÀÎÁõ±â (compositional style)
  • HW5 due 12/12. Static analysis design & implementation (III): oWon code static analyzer New

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

Textbook: Introduction to Static Analysis: an Abstract Interpretation Perspective, MIT Press, February 2020. [PDF»ùÇÃ]
  • ½Ç¶óºÎ½º
  • slides 0: lecture roadmap -- gentle introduction, motivations for formal concepts, general framework, scalability, specialized frameworks
  • slides 1: inductive definition, induction proof, inference rules, soundness, completeness
  • slides 2: denotational semantics, semantic domain, semantic function, fixpoint
  • slides 3: operational semantics, semantic domain, semantic function, fixpoint
  • slides 4: abstract interpretation framework (part I)
  • slides 5: abstract interpretation framework (part II)
  • slides 6: abstract interpretation framework (part III)
  • slides 7: abstract interpretation framework (part IV)
  • slides 8: abstract interpretation framework (part V)
  • slides 9: sparse analysis framework for analysis scalability
  • slides 10: specialized frameworks: static analysis by equations, monotonic closure, or proof construction

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