Supporting Requirements Validation: The EuRailCheck Tool. - Roberto Cavada; Alessandro Cimatti; Alessandro Mariotti; Cristian Mattarei; Andrea Micheli; Sergio Mover; Marco Pensallorto; Marco Roveri; Angelo Susi; Stefano Tonetta (ASE, 2009)

Model Checking of Hybrid Systems Using Shallow Synchronization. - Lei Bu; Alessandro Cimatti; Xuandong Li; Sergio Mover; Stefano Tonetta (FMOODS/FORTE, 2010)

From Sequential Extended Regular Expressions to NFA with Symbolic Labels. - Alessandro Cimatti; Sergio Mover; Marco Roveri; Stefano Tonetta (CIAA, 2010)

Efficient Scenario Verification for Hybrid Automata. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (CAV, 2011)

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (EUROMICRO-SEAA, 2011)

Proving and explaining the unfeasibility of message sequence charts for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (FMCAD, 2011)

Symbolic Model Checking and Safety Assessment of Altarica models. - Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

SMT-Based Verification of Hybrid Systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (AAAI, 2012)

A quantifier-free SMT encoding of non-linear hybrid automata. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (FMCAD, 2012)

Time-aware relational abstractions for hybrid systems. - Sergio Mover; Alessandro Cimatti; Ashish Tiwari 001; Stefano Tonetta (EMSOFT, 2013)

Parameter synthesis with IC3. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (FMCAD, 2013)

SMT-based scenario verification for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2013)

The nuXmv Symbolic Model Checker. - Roberto Cavada; Alessandro Cimatti; Michele Dorigatti; Alberto Griggio; Alessandro Mariotti; Andrea Micheli; Sergio Mover; Marco Roveri; Stefano Tonetta (CAV, 2014)

Verifying LTL Properties of Hybrid Systems with K-Liveness. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (CAV, 2014)

IC3 Modulo Theories via Implicit Predicate Abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2014)

Quantifier-free encoding of invariants for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2014)

Verification of Hybrid Systems using Satisfiability Modulo Theories. - Sergio Mover (2014)

Formal Verification of Infinite-State BIP Models. - Simon Bliudze; Alessandro Cimatti; Mohamad Jaber 001; Sergio Mover; Marco Roveri; Wajeb Saab; Qiang Wang 020 (ATVA, 2015)

Parameter Synthesis with IC3 (Informal Presentation). - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (SynCoP, 2015)

HyComp: An SMT-Based Model Checker for Hybrid Systems. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2015)

Safety assessment of AltaRica models via symbolic model checking. - Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta (Sci. Comput. Program., 2015)

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. - Jakub Daniel; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Sergio Mover (CAV (1), 2016)

From Electrical Switched Networks to Hybrid Automata. - Alessandro Cimatti; Sergio Mover; Mirko Sessa (FM, 2016)

Infinite-state invariant checking with IC3 and predicate abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2016)

SMT-based analysis of switching multi-domain linear Kirchhoff networks. - Alessandro Cimatti; Sergio Mover; Mirko Sessa (FMCAD, 2017)

Abstracting Event-Driven Systems with Lifestate Rules. - Shawn Meier; Aleksandar Chakarov; Maxwell Russek; Sergio Mover; Bor-Yuh Evan Chang (CoRR, 2017)

Learning Asynchronous Typestates for Android Classes. - Arjun Radhakrishna; Nicholas V. Lewchenko; Shawn Meier; Sergio Mover; Krishna Chaitanya Sripada; Damien Zufferey; Bor-Yuh Evan Chang; Pavol Cerný (CoRR, 2017)

Compositional Relational Abstraction for Nonlinear Hybrid Systems. - Xin Chen 002; Sergio Mover; Sriram Sankaranarayanan 001 (ACM Trans. Embed. Comput. Syst., 2017)

Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks. - Roberto Cavada; Alessandro Cimatti; Sergio Mover; Mirko Sessa; Giuseppe Cadavero; Giuseppe Scaglione (FMCAD, 2018)

DroidStar: callback typestates for Android classes. - Arjun Radhakrishna; Nicholas V. Lewchenko; Shawn Meier; Sergio Mover; Krishna Chaitanya Sripada; Damien Zufferey; Bor-Yuh Evan Chang; Pavol Cerný (ICSE, 2018)

Mining framework usage graphs from app corpora. - Sergio Mover; Sriram Sankaranarayanan 001; Rhys Braginton Pettee Olsen; Bor-Yuh Evan Chang (SANER, 2018)

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics. - Goran Frehse; Alessandro Abate; Dieky Adzkiya; Anna Becchi; Lei Bu; Alessandro Cimatti; Mirco Giacobbe; Alberto Griggio; Sergio Mover; Muhammad Syifa'ul Mufid; Idriss Riouak; Stefano Tonetta; et al. (ARCH@CPSIoTWeek, 2019)

Lifestate: Event-Driven Protocols and Callback Control Flow. - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (ECOOP, 2019)

Reaching Out Towards Fully Verified Autonomous Systems. - Sriram Sankaranarayanan 001; Souradeep Dutta; Sergio Mover (RP, 2019)

Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version). - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (CoRR, 2019)

Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact). - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (Dagstuhl Artifacts Ser., 2019)

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. - Sergio Mover; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Stefano Tonetta (CAV (1), 2021)

Verification modulo theories. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Marco Roveri; Stefano Tonetta (Formal Methods Syst. Des., 2022)

SMT-Based Stability Verification of an Industrial Switched PI Control Systems. - Stylianos Basagiannis; Ludovico Battista; Anna Becchi; Alessandro Cimatti; Georgios Giantamidis; Sergio Mover; Alberto Tacchella; Stefano Tonetta; Vassilios A. Tsachouridis (DSN-W, 2023)

Goal Space Abstraction in Hierarchical Reinforcement Learning via Set-Based Reachability Analysis. - Mehdi Zadem; Sergio Mover; Sao Mai Nguyen (ICDL, 2023)

Historia: Refuting Callback Reachability with Message-History Logics (Extended Version). - Shawn Meier; Sergio Mover; Gowtham Kaki; Bor-Yuh Evan Chang (CoRR, 2023)

Goal Space Abstraction in Hierarchical Reinforcement Learning via Reachability Analysis. - Mehdi Zadem; Sergio Mover; Sao Mai Nguyen (CoRR, 2023)

Historia: Refuting Callback Reachability with Message-History Logics. - Shawn Meier; Sergio Mover; Gowtham Kaki; Bor-Yuh Evan Chang (Proc. ACM Program. Lang., 2023)

Abstraction Techniques for Symbolic Model Checking of Infinite-state Discrete and Continuous Systems. - Sergio Mover (2024)

Reconciling Spatial and Temporal Abstractions for Goal Representation. - Mehdi Zadem; Sergio Mover; Sao Mai Nguyen (ICLR, 2024)