Pith. sign in

REVIEW 2 major objections 3 minor 39 references

Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach

T0 review · 2 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper establishes that sampling-based linear programming can synthesize formally verified barrier certificates for quantum circuits, covering uncertain initial states and gate noise over finite or infinite horizons.

desk verdict Solid sampling+SMT pipeline for small circuits, but the Grover case study overclaims: the 2D abstraction is unproved and the reported parameters violate the definition. read the letter →

arxiv 2506.07635 v2 pith:FUFC4EXE submitted 2025-06-09 cs.LO quant-ph

Siwei Hu , Victor Lopata , Sadegh Soudjani , Paolo Zuliani This is my paper
classification cs.LOquant-ph
keywords quantumcircuitverificationbarriercertificatesscenario-basedoptimizationSMTformalGrover'salgorithmuncertaindynamicsk-inductive
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that a formal safety proof for a quantum circuit can be produced by sampling a finite number of states, solving a linear program for the coefficients of a barrier-certificate template, and then checking the resulting candidate against the full state space with an SMT solver. If the check passes, the circuit is certified never to move from any of the specified initial states into any undesired state, even when the initial states and gate rotations are uncertain and the time horizon is unbounded. The authors demonstrate the approach on several small circuits and on Grover's search with an uncertain number of solutions and rotation noise, for both finite and infinite horizons. The payoff for a user is a machine-checkable certificate that covers infinitely many states without exhaustive simulation.

What carries the argument

The load-bearing object is the barrier-certificate template $B(\alpha,z)$: a parameterized real-valued function, usually a polynomial of bounded degree in the complex amplitudes, whose defining conditions become a linear program once states are sampled from the initial, unsafe, and full state regions. The second component is the verification step: the candidate returned by the linear program is checked with an SMT solver against the original universally quantified constraints, so the final certificate is not just a statistical statement about samples. For Grover's algorithm the machinery is a geometric reduction: the $n$-qubit search dynamics is confined to the two-dimensional subspace spanned by the uniform non-solution state $|\alpha\rangle$ and the solution state $|\beta\rangle$, the Grover operator becomes a rotation by angle $\theta$, and the certificate template is simply $B(c,\varphi)=c\cdot\varphi$ with $\varphi$ the polar angle of the state.

What would settle it

Run the exact n-qubit Grover circuit for the certified parameter choices (for example, 5 qubits, M=8, err=0.5, and η=0.3 with horizon T=2), sampling many initial states and noise values from the certified ranges, and check by state-vector simulation whether any exact trajectory reaches the unsafe angle interval within the horizon. A single such counterexample would show either that the two-dimensional reduction is not exact or that the SMT check was unsound.

Watch

Extended reading notes

Core claim

The central discovery is that barrier certificates for quantum circuits do not have to be constructed by hand or by solving a hard robust-optimization problem: a candidate can be synthesized from finitely many sampled complex states as the solution of a linear program, then promoted to a genuine proof by an SMT check of the universal constraints. The certificate is a real-valued function $B$ on the complex state space satisfying $B \leq 0$ on the initial set, $B > 0$ on the unsafe set, and a decrement condition along the circuit dynamics, with relaxed $k$-inductive and finite-horizon variants for harder cases. For complex polynomial templates the imaginary part is discarded, turning the sampled constraints into real linear inequalities. The case studies include verified certificates for the Z, T, CX, CZ, SWAP and Hadamard circuits, and for Grover's search under uncertainty in the number of solutions and the rotation angle after reducing the dynamics to a two-dimensional rotation.

Load-bearing premise

The load-bearing premise is that the circuit model used in the constraints—for Grover, the two-angle rotation—matches the true circuit exactly for every allowed uncertainty, so that a certificate for the model is a certificate for the real circuit.

Editorial extensions

