Research Area

Formal Methods for Engineering (ForME)

REFERENT

Tiziano Villa

Computer Science Department, University of Verona, Italy

DESCRIPTION

The aim of the research group is to apply formal methods to modelling, verification and synthesis of engineering systems. The domains range from timed systems to nonlinear cyberphysical systems.

View related projects

LINKS

Visit institutional webpage Visit webpage

TOPICS

Formal Verification
Timed Automata
Hybrid Automata
Cyber-Physical Systems
Reachability Analysis
Synthesis
Logics

RELATED PUBLICATIONS

Publication Project & Area

A computable and compositional semantics for hybrid automata.

Davide Bresolin, Pieter Collins, Luca Geretti, Roberto Segala, Tiziano Villa, Sanja Zivanovic Gonzalez

HSCC, Conference and Workshop Papers, 2020

 		None
Formal Methods for Engineering (ForME)

Higher Order Method for Differential Inclusions.

Sanja Zivanovic Gonzalez, Pieter Collins, Luca Geretti, Davide Bresolin, Tiziano Villa

CoRR, Informal Publications, 2020

 		None
Formal Methods for Engineering (ForME)

Automated Verification of Noisy Nonlinear Cyber-Physical Systems with Ariadne.

Davide Bresolin, Luca Geretti, Tiziano Villa

OVERLAY@AI*IA, Conference and Workshop Papers, 2019

 		None
Formal Methods for Engineering (ForME)

Rigorous Continuous Evolution of Uncertain Systems.

Luca Geretti, Sanja Zivanovic Gonzalez, Pieter Collins, Davide Bresolin, Tiziano Villa

NSV@CAV, Conference and Workshop Papers, 2019

 		None
Formal Methods for Engineering (ForME)

Formal Verification of Medical CPS - A Laser Incision Case Study.

Andre A. Geraldes, Luca Geretti, Davide Bresolin, Riccardo Muradore, Paolo Fiorini, Leonardo S. Mattos, Tiziano Villa

ACM Trans. Cyber Phys. Syst., Journal Articles, 2018

 		None
Formal Methods for Engineering (ForME)

Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne.

Luca Geretti, Davide Bresolin, Pieter Collins, Sanja Zivanovic Gonzalez, Tiziano Villa

ICTSS, Conference and Workshop Papers, 2017

 		None
Formal Methods for Engineering (ForME)

Formal verification of robotic surgery tasks by reachability analysis.

Davide Bresolin, Luca Geretti, Riccardo Muradore, Paolo Fiorini, Tiziano Villa

Microprocess. Microsystems, Journal Articles, 2015

 		None
Formal Methods for Engineering (ForME)

A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems.

Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Davide Bresolin, Luca Geretti, Tiziano Villa

Proc. IEEE, Journal Articles, 2015

 		None
Formal Methods for Engineering (ForME)

Verification of Robotic Surgery Tasks by Reachability Analysis - A Comparison of Tools.

Davide Bresolin, Luca Geretti, Riccardo Muradore, Paolo Fiorini, Tiziano Villa

DSD, Conference and Workshop Papers, 2014

 		None
Formal Methods for Engineering (ForME)

Computing the Evolution of Hybrid Systems using Rigorous Function Calculus.

Pieter Collins, Davide Bresolin, Luca Geretti, Tiziano Villa

ADHS, Conference and Workshop Papers, 2012

 		None
Formal Methods for Engineering (ForME)

Open Problems in Verification and Refinement of Autonomous Robotic Systems.

Davide Bresolin, Luigi Di Guglielmo, Luca Geretti, Riccardo Muradore, Paolo Fiorini, Tiziano Villa

DSD, Conference and Workshop Papers, 2012

 		None
Formal Methods for Engineering (ForME)

Ariadne - Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis.

Luca Benvenuti, Davide Bresolin, Pieter Collins, Alberto Ferrari, Luca Geretti, Tiziano Villa

RP, Conference and Workshop Papers, 2012

 		None
Formal Methods for Engineering (ForME)

Cookies disclaimer

Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.