Andrei Paskevich

Associate professor / Maître de conférences
Laboratoire Méthodes Formelles
Université Paris-Saclay, IUT d'Orsay
project-team Toccata, Inria Saclay

(photo)

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.

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) lmf (dot) cnrs (dot) fr

Last update: 25 Oct 2024