If this is right

  • A verified barrier certificate is a formal proof of non-reachability; no simulation or testing of individual runs is needed to trust the safety claim for the specified initial and unsafe sets.
  • Uncertain initial states and uncertain gate parameters can be folded into the sampled constraints, so certificates can cover whole families of circuits rather than a single nominal circuit.
  • Finite-horizon certificates can certify algorithms like Grover with a bounded number of iterations, where an invariant barrier that must hold forever would be too strict.
  • If no certificate is found, the method only reports that the chosen template failed on the samples; it does not imply the circuit is unsafe, so a user must change the template or sampler rather than declare failure.
  • The approach currently scales exponentially with qubit count because sampling density and SMT verification cost grow with the dimension of the state space, so the demonstrated cases are small circuits.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: if the sampling-and-LP pipeline is the bottleneck, then exploiting low-dimensional invariant subspaces of the sort used for Grover may be the main route to scaling, and other algorithms with known symmetry reductions are natural next targets.
  • Inference: the paper leaves open whether every safe quantum circuit admits a barrier certificate; if that necessity question is answered affirmatively, the two-phase synthesize-then-check scheme would become a complete verification method rather than a sufficient one.
  • Inference: a direct experimental check of the Grover reduction would be to run the exact state-vector circuit for the certified parameters and compare reachable angles with the angle-interval certificate; disagreement would localize the failure to the reduction rather than to the certificate search.
  • Inference: the same sampling, linear-programming, and SMT-check recipe could be applied to time-dependent classical systems and to hybrid quantum-classical circuits, provided the dynamics are given as computable unitary or superoperator maps.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 3 minor

Summary. The paper proposes a scenario-based synthesis method for barrier certificates for discrete-time quantum circuit models. Given a parametrized certificate template, the method samples states from the initial, unsafe, and full state sets, solves a linear program to fit the template parameters, and then uses an SMT solver to verify the candidate against the universally quantified barrier-certificate conditions. The framework covers invariant, k-inductive, time-varying k-inductive, and finite-horizon certificates. Experiments are reported for several small circuits (Z, CNOT, T, CZ, Hadamard, X, SWAP, alternating CX/CZ), and for Grover's algorithm using a two-dimensional angle abstraction with uncertainty in the number of solutions and in the rotation angle.

Significance. If the method works as claimed, it provides a practical, machine-checkable route to safety verification of small quantum circuits under initial-state and dynamics uncertainty, combining sampling-based optimization with SMT validation. The non-Grover case studies are supported by the final SMT checks over the original state space, and the implementation is publicly available, which aids reproducibility. However, the Grover case studies currently do not support the paper's central claim: the abstraction from the n-qubit circuit to the two-dimensional rotation model is unproved, and the reported finite-horizon parameters violate Definition 5. The central methodology is sound in principle, but these issues are load-bearing for a major advertised application.

major comments (2)
  1. [Section VI-B3 and Section VI-C] The Grover* certificates in Table III are synthesized and SMT-checked only over the two-dimensional manifold z(φ)=cosφ|α⟩+sinφ|β⟩ with φ∈[0,2π], while the specification in Section VI-C is stated for the full n-qubit state space. The paper never establishes that this manifold is a sound or conservative abstraction of the original uncertain dynamics and of the sets Z0={z: 2^{-n}-err≤|z_j|²≤2^{-n}+err, |Im z_j|≤√err} and Zu={z: |z_p|²≥0.9}. This matters because Z0 contains states outside span{|α⟩,|β⟩}, and Zu cannot be represented on the manifold: for K=32 and M=8, any state on the manifold has probability cos²φ/(K-M)≤1/24≈0.042 for a fixed non-solution state p, which never reaches 0.9. The abstract unsafe set [3π/2,11π/6] therefore corresponds to a different property. An SMT check over φ does not imply safety of the original circuit; a sound abstraction relation or direct verification over the original state space is required.
  2. [Section VI-B3, Definition 5] The reported finite-horizon certificate for n=5, M=8 with γ=11.49015, λ=28.58842, δ=100, T=2 does not satisfy the defining inequality γ+δ·T<λ, since 11.49015+200=211.49015 is not less than 28.58842. The certificate is therefore not a valid barrier certificate according to Definition 5, and the safety conclusion for that case does not follow from Theorem 1. The numbers also appear internally inconsistent: for B(c,z(φ))=21.22065φ, the maximum one-step increase on Z0 is c·(θ+η)≈28.59, so δ should be at most ≈28.59, while the minimum of B on Zu is ≈100.0, so λ should be at least ≈100.0 for the condition γ+δ·T<λ to hold. The authors should correct the reported parameters and re-run the SMT verification.
