Abstract interpretation is a formal mathematical framework which makes it possible to define and implement program analyses which are correct by construction -- provided that some basic properties are met. Software is an essential part of more and more complex systems. In order to master that complexity, it is necessary to be able to compute automatically reliable information about software. This is the goal of static analysis. To reason rigorously about programs, mathematical models of the behavior or programs are developed. Such models are called semantics. Depending on the properties to compute, we can use different semantics - some more detailed for more precision, others coarser for more efficiency. Abstract interpretation is a theory of approximation that allows the comparison of different semantics, or building new semantics through refinement or abstraction. Because all interesting properties of programs are undecidable, all static analysis methods introduce approximations in one way or another. Therefore, abstract interpretation is a good framework to give a unified vision of such methods and to compare them.
|SSC1||Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems||S|
|SSC5||Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools||A|
|Code||Learning Outcome||Associated competences||Proficiency level|
|RA-AV-8||Ability to use existing program static analysis, program formal verification and automatic program transformation tools||SSC5||A|
|RA-AV-9||Knowledge of the foundations of abstract interpretation as a method of program static analysis||SSC1||K|
Subject learning guide for Abstract Interpretation