Semantics and program analysis - 4MM1SAP

• General notions : operational semantics of imperative programming languages, how to express the properties of programs, exact or approximate verification;
• Elements of theory: fixed point and decidability
• Development of a complete verification chain based on abstract interpretation principles, from the text of the program to the answer of a verification tool.

• Algorithms and imperative programming
• Language theory

Give kind of exam for session 1 and session 2: written, allowed documents or not, oral, practical work, reports, plan, vivas

Session 1 : un examen écrit de 2h en fin de 1ère période (E1a), un examen écrit de 2h en fin de deuxième période (E1b). La note est N1 = E1 = (E1a + E1b)/2
Session 2 : un examen écrit de 1h30 (E2) qui remplace tout : N2 = E2
Pour toutes les épreuves écrites : tous documents autorisés. Toute machine communicante interdite.