minor comments (3)
  1. [Section VI-B1] The displayed certificate B(z)=-9.99934 z0 z0 + 12.99994 should use |z0|² (or ̅z0 z0); as printed, z0z0 is ambiguous. With the reported γ=4, evaluating the displayed expression at |z0|²=0.9 gives about 4.0005, which exceeds γ; the rounded coefficients should be reconciled with the SMT-verified values.
  2. [Section V-C] The Sobol-sequence sampling description is inconsistent: it first decomposes z_j=x_j+iy_j into real variables, then describes constructing a probability vector and assigning independent phases θ_j∈[0,2π). Please clarify the exact dimension and algorithm used to map Sobol points to normalized quantum states.
  3. [Section VI-B3] The constraint derivation contains typographical errors: 'B(c, G(z(ϕ)) − B(c, z(ϕ)) = c·(ϕ+eθ) − c·ϕ' has a missing parenthesis and an undefined symbol eθ; it should state the one-step increment as c·(θ+μ), where μ is the rotation noise. The worst-case condition c·(θ+η)≤δ should be written explicitly as the constraint used in the linear program.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the safety conclusion is produced by independent SMT verification of universal constraints, not by the sample fit; flagged Grover* inconsistencies are correctness risks, not circular reductions.

full rationale

The derivation chain is not circular. Candidates are found by solving the sample-based LP (2), but Algorithm 1 (lines 10-12) and Section V require an independent Z3 check of the universally quantified constraints before any certificate is returned: 'Checking whether a function is an actual barrier certificate can be done automatically by SMT solvers' and 'A candidate barrier certificate that satisfies (2) might just as well satisfy the stricter problem (1), thereby formally showing that our system is safe (over the entire space, not just for the sampled scenarios).' The safety verdict is therefore produced by the SMT check over the full state space, not by the fitted parameters; no fitted quantity is renamed as a prediction. The Grover* template B(c, z(phi)) = c*phi (Eq. 3, Sec. VI-B3) is an ansatz, but it is motivated by the well-known 2-D rotation structure cited to the external survey [33] and is then verified a posteriori, so no ansatz is smuggled in via citation. Self-citations are present — Definition 6 and Theorem 2 are imported from the authors' own [20] (Lewis, Soudjani, Zuliani) — but they serve as stated lemmas with proofs given in the cited prior work, not as uniqueness theorems forcing the experimental outcome; the finite-horizon definition used for the main experiments is the external [25] and the scenario program is the external [11], so the central framework is independently anchored. The Z-gate and alternating CX/CZ certificates of Sec. VI-B satisfy their stated definitions (e.g., gamma + delta*T = 4 < 5 = lambda for the Z gate; d = 4.7079 > k*(epsilon+gamma) = 0.04 for CX/CZ), so the core demonstrations are internally valid. Two Grover* defects are flagged as correctness risks, explicitly distinguished from circularity. (i) The reported certificate 'B(z(phi)) = 21.22065 * phi, with constraint parameters gamma = 11.49015, lambda = 28.58842, delta = 100 and time horizon T = 2' (Sec. VI-B3) violates Definition 5, which requires gamma + delta*T < lambda: 11.49015 + 200 is not less than 28.58842; if delta and lambda were swapped (delta = 28.59, lambda = 100) the inequality would hold, so this appears to be a parameter-swap reporting error rather than an engineered reduction. (ii) The reduction of the n-qubit Grover circuit to the manifold z(phi) = cos(phi)|alpha> + sin(phi)|beta> replaces the original Z0/Zu described in Sec.

