130 citations · 267 across the 16 of their papers we have counts for
16 papers
Verification of Quantum Systems using Barrier Certificates
Marco Lewis, Paolo Zuliani, Sadegh Soudjani
Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification…
Matrix Representation of Arbitrarily Controlled Quantum Gates
Marco Lewis, Sadegh Soudjani, Paolo Zuliani
Controlled operations allow for the entanglement of quantum registers. In particular, a controlled- gate allows an operation, , to be applied to the target register and entan…
Quantum Computer Benchmarking via Quantum Algorithms
Konstantinos Georgopoulos, Clive Emary, Paolo Zuliani
We present a framework that utilizes quantum algorithms, an architecture aware quantum noise model and an ideal simulator to benchmark quantum computers. The benchmark metrics high…
Formal Verification of Quantum Programs: Theory, Tools and Challenges
Marco Lewis, Sadegh Soudjani, Paolo Zuliani
Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backe…
Modelling and Simulating the Noisy Behaviour of Near-term Quantum Computers
Konstantinos Georgopoulos, Clive Emary, Paolo Zuliani
Noise dominates every aspect of near-term quantum computers, rendering it exceedingly difficult to carry out even small computations. In this paper we are concerned with the modell…
A Comparison of Quantum Walk Implementations on NISQ Computers
Konstantinos Georgopoulos, Clive Emary, Paolo Zuliani
This paper explores two circuit approaches for quantum walks: the first consists of generalised controlled inversions, whereas the second one effectively replaces them with rotatio…
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…
Full version: An evaluation of estimation techniques for probabilistic reachability
Mariia Vasileva, Paolo Zuliani
We evaluate numerically-precise Monte Carlo (MC), Quasi-Monte Carlo (QMC) and Randomised Quasi-Monte Carlo (RQMC) methods for computing probabilistic reachability in hybrid systems…
Verifying Quantum Programs: From Quipper to QPMC
Linda Anticoli, Carla Piazza, Leonardo Taglialegne +1
In this paper we present a translation from the quantum programming language Quipper to the QPMC model checker, with the main aim of verifying Quipper programs. Quipper is an embed…
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…
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…
Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis
Bing Liu, Soonho Kong, Sicun Gao +2
Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computat…
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions
Bing Liu, Soonho Kong, Sicun Gao +2
A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (\eg, time series). In this paper we focus o…
Statistical Model Checking for Biological Applications
Paolo Zuliani
In this paper we survey recent work on the use of statistical model checking techniques for biological applications. We begin with an overview of the basic modelling techniques for…
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…
SReach: A Bounded Model Checker for Stochastic Hybrid Systems
Qinsi Wang, Paolo Zuliani, Soonho Kong +2
In this paper we describe a new tool, SReach, which solves probabilistic bounded reachability problems for two classes of stochastic hybrid systems. The first one is (nonlinear) hy…