Stefano Tonetta

Orcid: 0000-0001-9091-7899

According to our database1, Stefano Tonetta authored at least 114 papers between 2003 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
A first-order logic characterization of safety and co-safety languages.
Log. Methods Comput. Sci., 2023

GR(1) is equivalent to R(1).
Inf. Process. Lett., 2023

Asynchronous Composition of LTL Properties over Infinite and Finite Traces.
CoRR, 2023

Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems.
Proceedings of the Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems, 2023

EVA: a Tool for the Compositional Verification of AUTOSAR Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Reasoning with Metric Temporal Logic and Resettable Skewed Clocks.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023

Symbolic Model Checking of Relative Safety LTL Properties.
Proceedings of the iFM 2023 - 18th International Conference, 2023

Two formal methodologies of Model-Based Safety Assessment for Fault Tree Analysis.
Proceedings of the 7th International Conference on System Reliability and Safety, 2023

SMT-Based Stability Verification of an Industrial Switched PI Control Systems.
Proceedings of the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2023

Metric Temporal Logic with Resettable Skewed Clocks.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2023

Set-Based Invariants over Polynomial Systems.
Proceedings of the 38th Italian Conference on Computational Logic, 2023

2022
Assumption-based Runtime Verification.
Formal Methods Syst. Des., April, 2022

Verification modulo theories.
Formal Methods Syst. Des., 2022

Diagnosability of fair transition systems.
Artif. Intell., 2022

Searching for Ribbon-Shaped Paths in Fair Transition Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

The VMT-LIB Language and Tools.
Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Asynchronous Composition of Local Interface LTL Properties.
Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

A comprehensive framework for the analysis of automotive systems.
Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, 2022

COMPASTA: Extending TASTE with Formal Design and Verification Functionality.
Proceedings of the Model-Based Safety and Assessment - 8th International Symposium, 2022

A first-order logic characterisation of safety and co-safety languages.
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.
Microprocess. Microsystems, November, 2021

Certifying proofs for SAT-based model checking.
Formal Methods Syst. Des., 2021

Expressiveness of Extended Bounded Response LTL.
Proceedings of the Proceedings 12th International Symposium on Games, 2021

Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis.
Proceedings of the Software Engineering and Formal Methods - 19th International Conference, 2021

Assumption-Based Runtime Verification of Infinite-State Systems.
Proceedings of the Runtime Verification - 21st International Conference, 2021

Assumptions and Guarantees for Composable Models in Papyrus for Robotics.
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.
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.
Proceedings of the Quality of Information and Communications Technology, 2021

Model-based Analysis Support for Dependable Complex Systems in CHESS.
Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development, 2021

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.
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.
Inf. Comput., 2020

Safe Decomposition of Startup Requirements: Verification and Synthesis.
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.
Proceedings of the Simulation and Modeling Methodologies, Technologies and Applications, 2020

A Cloud-based Collaboration Platform for Model-based Design of Cyber-Physical Systems.
Proceedings of the 10th International Conference on Simulation and Modeling Methodologies, 2020

Model-Based Safety Analysis of Mode Transitions.
Proceedings of the Computer Safety, Reliability, and Security, 2020

Reactive Synthesis from Extended Bounded Response LTL Specifications.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

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

NuRV: A nuXmv Extension for Runtime Verification.
Proceedings of the Runtime Verification - 19th International Conference, 2019

Assumption-Based Runtime Verification with Partial Observability and Resets.
Proceedings of the Runtime Verification - 19th International Conference, 2019

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
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.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Tightening the contract refinements of a system architecture.
Formal Methods Syst. Des., 2018

Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides.
Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems, 2018

Certifying Proofs for LTL Model Checking.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Formal Specification and Verification of Dynamic Parametrized Architectures.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017
Linear-time Temporal Logic with Event Freezing Functions.
Proceedings of the Proceedings Eighth International Symposium on Games, 2017

From System Specification to Anomaly Detection (and back).
Proceedings of the 2017 Workshop on Cyber-Physical Systems Security and PrivaCy, 2017

2016
Infinite-state invariant checking with IC3 and predicate abstraction.
Formal Methods Syst. Des., 2016

Tightening a Contract Refinement.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Catalogue of System and Software Properties.
Proceedings of the Computer Safety, Reliability, and Security, 2016

Verification of Railway Interlocking - Compositional Approach with OCRA.
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.
Proceedings of the FM 2016: Formal Methods, 2016

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

A Lazy Approach to Temporal Epistemic Logic Model Checking.
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

2015
Contracts-refinement proof system for component-based embedded systems.
Sci. Comput. Program., 2015