Assumptions & free parameters 5 free parameters · 4 assumptions · 0 invented entities

The central claim is an algorithmic capability, not a physical law. The main hand-chosen inputs are template degree, sample counts, and relaxation parameters; the certificate coefficients are LP outputs, not fitted scientific constants. The axioms are the soundness of barrier certificates, the modeling of circuits as discrete-time complex systems, the 2D reduction for Grover, and solver soundness.

free parameters (5)
  • sample count N per region = 500 to 50000 across experiments
    Chosen by hand; larger N gives better candidate coverage but more LP constraints.
  • polynomial degree = 2 or 4 in experiments
    Template expressiveness and complexity tradeoff; no automatic selection.
  • k in k-inductive certificates = k=2 in alternating CX/CZ case
    Relaxation parameter chosen by the user.
  • Grover template coefficient c and certificate parameters = c=21.22065, gamma=11.49015, lambda=28.58842, delta=100, T=2
    LP solution over sampled angles; the reported values appear inconsistent with Definition 5 because gamma + delta*T = 211.49 is not less than lambda = 28.588.
  • uncertainty bounds err and eta = err=0.5, eta=0.3 for 5-qubit Grover
    User-specified perturbation magnitudes defining Z0 and the noisy rotation angle.
assumptions (4)
  • standard math Barrier certificate conditions (Definitions 3, 4, 5, Theorem 2) are sound: satisfaction implies safety.
    Taken from Prajna and Jadbabaie, Anand et al., Nejati et al., and Lewis et al.; the paper does not reprove them.
  • domain assumption A quantum circuit can be modeled as a discrete-time complex-space system with unitary or set-valued transition maps.
    Section IV-A establishes this modeling bridge that lets barrier certificates apply to quantum circuits.
  • domain assumption For Grover's algorithm, the state remains in the two-dimensional subspace spanned by |alpha> and |beta>, and the Grover operator acts as a rotation by angle theta.
    Section VI-B3; standard result cited as Aharonov, used to justify the reduced template B(c, phi) = c * phi.
  • domain assumption The LP solver HiGHS and the SMT solver Z3 are sound for the formulas they decide.
    Tooling assumption; if Z3's encoding of the complex polynomial constraints over the quantum state sphere is incorrect, the verification step is unsound.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach." pith.science (2026). https://pith.science/paper/FUFC4EXE

@misc{pith2026250607635,
  author       = {Pith},
  title        = {Pith review of: Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FUFC4EXE}},
  note         = {Machine review of arXiv:2506.07635}
}
read the original abstract

In recent years, various techniques have been explored for the verification of quantum circuits, including the use of barrier certificates, mathematical tools capable of demonstrating the correctness of such systems. These certificates ensure that, starting from initial states and applying the system's dynamics, the system will never reach undesired states. In this paper, we propose a methodology for synthesizing such certificates for quantum circuits using a scenario-based approach, for both finite and infinite time horizons. In addition, our approach can handle uncertainty in the initial states and in the system's dynamics. We present several case studies on quantum circuits, comparing the performance of different types of barrier certificate and analyzing which one is most suitable for each case.

Figures

Figures reproduced from arXiv: 2506.07635 by the authors.

