Static Analysis Using Abstract Interpretation

Arthaud, Maxime

关键词: C++ (PROGRAMMING LANGUAGE);    LECTURES;    KERNEL FUNCTIONS;    INFERENCE;   

RP-ID  :  ARC-E-DAA-TN74713

美国|英语

来源: NASA Technical Reports Server

【 摘 要 】

Lecture about abstract interpretation. This lecture starts with a brief introduction to validation and verification using formal methods. It then demonstrates IKOS (Inference Kernel for Open Static Analyzers), a static analyzer for C/C++ based on Abstract Interpretation. Then, it describes in details the theory of Abstract Interpretation, a mathematical framework to over-approximate the reachable states of a program.