Andrei Paskevich

Associate professor / Maître de conférences
LRI / VALS, Paris-Sud University, IUT d'Orsay
project-team Toccata, Inria Saclay


My research interests lie in formal verification and automated reasoning. Together with other members of the Toccata team, I develop Why3, a platform for deductive program verification. Why3 provides a functional language with contracts, called WhyML, and uses third-party theorem provers to discharge verification conditions. WhyML can be compiled to OCaml. It also serves as an intermediate language for verification of C and Ada programs.

Between 2000 and 2008, I took part in the Evidence Algorithm project. We developed a mathematical assistant, called System for Automated Deduction (SAD) and intended for automated verification of formalized mathematical texts. SAD processes texts written in ForTheL, a variant of controlled English language that closely follows the natural language and style of mathematical publications.

In 2008, I contributed to the development of CiME 3, a tool for certification of termination proofs for term rewriting systems and also an automated termination prover.

Here you can find my publications.

I teach a course on Unix system programming (Principes des systèmes d'exploitation, M3101) at the IUT d'Orsay. In preparation of the lecture slides (C), I used materials by Dominique Gouyou-Beauchamps and Lydia Nicaud. The classroom notes (TD and TP) are mostly derived from the system programming course by Cédric Bastoul, to whom I owe the overall presentation and the majority of exercises.

Course materials (in French): C1 C2 C3 C4 C5 C6 C7 C8 TD1 TD2 TD3 TD4 TD5 TP0 TP1 TP2 TP3 TP4

andrei (at) lri (dot) fr

Last update: 22 Mar 2016