Figure 1
Figure 1. An infinite-depth quantum circuit alternating unitaries [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Quantum circuit of three qubits. to negate the formula, resulting in ∃z ¬ϕ(z), which the solver can process. For example, the constraint B(z) ≤ 0, ∀z ∈ Z0 is encoded in ∃z B(z) > 0. (The other two types of barrier certificate constraint follow easily.) If ∃z ¬ϕ(z) is false (¬ϕ(z) unsatisfiable), then ϕ(z) is true for every z. However, if it is true (satisfiable), then there exists a counterexample where ϕ is not tru… view at source ↗
Figure 3
Figure 3. Quantum circuit of two qubits. |001⟩ exceeds 0.2. In particular, we specify as the initial and unsafe region the following sets: Z0 = {z ∈ C 8 : |z0| 2 ≥ 0.9}, and Zu = {z ∈ C 8 : |z1| 2 ≥ 0.2}. Note that the system with respect to Z0 and Zu is deliberately correct, as applying the Z gate will only flip the phase of the |1⟩ states. By running our algorithm with an input of 20000 samples per region and a maximum degr… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Representation of Grover’s operator in a two-dimensional plane. The [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

39 extracted references · 35 canonical work pages

  1. [1]

    Quantum error correction below the surface code threshold,

    Google Quantum AI and Collaborators, “Quantum error correction below the surface code threshold,” Nature, vol. 638, no. 8052, pp. 920– 926, Feb 2025

    work page 2025

  2. [2]

    Hardware-efficient quantum error correction via concatenated bosonic qubits,

    H. Putterman, K. Noh, C. T. Hann et al., “Hardware-efficient quantum error correction via concatenated bosonic qubits,” Nature, vol. 638, no. 8052, pp. 927–934, Feb 2025

    work page 2025

  3. [3]

    Fault-tolerant quantum computation by anyons,

    A. Kitaev, “Fault-tolerant quantum computation by anyons,” Annals of Physics, vol. 303, no. 1, pp. 2–30, 2003

    work page 2003

  4. [4]

    Interferometric single-shot parity measure- ment in InAs–Al hybrid devices,

    Microsoft Azure Quantum, “Interferometric single-shot parity measure- ment in InAs–Al hybrid devices,” Nature, vol. 638, no. 8051, pp. 651– 655, Feb 2025

    work page 2025

  5. [5]

    Quantum Computing in the NISQ era and beyond,

    J. Preskill, “Quantum Computing in the NISQ era and beyond,” Quan- tum, vol. 2, p. 79, Aug. 2018

    2018

  6. [6]

    Beyond NISQ: The Megaquop Machine,

    ——, “Beyond NISQ: The Megaquop Machine,” 2025. [Online]. Available: https://arxiv.org/abs/2502.17368

    arXiv 2025

  7. [7]

    Simulating physics with computers,

    R. P. Feynman, “Simulating physics with computers,” International Journal of Theoretical Physics , vol. 21, no. 6, pp. 467–488, Jun 1982

    1982

  8. [8]

    Improved simulation of stabilizer circuits,

    S. Aaronson and D. Gottesman, “Improved simulation of stabilizer circuits,” Phys. Rev. A, vol. 70, p. 052328, 2004

    work page 2004

Show all 39 references
  1. [9]

    Safety verification of hybrid systems using barrier certificates,

    S. Prajna and A. Jadbabaie, “Safety verification of hybrid systems using barrier certificates,” in Hybrid Systems: Computation and Control, R. Alur and G. J. Pappas, Eds. Springer, 2004, pp. 477–492

    2004

  2. [10]

    Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems,

    R. Alur, C. Courcoubetis, T. A. Henzinger, and P. H. Ho, “Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems,” in Hybrid Systems , R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, Eds. Springer, 1993, pp. 209–229

    1993

  3. [11]

    A scenario approach for syn- thesizing k-inductive barrier certificates,

    V . Murali, A. Trivedi, and M. Zamani, “A scenario approach for syn- thesizing k-inductive barrier certificates,” IEEE Control Systems Letters, vol. 6, pp. 3247–3252, 2022

    2022

  4. [12]

    A fast quantum mechanical algorithm for database search,

    L. K. Grover, “A fast quantum mechanical algorithm for database search,” in Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing (STOC) . ACM, 1996, p. 212–219

    1996

  5. [13]

    Towards Quantum Programs Verification: From Quipper Circuits to QPMC,

    L. Anticoli, C. Piazza, L. Taglialegne, and P. Zuliani, “Towards Quantum Programs Verification: From Quipper Circuits to QPMC,” in Reversible Computation, ser. LNCS, S. Devitt and I. Lanese, Eds., vol. 9720. Springer, 2016, pp. 213–219

    2016

  6. [14]

    An automated deductive verification framework for circuit-building quantum programs,

    C. Chareton, S. Bardin, F. Bobot, V . Perrelle, and B. Valiron, “An automated deductive verification framework for circuit-building quantum programs,” in Programming Languages and Systems, ESOP 2021 , ser. Lecture Notes in Computer Science, N. Yoshida, Ed., vol. 12648. Cham: S...

    2021

  7. [15]

    Giallar: Push-button verification for the Qiskit quantum compiler,

    R. Tao, Y . Shi, J. Yao, X. Li, A. Javadi-Abhari, A. W. Cross, F. T. Chong, and R. Gu, “Giallar: Push-button verification for the Qiskit quantum compiler,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, ser. P...

    2022

  8. [16]

    Quantum abstract interpretation,

    N. Yu and J. Palsberg, “Quantum abstract interpretation,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation . ACM, 2021, p. 542–558

    2021

  9. [17]

    Analyzing quantum programs with LintQ: A static analysis framework for Qiskit,

    M. Paltenghi and M. Pradel, “Analyzing quantum programs with LintQ: A static analysis framework for Qiskit,” Proc. ACM Softw. Eng., vol. 1, no. FSE, 2024

    2024

  10. [18]

    Au- toQ: An automata-based quantum circuit verifier,

    Y .-F. Chen, K.-M. Chung, O. Leng ´al, J.-A. Lin, and W.-L. Tsai, “Au- toQ: An automata-based quantum circuit verifier,” in Computer Aided Verification, C. Enea and A. Lal, Eds. Springer Nature Switzerland, 2023, pp. 139–153

    2023

  11. [19]

    An automata-based framework for verification and bug hunting in quantum circuits,

    Y .-F. Chen, K.-M. Chung, O. Leng ´al, J.-A. Lin, W.-L. Tsai, and D.-D. Yen, “An automata-based framework for verification and bug hunting in quantum circuits,” Proc. ACM Program. Lang. , vol. 7, no. PLDI, Jun. 2023

    2023

  12. [20]

    Verification of quan- tum circuits through discrete-time barrier certificates,

    M. Lewis, S. Soudjani, and P. Zuliani, “Verification of quan- tum circuits through discrete-time barrier certificates,” arXiv preprint arXiv:2408.07591, 2024

    2024 arXiv

  13. [21]

    Formal verification of quantum programs: Theory, tools, and challenges,

    ——, “Formal verification of quantum programs: Theory, tools, and challenges,” ACM Transactions on Quantum Computing , vol. 5, no. 1, 2023

    2023

  14. [22]

    Formal methods for quantum algorithms,

    C. Chareton, D. Lee, B. Valiron, R. Vilmart, S. Bardin, and Z. Xu, “Formal methods for quantum algorithms,” in Handbook of Formal Analysis and Verification in Cryptography , S. Akleylek and B. Dundua, Eds. CRC Press, 2023, pp. 319–422

    2023

  15. [23]

    Automated verification of silq quantum programs using smt solvers,

    M. Lewis, P. Zuliani, and S. Soudjani, “Automated verification of silq quantum programs using smt solvers,” in 2024 IEEE International Conference on Quantum Software (QSW) . IEEE, 2024, pp. 125–134

    2024

  16. [24]

    Safety verification of dynamical systems via k-inductive barrier certificates,

    M. Anand, V . Murali, A. Trivedi, and M. Zamani, “Safety verification of dynamical systems via k-inductive barrier certificates,” in 60th IEEE Conference on Decision and Control (CDC) , 2021, pp. 1314–1320

    2021

  17. [25]

    Formal verification of unknown discrete- and continuous-time systems: A data- driven approach,

    A. Nejati, A. Lavaei, P. Jagtap, S. Soudjani, and M. Zamani, “Formal verification of unknown discrete- and continuous-time systems: A data- driven approach,” IEEE Transactions on Automatic Control , vol. 68, no. 5, pp. 3011–3024, 2023

    2023

  18. [26]

    Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,

    A. Edwards, A. Peruffo, and A. Abate, “Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,” in Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , ser. HSCC ’24. ACM, 2024

    2024

  19. [27]

    On the necessity of barrier certificates,

    S. Prajna and A. Rantzer, “On the necessity of barrier certificates,” IFAC Proceedings Volumes, vol. 38, no. 1, pp. 526–531, 2005, 16th IFAC World Congress

    2005

  20. [28]

    Non-convex scenario optimization,

    S. Garatti and M. C. Campi, “Non-convex scenario optimization,” Mathematical Programming, vol. 209, p. 557–608, 2024

    2024

  21. [29]

    Delta-decidability over the reals,

    S. Gao, J. Avigad, and E. M. Clarke, “Delta-decidability over the reals,” in 2012 27th Annual IEEE Symposium on Logic in Computer Science , 2012, pp. 305–314

    2012

  22. [30]

    Distribution of points in a cube and approximate evalu- ation of integrals,

    I. M. Sobol’, “Distribution of points in a cube and approximate evalu- ation of integrals,” U.S.S.R Comput. Maths. Math. Phys. 7 , vol. 7, pp. 86–112, 1967

    1967

  23. [31]

    Parallelizing the dual revised simplex method,

    Q. Huangfu and J. A. J. Hall, “Parallelizing the dual revised simplex method,” Mathematical Programming Computation , vol. 10, no. 2, pp. 119–142, 2018. [Online]. Available: https://doi.org/10.1007/ s12532-017-0130-5

    2018

  24. [32]

    Z3: An Efficient SMT Solver,

    L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in TACAS 2008, ser. LNCS, vol. 4963. Springer-Verlag, 2008, p. 337–340

    2008

  25. [33]

    Quantum computation,

    D. Aharonov, “Quantum computation,” in Annual Reviews of Computa- tional Physics VI , 1999, pp. 259–346

    1999

  26. [34]

    Safe reach set computation via neural barrier certificates,

    A. Abate, S. Bogomolov, A. Edwards, K. Potomkin, S. Soudjani, and P. Zuliani, “Safe reach set computation via neural barrier certificates,” IFAC-PapersOnLine, vol. 58, no. 11, pp. 107–114, 2024

    2024

  27. [35]

    Uniform sample generation in semialgebraic sets,

    F. Dabbene, D. Henrion, and C. Lagoa, “Uniform sample generation in semialgebraic sets,” in 53rd IEEE Conference on Decision and Control , 2014, pp. 5177–5182

    2014

  28. [36]

    Compositional construction of control barrier functions for continuous-time stochastic hybrid systems,

    A. Nejati, S. Soudjani, and M. Zamani, “Compositional construction of control barrier functions for continuous-time stochastic hybrid systems,” Automatica, vol. 145, p. 110513, 2022

    2022

  29. [37]

    Necessary and sufficient certificates for almost sure reachability,

    R. Majumdar, V . Sathiyanarayana, and S. Soudjani, “Necessary and sufficient certificates for almost sure reachability,”IEEE Control Systems Letters, 2024

    2024

  30. [38]

    Data-driven distributionally robust safety verification using barrier certificates and conditional mean embeddings,

    O. Sch ¨on, Z. Zhong, and S. Soudjani, “Data-driven distributionally robust safety verification using barrier certificates and conditional mean embeddings,” in 2024 American Control Conference (ACC) . IEEE, 2024, pp. 3417–3423

    2024

  31. [39]

    Control barrier functions for stochastic systems under signal temporal logic tasks,

    A. B. Kordabad, M. Charitidou, D. V . Dimarogonas, and S. Soudjani, “Control barrier functions for stochastic systems under signal temporal logic tasks,” in 2024 European Control Conference (ECC). IEEE, 2024, pp. 3213–3219

    2024

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.