Sergio Mover

Assistant Professor

Department of Computer Science, École Polytechnique

Cosynus team, LIX - Computer Science Laboratory

I am interested in formal methods for Cyber-Physical Systems (CPSs), embedded systems, and mobile systems. I worked on model checking techniques for CPSs and embedded software using Satisfiability Modulo Theories (SMT), and on program analysis techniques for mobile apps (in particular for Android).

I am also interested in synthesis, “Big Code” (i.e., automatically learning from existing code to solve tasks like program synthesis or repair), model-based safety assessment, and planning (e.g., for hybrid domains).


  • SPIN 2021 conference: consider to submit to the SPIN-2021 conference (this year co-located with ECOOP and ISSTA). The deadline to submit is Monday March 1st 2021 (see the call for papers).
  • Ph.D. position at LIX: fully funded Ph.D. position at LIX (Ecole Polytechnique) and U2IS (ENSTA Paris) to start before June 2021: we're looking for a Ph.D. student to work at the intersection of robotics and formal methods (CoLeSlAw).
    Contact Sao Mai Nguyen and myself as soon as possible if you're interested.
  • IP Paris master - CPS Track: applications for the Cyber-Physical Systems track of the Master Program in Computer Science at the Institut Polytechnique de Paris (IPP). The first deadline to apply for the academic year 2021/2022 is February 7th 2021.
    Contact us if you need further information about the program.
    Consider also applying to the Ph.D. Track program (2 years of master + 3 years of Ph.D.) if you are an outstanding student.


Show list



An SMT-based symbolic model checker for hybrid systems


A symbolic model checker for finite- and infinite-state systems.


An open source symbolic model checker for finite-state systems.


A verification tool for event-driven application programming protocols.


A tool for mining programming patterns conserved across source code repositories.