Safety assessment of AltaRica models via symbolic model checking.
Sci. Comput. Program., 2015

HRELTL: A temporal logic for hybrid systems.
Inf. Comput., 2015

Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic.
Log. Methods Comput. Sci., 2015

HyComp: An SMT-Based Model Checker for Hybrid Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Parameter Synthesis with IC3 (Informal Presentation).
Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Combining MILS with Contract-Based Design for Safety and Security Requirements.
Proceedings of the Computer Safety, Reliability, and Security, 2015

Safely Using the AUTOSAR End-to-End Protection Library.
Proceedings of the Computer Safety, Reliability, and Security, 2015

Distributed MILS (D-MILS) Specification, Analysis, Deployment, and Assurance of Distributed Critical Systems.
Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems, 2015

Comparing Different Functional Allocations in Automated Air Traffic Control Design.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Formal Design and Safety Analysis of AIR6110 Wheel Brake System.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Quantifier-free encoding of invariants for hybrid systems.
Formal Methods Syst. Des., 2014

IC3 Modulo Theories via Implicit Predicate Abstraction.
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.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Making Implicit Safety Requirements Explicit - An AUTOSAR Safety Case.
Proceedings of the Computer Safety, Reliability, and Security, 2014

Verifying LTL Properties of Hybrid Systems with K-Liveness.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

The nuXmv Symbolic Model Checker.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Formal Safety Assessment via Contract-Based Design.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
Loop summarization using state and transition invariants.
Formal Methods Syst. Des., 2013

SMT-based scenario verification for hybrid systems.
Formal Methods Syst. Des., 2013

OCRA: A tool for checking the refinement of temporal contracts.
Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Parameter synthesis with IC3.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Time-aware relational abstractions for hybrid systems.
Proceedings of the International Conference on Embedded Software, 2013

A Formal Framework for the Specification, Verification and Synthesis of Diagnosers.
Proceedings of the Late-Breaking Developments in the Field of Artificial Intelligence, 2013

2012
Validation of requirements for hybrid systems: A formal approach.
ACM Trans. Softw. Eng. Methodol., 2012

An abstraction refinement approach combining precise and approximated techniques.
Int. J. Softw. Tools Technol. Transf., 2012

A quantifier-free SMT encoding of non-linear hybrid automata.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

A Property-Based Proof System for Contract-Based Design.
Proceedings of the 38th Euromicro Conference on Software Engineering and Advanced Applications, 2012

SMT-Based Verification of Hybrid Systems.
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

2011
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking.
Int. J. Softw. Tools Technol. Transf., 2011

Formalizing requirements with object models and temporal constraints.
Softw. Syst. Model., 2011

Symbolic Model Checking and Safety Assessment of Altarica models.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

OthelloPlay: a plug-in based tool for requirement formalization and validation.
Proceedings of the 1st Workshop on Developing Tools as Plug-ins, 2011

Proving and explaining the unfeasibility of message sequence charts for hybrid systems.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction.
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.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
From Sequential Extended Regular Expressions to NFA with Symbolic Labels.
Proceedings of the Implementation and Application of Automata, 2010

Formalization and validation of a subset of the European Train Control System.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Model Checking of Hybrid Systems Using Shallow Synchronization.
Proceedings of the Formal Techniques for Distributed Systems, 2010

Loopfrog - loop summarization for static analysis.
Proceedings of the Second International Workshop on Invariant Generation, 2010

2009
Formalization and Validation of Safety-Critical Requirements
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.
Proceedings of the SAVCBS'09, 2009

The synergy of precise and fast abstractions for program verification.
Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Loopfrog: A Static Analyzer for ANSI-C Programs.
Proceedings of the ASE 2009, 2009

Supporting Requirements Validation: The EuRailCheck Tool.
Proceedings of the ASE 2009, 2009

Abstract Model Checking without Computing the Abstraction.
Proceedings of the FM 2009: Formal Methods, 2009

Requirements Validation for Hybrid Systems.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Symbolic Compilation of PSL.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Object Models with Temporal Constraints.
Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

From Informal Requirements to Property-Driven Formal Validation.
Proceedings of the Formal Methods for Industrial Critical Systems, 2008

Loop Summarization Using Abstract Transformers.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
GSTE is partitioned model checking.
Formal Methods Syst. Des., 2007

Property-Driven Partitioning for Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Syntactic Optimizations for PSL Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Boolean Abstraction for Temporal Logic Satisfiability.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
A new hybrid approach for efficient LTL model checking.
PhD thesis, 2006

From PSL to NBA: a Modular Symbolic Encoding.
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.
Proceedings of the Correct Hardware Design and Verification Methods, 2003


  Loading...