List of works - Ezio Bartocci

A Counting Semantics for Monitoring LTL Specifications over Finite Traces

scientific article published in 2018

A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks

scholarly article published March 2018

A Linear Programming-based Iterative Approach to Stabilizing Polynomial Dynamics

scientific article published in July 2017

A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems

scientific article published on 7 January 2022

A Normative Supervisor for Reinforcement Learning Agents

scientific article published in 2021

A Novel Spatial–Temporal Specification-Based Monitoring System for Smart Cities

scientific article published in August 2021

A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage

scientific article published in 2017

A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems

scientific article published in 2019

A Robust Genetic Algorithm for Learning Temporal Specifications from Data

scientific article published in 2018

A formal methods approach to pattern synthesis in reaction diffusion systems

A survey of challenges for runtime verification from advanced application domains (beyond software)

scientific article published in November 2019

ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans

scientific article published in 2017

Abstraction-Based Parameter Synthesis for Multiaffine Systems

scientific article published in 2015

Adaptive Fault Detection Exploiting Redundancy with Uncertainties in Space and Time

scientific article published in June 2019

Adaptive Testing for Specification Coverage in CPS Models

scientific article published in 2021

Adaptive testing for specification coverage and refinement in CPS models

scientific article published in November 2022

An Algebraic Framework for Runtime Verification

scientific article published in November 2018

An agent-based multilayer architecture for bioinformatics grids

scientific article published on June 2007

Analysis of Bayesian Networks via Prob-Solvable Loops

scientific article published in 2020

Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems

scientific article published in 2020

Automated Termination Analysis of Polynomial Probabilistic Programs

scientific article published in 2021

Automatic Failure Explanation in CPS Models

scientific article published in 2019

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

scientific article published in 2019

BioWMS: a web-based Workflow Management System for bioinformatics

scientific article

Biowep: a workflow enactment portal for bioinformatics applications

scientific article

CPSDebug: Automatic failure explanation in CPS models

scientific article published on 8 January 2021

CPSDebug: a tool for explanation of failures in cyber-physical systems

scientific article published on 18 July 2020

Capacitive Soil Moisture Sensor Node for IoT in Agriculture and Home

scientific article published in June 2019

CellExcite: an efficient simulation environment for excitable cells

scientific article

Computational Modeling, Formal Analysis, and Tools for Systems Biology

scientific article

Computing with Biophysical and Hardware-Efficient Neural Models

scientific article published in 2017

Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics

scientific article published in December 2019

Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software)

scientific article published on 15 November 2019

Curvature analysis of cardiac excitation wavefronts

scientific article published in March 2013

Deductive Controller Synthesis for Probabilistic Hyperproperties

scientific article published in 2023

DeepSTL

scientific article published on 21 May 2022

Detecting synchronisation of biological oscillators by model checking

scientific article published in April 2010

Discrete Abstraction of Multiaffine Systems

scientific article published in 2016

Distribution Estimation for Probabilistic Loops

scientific article published in 2022

Enforcing ethical goals over reinforcement-learning policies

scientific article published on 29 September 2022

Expressionview: visualization of quantitative trait loci and gene-expression data in Ensembl

scientific article

Extending a Hodgkin-Huxley Model for Larval Drosophila Muscle Excitability via Particle Swarm Fitting

scientific article published in 2019

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014 ⬇️

Flavors of Sequential Information Flow

scientific article published in 2022

HyperProb: A Model Checker for Probabilistic Hyperproperties

scientific article published in 2021

Information-flow Interfaces

scientific article published in 2022

International Competition on Runtime Verification (CRV)

scientific article published in 2019

Introducing Asynchronicity to Probabilistic Hyperproperties

scientific article published in 2023

Introduction to Runtime Verification

scientific article published in 2018

Introduction to the special issue on runtime verification

scientific article published on 18 July 2017

Lightweight Verification of Hyperproperties

scientific article published in 2023

Localizing Faults in Simulink/Stateflow Models with STL

scientific article published on 11 April 2018

Mining Hyperproperties using Temporal Logics

scientific article published on 9 September 2023

Mining Shape Expressions From Positive Examples

scientific article published in November 2020

Mining Shape Expressions with ShapeIt

scientific article published in 2021

Mining Specification Parameters for Multi-class Classification

scientific article published in 2023

Model Checking Biological Oscillators

scientific article published in February 2009

Model checking hyperproperties for Markov decision processes

scientific article published in November 2022

Modeling and Analysis of Cardiac Hybrid Cellular Automata via GPU-Accelerated Monte Carlo Simulation

scientific article published on 14 January 2021

Modeling the cell cycle: from deterministic models to hybrid systems.

scientific article published on 29 March 2011

Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments

scientific article published in 2022

Moment-based analysis of Bayesian network properties

scientific article published in February 2022

Monitoring Spatio-Temporal Properties (Invited Tutorial)

scientific article published in 2020

Monitoring mobile and spatially distributed cyber-physical systems

scientific article published on 29 September 2017

Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial)

scientific article published in 2018

MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties

scientific article published in 2020

Mora - Automatic Generation of Moment-Based Invariants

scientific article published in 2020

Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications

scientific article published on 14 December 2021

On Normative Reinforcement Learning via Safe Reinforcement Learning

scientific article published on 12 November 2022

Online monitoring of spatio-temporal properties for imprecise signals

scientific article published on 20 November 2021

Parallel reachability analysis for hybrid systems ⬇️

scientific article published in November 2016

Parallel reachability analysis of hybrid systems in XSpeed

scientific article published on 19 February 2018

Parameter Synthesis for Probabilistic Hyperproperties

Parameter-Independent Strategies for pMDPs via POMDPs

