Sergio Mover

Sao Mai Nguyen

Proceedings of the Twelfth International Conference on Learning Representations, 2024

Abstraction Techniques for Symbolic Model Checking of Infinite-state Discrete and Continuous Systems.

[BibT_eX]

[DOI]

, 2024

2023

Historia: Refuting Callback Reachability with Message-History Logics.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., October, 2023

Goal Space Abstraction in Hierarchical Reinforcement Learning via Reachability Analysis.

[BibT_eX]

[DOI]

Mehdi Zadem

Sao Mai Nguyen

CoRR, 2023

Historia: Refuting Callback Reachability with Message-History Logics (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Goal Space Abstraction in Hierarchical Reinforcement Learning via Set-Based Reachability Analysis.

[BibT_eX]

[DOI]

Mehdi Zadem

Vassilios A. Tsachouridis

Sao Mai Nguyen

Proceedings of the IEEE International Conference on Development and Learning, 2023

SMT-Based Stability Verification of an Industrial Switched PI Control Systems.

[BibT_eX]

[DOI]

Stylianos Basagiannis

Proceedings of the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2023

2022

Verification modulo theories.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2022

2021

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2019

Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2019

Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2019

Reaching Out Towards Fully Verified Autonomous Systems.

[BibT_eX]

[DOI]

Sriram Sankaranarayanan

Souradeep Dutta

Proceedings of the Reachability Problems - 13th International Conference, 2019

Lifestate: Event-Driven Protocols and Callback Control Flow.

[BibT_eX]

[DOI]

Proceedings of the 33rd European Conference on Object-Oriented Programming, 2019

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.

[BibT_eX]

[DOI]

Muhammad Syifa'ul Mufid

Idriss Riouak

Enea Zaffanella

Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

2018

Mining framework usage graphs from app corpora.

[BibT_eX]

[DOI]

Rhys Braginton Pettee Olsen

Sriram Sankaranarayanan

Proceedings of the 25th International Conference on Software Analysis, 2018

DroidStar: callback typestates for Android classes.

[BibT_eX]

[DOI]

Arjun Radhakrishna

Nicholas V. Lewchenko

Krishna Chaitanya Sripada

Damien Zufferey

Pavol Cerný

Proceedings of the 40th International Conference on Software Engineering, 2018

Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

Compositional Relational Abstraction for Nonlinear Hybrid Systems.

[BibT_eX]

[DOI]

Xin Chen

Sriram Sankaranarayanan

ACM Trans. Embed. Comput. Syst., 2017

Learning Asynchronous Typestates for Android Classes.

[BibT_eX]

[DOI]

Arjun Radhakrishna

Nicholas V. Lewchenko

Krishna Chaitanya Sripada

Damien Zufferey

Pavol Cerný

CoRR, 2017

Abstracting Event-Driven Systems with Lifestate Rules.

[BibT_eX]

[DOI]

CoRR, 2017

SMT-based analysis of switching multi-domain linear Kirchhoff networks.

[BibT_eX]

[DOI]

Mirko Sessa

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

Infinite-state invariant checking with IC3 and predicate abstraction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

From Electrical Switched Networks to Hybrid Automata.

[BibT_eX]

[DOI]

Mirko Sessa

Proceedings of the FM 2016: Formal Methods, 2016

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Safety assessment of AltaRica models via symbolic model checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

HyComp: An SMT-Based Model Checker for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Parameter Synthesis with IC3 (Informal Presentation).

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Formal Verification of Infinite-State BIP Models.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Verification of Hybrid Systems using Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

PhD thesis, 2014

Quantifier-free encoding of invariants for hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

IC3 Modulo Theories via Implicit Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Verifying LTL Properties of Hybrid Systems with K-Liveness.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

The nuXmv Symbolic Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

SMT-based scenario verification for hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Parameter synthesis with IC3.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Time-aware relational abstractions for hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2013

2012

A quantifier-free SMT encoding of non-linear hybrid automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2012

SMT-Based Verification of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

2011

Symbolic Model Checking and Safety Assessment of Altarica models.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Proving and explaining the unfeasibility of message sequence charts for hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction.

[BibT_eX]

[DOI]

Proceedings of the 37th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2011, Oulu, Finland, August 30, 2011

Efficient Scenario Verification for Hybrid Automata.

[BibT_eX]

[DOI]