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
  • Verifying LTL properties of Hybrid Systems with K-liveness, to appear in CAV 2014.
    Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta.
  • The NUXMV Symbolic Model Checker, to appear in CAV 2014.
    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.
  • Quantier-free encoding of invariants for Hybrid Systems, to appear on Formal Methods in System Design (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 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