Post-Doctoral reasearcher at Fondazione Bruno Kessler, Embedded System Unit.
Contact: mover [at] fbk.eu
Research Interests
Formal methods, verification of hybrid systems, verification of infinite-state systems, abstraction refinement techniques, parameter synthesis, satisfiability modulo theories.
Software
PhD Thesis
Verification of Hybrid Systems using Satisfiability Modulo Theories (PDF)
I defended my PhD Thesis in March 2014.
The thesis was supervised by Alessandro Cimatti and Stefano Tonetta.
Publications
  • Formal verification of infinite-state BIP models, to appear in ATVA 2015.
    Simon Bliudze Alessandro Cimatti, Mohamad Jaber, Sergio Mover,Marco Roveri, Wajeb Saab, Qiang Wang
  • HyCOMP: an SMT-based model checker for Hybrid Systems, TACAS 2015 (PDF).
    Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta.
  • Safety Assesment of AltaRica models via symbolic model checking, Science of Computer Programming, Volume 98, Issue 4, 2014 (PDF).
    Marco Bozzano, Alessandro Cimatti, Oleg Lisagor, Cristian Mattarei, Sergio Mover, Marco Roveri, Stefano Tonetta
  • Verifying LTL properties of Hybrid Systems with K-liveness, CAV 2014 (PDF).
    Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta.
  • The NUXMV Symbolic Model Checker, CAV 2014 (PDF).
    Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta
  • IC3 Modulo Theories via Implicit Predicate Abstraction, TACAS 2014 (PDF).
    Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta.
  • Quantifier-free encoding of invariants for Hybrid Systems, Formal Methods in System Design, Volume 45, Issue 2, October 2014 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • Parameter Synthesis with IC3, FMCAD 2013 (PDF)
    Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta.
  • Time-aware Relational Abstractions for Hybrid Systems, EMSOFT 2013 (PDF)
    Sergio Mover, Alessandro Cimatti, Ashish Tiwari, Stefano Tonetta.
  • SMT-based scenario verification for Hybrid Systems, Formal Methods in System Design, Volume 42 Issue 1, February 2013 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • SMT-Based Verification of Hybrid Systems, AAAI 2012 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • Quantifier-free SMT encoding of non-linear hybrid automata, FMCAD 2012 (Best Paper Award) (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • Symbolic Model Checking and Safety Assessment of Altarica models, AVOCS 2011 (PDF)
    Marco Bozzano, Alessandro Cimatti, Oleg Lisagor, Cristian Mattarei, Sergio Mover, Marco Roveri and Stefano Tonetta.
  • Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems, FMCAD 2011 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • HYDI: a language for symbolic hybrid systems with discrete interaction, EUROMICRO-SEAA 2011 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • Efficient Scenario Verification for Hybrid Automata, CAV 2011 (PDF)
    Alessandro Cimatti, Sergio Mover, Stefano Tonetta.
  • From Sequential Extended Regular Expressions to NFA with Symbolic Labels, CIAA 2010 (PDF)
    Alessandro Cimatti, Sergio Mover, Marco Roveri, Stefano Tonetta.
  • Model Checking of Hybrid Systems Using Shallow Synchronization, FORTE 2010 (PDF)
    Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta.
  • Supporting Requirements Validation: The EuRailCheck Tool, ASE 2009
    Roberto Cavada, Alessandro Cimatti, Alessandro Mariotti, Cristian Mattarei, Andrea Micheli, Sergio Mover, Marco Pensallorto, Marco Roveri, Angelo Susi, Stefano Tonetta.
Teaching
  • 2009/2010 Teaching Assistant for the Functional Programming course
  • 2008/2009 Teaching Assistant for the Functional Programming course