activity
20142025
most citedProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems

5 citations · 9 across the 9 of their papers we have counts for

collaborators

9 papers

cs.SE2025

Floating-Point Neural Network Verification at the Software Level

Edoardo Manino, Bruno Farias, Rafael Sá Menezes +2

The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques canno…

cs.SE2024★ 1 cited

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov +3

Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack…

cs.SE2023

ESBMC v7.4: Harnessing the Power of Intervals

Rafael Menezes, Mohannad Aldughaim, Bruno Farias +9

ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported…

cs.SE2023★ 1 cited

NeuroCodeBench: a plain C neural network benchmark for software verification

Edoardo Manino, Rafael Sá Menezes, Fedor Shmarov +1

Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal,…

cs.SE2022

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs

Fatimah K. Aljaafari, Rafael Menezes, Edoardo Manino +3

Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially wit…

eess.SY2019

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

Fedor Shmarov, Sadegh Soudjani, Nicola Paoletti +4

We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochas…

eess.SY2017★ 2 cited

Automated Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems

Fedor Shmarov, Nicola Paoletti, Ezio Bartocci +3

We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread us…

cs.LO2014★ 5 cited

ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems

Fedor Shmarov, Paolo Zuliani

We present ProbReach, a tool for verifying probabilistic reachability for stochastic hybrid systems, i.e., computing the probability that the system reaches an unsafe region of the…

cs.LO2014

Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters

Fedor Shmarov, Paolo Zuliani

We develop an algorithm for computing bounded reachability probability for hybrid systems, i.e., the probability that the system reaches an unsafe region within a finite number of…