Introduction to Static Program Analysis
Why static analysis matters and key concepts around soundness and completeness.
Introduction
Structure of Programming Language
Theory
Environment
Application
- Program analysis(You are here!)
- Program verification
- Program synthesis
Why do we need program analysis?
- Program Reliability
- Program Security
- Compiler Optimization
- Program Understanding
Static Analysis
analysis program P to reason about its behaviors and determines whether it satisfies some demands before running.
Rice Theory: Any non-trival property of the behavior of programs in a r.e language is undecidable. 鎬荤殑鏉ヨ锛屼竴涓畬缇庣殑闈欐€佸垎鏋愭槸涓嶅瓨鍦ㄧ殑
Perfect Static Analysis can not be done:Sound&Complete
=>Sound ~= overapproximate
=>Complete ~= underapproximate
p.s:Sound鍜孋omplete浜岄€変竴锛氶€塻ound鍒欏嚭鐜癴alse positive璇姤锛岄€塩omplete鍒欏嚭鐜癴alse negative婕忔姤
涓€鑸潵璇达紝鎴戜滑鏇村€惧悜soundness
Necessity of Soundness
Soundness is critical in compiler optimization and program verification