Stefano Tonetta

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

A comprehensive framework for the analysis of automotive systems.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, 2022

COMPASTA: Extending TASTE with Formal Design and Verification Functionality.

[BibT_eX]

[DOI]

Proceedings of the Model-Based Safety and Assessment - 8th International Symposium, 2022

A first-order logic characterisation of safety and co-safety languages.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2022

2021

The VALU3S ECSEL project: Verification and validation of automated systems safety and security.

[BibT_eX]

[DOI]

Joseba Andoni Agirre

Leire Etxeberria

Raul Barbosa

Stylianos Basagiannis

Georgios Giantamidis

Thomas Bauer

Enrico Ferrari

Mikel Labayen Esnaola

Microprocess. Microsystems, November, 2021

Certifying proofs for SAT-based model checking.

[BibT_eX]

[DOI]

Alberto Griggio

Formal Methods Syst. Des., 2021

Expressiveness of Extended Bounded Response LTL.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 12th International Symposium on Games, 2021

Assumption-Based Runtime Verification of Infinite-State Systems.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 21st International Conference, 2021

Assumptions and Guarantees for Composable Models in Papyrus for Robotics.

[BibT_eX]

[DOI]

Proceedings of the 3rd IEEE/ACM International Workshop on Robotics Software Engineering, 2021

Modelling the Component-based Architecture and Safety Contracts of ArmAssist in Papyrus for Robotics.

[BibT_eX]

[DOI]

Proceedings of the 3rd IEEE/ACM International Workshop on Robotics Software Engineering, 2021

A Proposal for the Classification of Methods for Verification and Validation of Safety, Cybersecurity, and Privacy of Automated Systems.

[BibT_eX]

[DOI]

Proceedings of the Quality of Information and Communications Technology, 2021

Model-based Analysis Support for Dependable Complex Systems in CHESS.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development, 2021

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.

[BibT_eX]

[DOI]

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

2020

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators.

[BibT_eX]

[DOI]

Inf. Comput., 2020

Safe Decomposition of Startup Requirements: Verification and Synthesis.

[BibT_eX]

[DOI]

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

HUBCAP: A Novel Collaborative Approach to Model-Based Design of Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the Simulation and Modeling Methodologies, Technologies and Applications, 2020

A Cloud-based Collaboration Platform for Model-based Design of Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Simulation and Modeling Methodologies, 2020

Model-Based Safety Analysis of Mode Transitions.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2020

Reactive Synthesis from Extended Bounded Response LTL Specifications.

[BibT_eX]

[DOI]

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

2019

COMPASS 3.0.

[BibT_eX]

[DOI]

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

Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2019

NuRV: A nuXmv Extension for Runtime Verification.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 19th International Conference, 2019

Assumption-Based Runtime Verification with Partial Observability and Resets.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 19th International Conference, 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

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Tightening the contract refinements of a system architecture.

[BibT_eX]

[DOI]

Ramiro Demasi

Formal Methods Syst. Des., 2018

Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems, 2018

Certifying Proofs for LTL Model Checking.

[BibT_eX]

[DOI]

Alberto Griggio

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

Formal Specification and Verification of Dynamic Parametrized Architectures.

[BibT_eX]

[DOI]

Ivan Stojic

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Linear-time Temporal Logic with Event Freezing Functions.

[BibT_eX]

[DOI]

Daniel Ricardo dos Santos

Proceedings of the Proceedings Eighth International Symposium on Games, 2017

From System Specification to Anomaly Detection (and back).

[BibT_eX]

[DOI]

Davide Fauri

Proceedings of the 2017 Workshop on Cyber-Physical Systems Security and PrivaCy, 2017

2016

Infinite-state invariant checking with IC3 and predicate abstraction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Tightening a Contract Refinement.

[BibT_eX]

[DOI]

Ramiro Demasi

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Catalogue of System and Software Properties.

[BibT_eX]

[DOI]

Victor Bos

Harold Bruintjes

Proceedings of the Computer Safety, Reliability, and Security, 2016

Verification of Railway Interlocking - Compositional Approach with OCRA.

[BibT_eX]

[DOI]

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2016

Model-Based Design of an Energy-System Embedded Controller Using Taste.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.

[BibT_eX]

[DOI]

Kristin Yvonne Rozier

Proceedings of the Computer Aided Verification - 28th International Conference, 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

A Lazy Approach to Temporal Epistemic Logic Model Checking.

[BibT_eX]

[DOI]

Marco Gario

Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

2015

Contracts-refinement proof system for component-based embedded systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

Safety assessment of AltaRica models via symbolic model checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

HRELTL: A temporal logic for hybrid systems.

