4541.664A Program Analysis: Theories and Practices

À̱¤±Ù Kwangkeun Yi
Programming Research Lab./CSE/Seoul National University

°­ÀÇ: È­/¸ñ 13:00-14:30 @ 302µ¿ 308È£

¸ñÇ¥ Objectives

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

¼ÒÇÁÆ®¿þ¾î¿¡ ´ëÇؼ­´Â ¾î¶²°¡? ÀÛ¼ºÇÑ ¼ÒÇÁÆ®¿þ¾î°¡ Á¦´ë·Î ½ÇÇàµÉ Áö¸¦ ¹Ì¸® ¾ö¹ÐÇÏ°Ô È®ÀÎÇØ ÁÖ´Â ±â¼úµéÀº Àִ°¡? ÀÌ¿¡ ´ëÇÑ ´äÀÌ ÇÁ·Î±×·¥ ºÐ¼®(static program analysis)±â¼ú À̶ó´Â À̸§À¸·Î ¸ð¿©Áö´Â ±â¼úµéÀÌ´Ù.

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

³»¿ë Contents

  • Preliminaries: abstract syntax, semantics, inductive definitions, logics and inference, fixpoints
  • Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, denotational semantics
  • Abstract interpretation: abstraction, concretization, galois connection, correctness, fixpoint algorithms
  • Type-based analysis: monomorphic type system, polymorphic type system, effect system, unification
  • Constraint-based analysis: set constraints, flow logics, constraint solving
  • Software model checking: model checking, program logics, abstraction refinement
  • Data-flow analysis: ad-hoc, engineering techniques

±ÔÁ¤ Policy

 ½ÃÇè: 20%, ¼÷Á¦: 30%, ÇÁ·ÎÁ§Æ®/³í¹®¹ßÇ¥: 50%
  • ¼ºÀûÀº Àý´ëÆò°¡.
  • Ãâ¼® 100%´Â Çʼö. ¾î¿ ¼ö ¾ø´Â °æ¿ì´Â ¹Ýµå½Ã »çÀü Çã¶ôÀ» ¹Þ´Â´Ù.

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

wk 1 preliminaries book5-24, slide1                    
wk 2 semantic formalisms I book25-50, slide2, slide3  
wk 3 semantic formalisms II slide4, slide5
wk 4 abstract interpretation I book61-75 slide6, slide7
wk 5 abstract interpretation II slide8, slide9, slide10
wk 6 abstract interpretation III book74-108, slide11
wk 7 abstract interpretation IV slide12, slide13 airac.ppt
EXAM I exam1
wk 8 type-based analysis I slide14, slide15 slide16
wk 9 type-based analysis II slide17, slide18
wk 10 constraint-based analysis I slide19, slide20
wk 11 constraint-based analysis II slide21 New
wk 12 software model-checking I slide22 New
EXAM II  

ÀÐÀ» ³í¹® Papers

¼÷Á¦ Homeworks

 
© Copyright 2005, ÀÌ ±¤±Ù Kwangkeun Yi