scientific article published in 2018

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty

scientific article published in 2019

Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems

scientific article published on 22 September 2021

Predictive monitoring with uncertainty for deep learning enabled smart cities

scientific article published on 16 November 2020

Preface of the special issue on Model Checking of Software ⬇️

Scientific article

Probabilistic Hyperproperties with Nondeterminism

scientific article published in 2020

Probabilistic Hyperproperties with Rewards

scientific article published in 2022

Progression for Monitoring in Temporal ASP

scientific article published on 28 September 2023

Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties

scientific article published in 2023

Quantitative Regular Expressions for Arrhythmia Detection

scientific article published on 10 December 2018

Quantitative monitoring of STL with edit distance

scientific article published on 27 March 2018

RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction)

scientific article published in 2018

Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes

scientific article published in 2018

Runtime Verification of Autonomous Driving Systems in CARLA

scientific article published in 2020

SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities

scientific article published in April 2020

Signal Convolution Logic

scientific article published in 2018

Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications

scientific article published in 2018

Survey on mining signal temporal logic specifications

scientific article published in November 2022

TOOLympics 2019: An Overview of Competitions in Formal Methods

scientific article published in 2019

Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics.

scientific article

The Probabilistic Termination Tool Amber

scientific article published in 2021

The probabilistic termination tool amber

scientific article published in 2022

This is the moment for probabilistic loops

scientific article published on 31 October 2022

UBioLab: a web-laboratory for ubiquitous in-silico experiments

scientific article

Verifying nonlinear analog and mixed-signal circuits with inputs

scientific article published in 2018

XSpeed: Accelerating Reachability Analysis on Multi-core Processors

scientific article published in 2015

List of works by Ezio Bartocci

A Counting Semantics for Monitoring LTL Specifications over Finite Traces

A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks

A Linear Programming-based Iterative Approach to Stabilizing Polynomial Dynamics

A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems

A Normative Supervisor for Reinforcement Learning Agents

A Novel Spatial–Temporal Specification-Based Monitoring System for Smart Cities

A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage

A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems

A Robust Genetic Algorithm for Learning Temporal Specifications from Data

A formal methods approach to pattern synthesis in reaction diffusion systems

A survey of challenges for runtime verification from advanced application domains (beyond software)

ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans

Abstraction-Based Parameter Synthesis for Multiaffine Systems

Adaptive Fault Detection Exploiting Redundancy with Uncertainties in Space and Time

Adaptive Testing for Specification Coverage in CPS Models

Adaptive testing for specification coverage and refinement in CPS models

An Algebraic Framework for Runtime Verification

An agent-based multilayer architecture for bioinformatics grids

Analysis of Bayesian Networks via Prob-Solvable Loops

Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems

Automated Termination Analysis of Polynomial Probabilistic Programs

Automatic Failure Explanation in CPS Models

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

BioWMS: a web-based Workflow Management System for bioinformatics

Biowep: a workflow enactment portal for bioinformatics applications

CPSDebug: Automatic failure explanation in CPS models

CPSDebug: a tool for explanation of failures in cyber-physical systems

Capacitive Soil Moisture Sensor Node for IoT in Agriculture and Home

CellExcite: an efficient simulation environment for excitable cells

Computational Modeling, Formal Analysis, and Tools for Systems Biology

Computing with Biophysical and Hardware-Efficient Neural Models

Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics

Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software)

Curvature analysis of cardiac excitation wavefronts

Deductive Controller Synthesis for Probabilistic Hyperproperties

DeepSTL

Detecting synchronisation of biological oscillators by model checking

Discrete Abstraction of Multiaffine Systems

Distribution Estimation for Probabilistic Loops

Enforcing ethical goals over reinforcement-learning policies

Expressionview: visualization of quantitative trait loci and gene-expression data in Ensembl

Extending a Hodgkin-Huxley Model for Larval Drosophila Muscle Excitability via Particle Swarm Fitting

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014 ⬇️

Flavors of Sequential Information Flow

HyperProb: A Model Checker for Probabilistic Hyperproperties

Information-flow Interfaces

International Competition on Runtime Verification (CRV)

Introducing Asynchronicity to Probabilistic Hyperproperties

Introduction to Runtime Verification

Introduction to the special issue on runtime verification

Lightweight Verification of Hyperproperties

Localizing Faults in Simulink/Stateflow Models with STL

Mining Hyperproperties using Temporal Logics

Mining Shape Expressions From Positive Examples

Mining Shape Expressions with ShapeIt

Mining Specification Parameters for Multi-class Classification

Model Checking Biological Oscillators

Model checking hyperproperties for Markov decision processes

Modeling and Analysis of Cardiac Hybrid Cellular Automata via GPU-Accelerated Monte Carlo Simulation

Modeling the cell cycle: from deterministic models to hybrid systems.

Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments

Moment-based analysis of Bayesian network properties

Monitoring Spatio-Temporal Properties (Invited Tutorial)

Monitoring mobile and spatially distributed cyber-physical systems

Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial)

MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties

Mora - Automatic Generation of Moment-Based Invariants

Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications

On Normative Reinforcement Learning via Safe Reinforcement Learning

Online monitoring of spatio-temporal properties for imprecise signals

Parallel reachability analysis for hybrid systems ⬇️

Parallel reachability analysis of hybrid systems in XSpeed

Parameter Synthesis for Probabilistic Hyperproperties

Parameter-Independent Strategies for pMDPs via POMDPs

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty

Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems

Predictive monitoring with uncertainty for deep learning enabled smart cities

Preface of the special issue on Model Checking of Software ⬇️

Probabilistic Hyperproperties with Nondeterminism