[BibT_eX]

[DOI]

Inf. Comput., 2015

Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 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

Combining MILS with Contract-Based Design for Safety and Security Requirements.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2015

Safely Using the AUTOSAR End-to-End Protection Library.

[BibT_eX]

[DOI]

Thomas Arts

Proceedings of the Computer Safety, Reliability, and Security, 2015

Distributed MILS (D-MILS) Specification, Analysis, Deployment, and Assurance of Distributed Critical Systems.

[BibT_eX]

[DOI]

Harald Rueß

Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems, 2015

Comparing Different Functional Allocations in Automated Air Traffic Control Design.

[BibT_eX]

[DOI]

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

Formal Design and Safety Analysis of AIR6110 Wheel Brake System.

[BibT_eX]

[DOI]

Marco Bozzano

Anthony Fernandes Pires

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

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

Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic.

[BibT_eX]

[DOI]

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

Making Implicit Safety Requirements Explicit - An AUTOSAR Safety Case.

[BibT_eX]

[DOI]

Thomas Arts

Michele Dorigatti

Proceedings of the Computer Safety, Reliability, and Security, 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

Formal Safety Assessment via Contract-Based Design.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Loop summarization using state and transition invariants.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

SMT-based scenario verification for hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

OCRA: A tool for checking the refinement of temporal contracts.

[BibT_eX]

[DOI]

Michele Dorigatti

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 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

A Formal Framework for the Specification, Verification and Synthesis of Diagnosers.

[BibT_eX]

[DOI]

Proceedings of the Late-Breaking Developments in the Field of Artificial Intelligence, 2013

2012

Validation of requirements for hybrid systems: A formal approach.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2012

An abstraction refinement approach combining precise and approximated techniques.

[BibT_eX]

[DOI]

Natasha Sharygina

Aliaksei Tsitovich

Int. J. Softw. Tools Technol. Transf., 2012

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

[BibT_eX]

[DOI]

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

A Property-Based Proof System for Contract-Based Design.

[BibT_eX]

[DOI]

Proceedings of the 38th Euromicro Conference on Software Engineering and Advanced Applications, 2012

SMT-Based Verification of Hybrid Systems.

[BibT_eX]

[DOI]

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

2011

Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking.

[BibT_eX]

[DOI]

Roberto Sebastiani

Moshe Y. Vardi

Int. J. Softw. Tools Technol. Transf., 2011

Formalizing requirements with object models and temporal constraints.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2011

Symbolic Model Checking and Safety Assessment of Altarica models.

[BibT_eX]

[DOI]

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

OthelloPlay: a plug-in based tool for requirement formalization and validation.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Developing Tools as Plug-ins, 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]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

From Sequential Extended Regular Expressions to NFA with Symbolic Labels.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2010

Formalization and validation of a subset of the European Train Control System.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Model Checking of Hybrid Systems Using Shallow Synchronization.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2010

Loopfrog - loop summarization for static analysis.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

2009

Formalization and Validation of Safety-Critical Requirements

[BibT_eX]

[DOI]

Proceedings of the Proceedings FM-09 Workshop on Formal Methods for Aerospace, 2009

An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk.

[BibT_eX]

[DOI]

Natasha Sharygina

Aliaksei Tsitovich

Proceedings of the SAVCBS'09, 2009

The synergy of precise and fast abstractions for program verification.

[BibT_eX]

[DOI]

Natasha Sharygina

Aliaksei Tsitovich

Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Loopfrog: A Static Analyzer for ANSI-C Programs.

[BibT_eX]

[DOI]

Proceedings of the ASE 2009, 2009

Supporting Requirements Validation: The EuRailCheck Tool.

[BibT_eX]

[DOI]

Proceedings of the ASE 2009, 2009

Abstract Model Checking without Computing the Abstraction.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

Requirements Validation for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Symbolic Compilation of PSL.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Object Models with Temporal Constraints.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

From Informal Requirements to Property-Driven Formal Validation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2008

Loop Summarization Using Abstract Transformers.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

GSTE is partitioned model checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

Property-Driven Partitioning for Abstraction Refinement.

[BibT_eX]

[DOI]

Roberto Sebastiani

Moshe Y. Vardi

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

Syntactic Optimizations for PSL Verification.

[BibT_eX]

[DOI]

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

Boolean Abstraction for Temporal Logic Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

A new hybrid approach for efficient LTL model checking.

[BibT_eX]

[DOI]

PhD thesis, 2006

From PSL to NBA: a Modular Symbolic Encoding.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

2003

"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking.

[BibT_eX]

[DOI]

Roberto Sebastiani