pith. machine review for the scientific record. sign in

arxiv: 2605.10474 · v1 · submitted 2026-05-11 · 💻 cs.LG · cs.AI

Recognition: 2 theorem links

· Lean Theorem

Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

Yasmine Abu-Haeyeh , Tobias Ladner , Matthias Althoff , Lars Hedrich
Authors on Pith no claims yet

Pith reviewed 2026-05-12 03:39 UTC · model grok-4.3

classification 💻 cs.LG cs.AI
keywords analog neural networksprocess variationsformal verificationpolynomial zonotopesreachability analysisMonte Carlo simulation
0
0 comments X

The pith

Polynomial models and zonotope reachability let analog neural networks be formally verified under process variations in seconds rather than days.

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

The paper develops a polynomial approximation of neuron circuit behavior when manufacturing process variations are present. It applies reachability analysis with polynomial zonotopes to compute sound bounds on network outputs without running exhaustive Monte Carlo trials. The method is demonstrated on both fully connected and convolutional analog networks across three datasets. If the approach holds, it turns a previously impractical verification task into a routine computation that still captures nearly all variation samples. This matters because analog neural hardware promises speed and power gains but has been hard to certify reliably before fabrication.

Core claim

We present a polynomial-based model that resembles the performance of the neuron circuit under process variations. Then, we formally verify the behavior of the circuit-level model using reachability analysis with polynomial zonotopes, thus avoiding conventional, time-consuming Monte Carlo simulations. Our experimental results confirm the effectiveness of our verification approach by reducing the verification time from days to seconds while enclosing 99% of the variation samples.

What carries the argument

Polynomial zonotopes used in reachability analysis on top of a polynomial model of analog neuron circuits under process variations.

If this is right

  • Verification of both fully-connected and convolutional analog neural networks becomes feasible on standard datasets.
  • The time required drops from days of simulation to seconds of reachability computation.
  • Ninety-nine percent of sampled variation cases remain inside the computed output bounds.
  • Formal methods can replace Monte Carlo sampling for checking analog neural hardware behavior.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same polynomial-zonotope pipeline might be applied to certify other analog circuits that feed into machine-learning pipelines.
  • If the modeling step can be automated for new neuron topologies, the approach could shorten design cycles for variation-aware analog accelerators.
  • The speed gain opens the door to embedding verification inside iterative hardware-optimization loops rather than treating it as a final check.

Load-bearing premise

The polynomial model must capture enough of the actual circuit response to process variations for the resulting zonotope enclosures to stay both sound and tight enough to be useful.

What would settle it

A large-scale Monte Carlo run on the same verified circuits that places more than one percent of variation samples outside the computed reachable sets would show the enclosures are either unsound or too loose for practical verification.

Figures

Figures reproduced from arXiv: 2605.10474 by Lars Hedrich, Matthias Althoff, Tobias Ladner, Yasmine Abu-Haeyeh.

Figure 1
Figure 1. Figure 1: Verification of neural networks: (a) input to neural network, (b) output [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Circuit schematic of the analog neuron circuit: (a) current summation [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Monte Carlo analysis of the neuron netlist output current versus the [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Enclosure of breast cancer dataset: (a) enclosure of the neuron with [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Enclosure of Iris dataset: (a) projection of all dimensions, and (b) [PITH_FULL_IMAGE:figures/full_fig_p006_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Enclosure of the fully-connected model on MNIST: (a) projection of [PITH_FULL_IMAGE:figures/full_fig_p006_8.png] view at source ↗
read the original abstract

Analog neural networks are gaining attention due to their efficiency in terms of power consumption and processing speed. However, since analog neural networks are implemented as physical circuits, they are highly sensitive to manufacturing process variations, which can cause large deviations from the nominal model. We present a polynomial-based model that resembles the performance of the neuron circuit under process variations. Then, we formally verify the behavior of the circuit-level model using reachability analysis with polynomial zonotopes, thus, avoiding conventional, time-consuming Monte Carlo simulations. We evaluate our proposed verification approach on three different datasets, verifying both fully-connected and convolutional analog neural networks. Our experimental results confirm the effectiveness of our verification approach by reducing the verification time from days to seconds while enclosing 99% of the variation samples.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper proposes a polynomial-based surrogate model for the behavior of analog neuron circuits under manufacturing process variations. It then applies reachability analysis using polynomial zonotopes to formally verify the input-output behavior of both fully-connected and convolutional analog neural networks on three datasets, claiming to enclose 99% of variation samples while reducing verification time from days to seconds compared to Monte Carlo simulation.

Significance. If the polynomial surrogate is shown to be a sufficiently accurate and bounded approximation to the transistor-level circuit response (including higher-order effects and parasitics), the method would provide a sound and scalable alternative to Monte-Carlo-based verification for analog neural hardware, addressing a key barrier to reliable deployment of analog ML accelerators.

major comments (3)
  1. [Abstract and §3] Abstract and §3 (model derivation): The central claim that the polynomial-based model 'resembles the performance of the neuron circuit under process variations' is load-bearing for soundness, yet the manuscript provides no quantitative validation (e.g., maximum relative error, Kolmogorov-Smirnov distance, or per-parameter fitting residuals) against SPICE Monte-Carlo ground truth for the same process-variation parameters. Without such bounds, the reported 99% enclosure rate and speed-up do not transfer to the physical circuit.
  2. [§5] §5 (experimental evaluation): The 99% enclosure figure is presented without accompanying tightness metrics (e.g., volume of the zonotope enclosure relative to the sample cloud) or analysis of corner-case deviations outside the 99% region. This leaves open whether the over-approximations remain usefully tight for practical verification or become vacuous for larger networks.
  3. [§4] §4 (reachability with polynomial zonotopes): The transfer of soundness from the zonotope reachability tool to the analog circuit depends entirely on the fidelity of the polynomial surrogate; any unmodeled higher-order variation effects would invalidate the formal guarantees. The paper does not discuss how the polynomial degree was chosen or whether residual modeling error was propagated into the reachability computation.
minor comments (2)
  1. [§3] Notation for the polynomial coefficients and variation parameters should be introduced with explicit definitions and ranges before the reachability section to improve readability.
  2. [Abstract] The abstract states 'enclosing 99% of the variation samples' but does not clarify whether this is measured over the full input domain or only on the test sets; a precise statement would strengthen the claim.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the thoughtful and detailed review of our manuscript. The major comments raise valid points about the validation of the polynomial surrogate model and the presentation of the experimental results. We provide point-by-point responses below and will incorporate revisions to address these concerns.

read point-by-point responses

  1. Referee: [Abstract and §3] Abstract and §3 (model derivation): The central claim that the polynomial-based model 'resembles the performance of the neuron circuit under process variations' is load-bearing for soundness, yet the manuscript provides no quantitative validation (e.g., maximum relative error, Kolmogorov-Smirnov distance, or per-parameter fitting residuals) against SPICE Monte-Carlo ground truth for the same process-variation parameters. Without such bounds, the reported 99% enclosure rate and speed-up do not transfer to the physical circuit.

    Authors: We acknowledge the importance of quantitative validation for establishing the fidelity of the polynomial-based model. While the abstract and §5 report that the verification encloses 99% of variation samples from the model, we agree that explicit metrics comparing the surrogate to SPICE Monte Carlo simulations are not detailed in the current version. In the revised manuscript, we will add quantitative validation results in §3, including maximum relative error, fitting residuals, and statistical measures such as the Kolmogorov-Smirnov distance between the polynomial model outputs and SPICE simulations under the same process variation parameters. This will provide the necessary bounds to support the soundness claims. revision: yes

  2. Referee: [§5] §5 (experimental evaluation): The 99% enclosure figure is presented without accompanying tightness metrics (e.g., volume of the zonotope enclosure relative to the sample cloud) or analysis of corner-case deviations outside the 99% region. This leaves open whether the over-approximations remain usefully tight for practical verification or become vacuous for larger networks.

    Authors: We agree that the 99% enclosure rate alone does not fully characterize the quality of the over-approximation. The manuscript currently emphasizes the computational advantage and the high enclosure percentage. To address this, we will update §5 to include tightness metrics, such as the volume of the polynomial zonotope relative to the volume of the minimum enclosing ellipsoid or convex hull of the Monte Carlo samples. We will also provide an analysis of the outliers beyond the 99% region, quantifying their deviations and discussing implications for larger networks to ensure the enclosures remain practically useful. revision: yes

  3. Referee: [§4] §4 (reachability with polynomial zonotopes): The transfer of soundness from the zonotope reachability tool to the analog circuit depends entirely on the fidelity of the polynomial surrogate; any unmodeled higher-order variation effects would invalidate the formal guarantees. The paper does not discuss how the polynomial degree was chosen or whether residual modeling error was propagated into the reachability computation.

    Authors: The reachability analysis with polynomial zonotopes provides formal guarantees for the input-output behavior of the polynomial surrogate model, as described in §4. We will revise the manuscript to discuss the choice of polynomial degree in §3 and §4, explaining the trade-off between accuracy and complexity that guided our selection. Furthermore, we will clarify that the residual error of the surrogate is not propagated as an additional uncertainty set in the current reachability computation; instead, the 99% enclosure serves as empirical evidence of model fidelity. We will add a note on how increasing the polynomial degree can capture higher-order effects if needed, and how the validation metrics will help bound any remaining discrepancies. revision: yes

Circularity Check

0 steps flagged

No circularity: new surrogate model plus standard reachability applied to it

full rationale

The paper introduces a polynomial-based surrogate for analog neuron behavior under process variation, then applies existing polynomial-zonotope reachability (from prior literature) to compute enclosures on that surrogate. Experimental results compare the enclosures against independent Monte-Carlo samples drawn from the same variation parameters, reporting coverage and runtime. No equation or claim reduces the reported verification result to a quantity defined by the authors' own fitting procedure or prior self-citation; the central claim remains an empirical demonstration that the surrogate-plus-reachability pipeline is faster than direct Monte-Carlo while still enclosing the sampled points. The model-fidelity assumption is stated but does not create a definitional loop inside the derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no identifiable free parameters, axioms, or invented entities; the polynomial model and zonotope representation are presented as tools rather than new postulates requiring independent evidence.

pith-pipeline@v0.9.0 · 5432 in / 1120 out tokens · 57456 ms · 2026-05-12T03:39:50.726180+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    Efficient hardware architectures for accelerating deep neural networks: Survey,

    P. Dhilleswararao, S. Boppu, M. S. Manikandan, and L. R. Cenkeramaddi, “Efficient hardware architectures for accelerating deep neural networks: Survey,”IEEE Access, 2022

    work page 2022

  2. [2]

    The promise of analog deep learning: Recent advances, challenges and opportunities,

    A. Datar and P. Saha, “The promise of analog deep learning: Recent advances, challenges and opportunities,”arXiv preprint arXiv:2406.12911, 2024

    work page arXiv 2024

  3. [3]

    PolyThrottle: Energy- efficient neural network inference on edge devices,

    M. Yan, H. Wang, and S. Venkataraman, “PolyThrottle: Energy- efficient neural network inference on edge devices,”arXiv preprint arXiv:2310.19991, 2023

    work page arXiv 2023

  4. [4]

    Overview of emerging electronics technologies for artificial intelligence: A review,

    P. Gao and M. Adnan, “Overview of emerging electronics technologies for artificial intelligence: A review,”Materials Today Electronics, 2025

    work page 2025

  5. [5]

    J3DAI: A tiny DNN-based edge AI accelerator for 3D-stacked CMOS image sensor,

    B. Tain, R. Millet, R. Lemaire, M. Szczepanski, L. Alacoque, E. Pluchart, S. Choisnet, R. Prasad, J. Chossat, P. Pieruneket al., “J3DAI: A tiny DNN-based edge AI accelerator for 3D-stacked CMOS image sensor,” arXiv preprint arXiv:2506.15316, 2025

    work page arXiv 2025

  6. [6]

    Statistical performance modeling and optimization,

    X. Li, J. Le, L. T. Pileggiet al., “Statistical performance modeling and optimization,”Foundations and Trends in Electronic Design Automation, 2007

    work page 2007

  7. [7]

    Computing-in-memory neural network accelerators for safety-critical systems: Can small device variations be disastrous?

    Z. Yan, X. S. Hu, and Y . Shi, “Computing-in-memory neural network accelerators for safety-critical systems: Can small device variations be disastrous?” inProceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, 2022

    work page 2022

  8. [8]

    On the accuracy of analog neural network inference accelerators,

    T. P. Xiao, B. Feinberg, C. H. Bennett, V . Prabhakar, P. Saxena, V . Agrawal, S. Agarwal, and M. J. Marinella, “On the accuracy of analog neural network inference accelerators,”IEEE Circuits and Systems Magazine, 2023

    work page 2023

  9. [9]

    Design and validation of an artificial neural network based on analog circuits,

    F. B. Gencer, X. Xhafa, B. B. ˙Inam, and M. B. Yelten, “Design and validation of an artificial neural network based on analog circuits,”Analog Integrated Circuits and Signal Processing, 2021

    work page 2021

  10. [10]

    Modeling the dependency of analog circuit performance parameters on manufacturing process variations with applications in sensitivity analysis and yield prediction,

    E.-D. ¸ Sandru, E. David, I. Kovacs, A. Buzo, C. Burileanu, and G. Pelz, “Modeling the dependency of analog circuit performance parameters on manufacturing process variations with applications in sensitivity analysis and yield prediction,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2021

    work page 2021

  11. [11]

    Formal verification of analog circuits in the presence of noise and process variation,

    R. Narayanan, B. Akbarpour, M. H. Zaki, S. Tahar, and L. C. Paulson, “Formal verification of analog circuits in the presence of noise and process variation,” inIEEE Design, Automation & Test in Europe Conference & Exhibition, 2010

    work page 2010

  12. [12]

    Machine learning-assisted device modeling with process variations for advanced technology,

    Y . Lyu, W. Chen, M. Zheng, B. Yin, J. Li, and L. Cai, “Machine learning-assisted device modeling with process variations for advanced technology,”IEEE Journal of the Electron Devices Society, 2023

    work page 2023

  13. [13]

    Glova: Global and local variation-aware analog circuit design with risk-sensitive reinforcement learning,

    D. Kim, J. Park, C. Shin, J. Jung, K. Shin, S. Baek, S. Heo, W. Kim, I. Jeong, J. Choet al., “Glova: Global and local variation-aware analog circuit design with risk-sensitive reinforcement learning,”arXiv preprint arXiv:2505.11208, 2025

    work page arXiv 2025

  14. [14]

    Important considerations regarding device parameter process variations in semiconductor-based manufacturing,

    M. Huff, “Important considerations regarding device parameter process variations in semiconductor-based manufacturing,”ECS Journal of Solid State Science and Technology, 2021

    work page 2021

  15. [15]

    Explaining and harnessing adversarial examples,

    I. Goodfellow, J. Shlens, and C. Szegedy, “Explaining and harnessing adversarial examples,” inInternational Conference on Learning Representations, 2015

    work page 2015

  16. [16]

    On the sensitivity of analog artificial neural network models to process variation,

    N. Afroz, A. Sayem, G. V olanis, D. Maliuk, H. Stratigopoulos, and Y . Makris, “On the sensitivity of analog artificial neural network models to process variation,” inIEEE 42nd VLSI Test Symposium, 2024

    work page 2024

  17. [17]

    Calibrating process variation at system level with in-situ low-precision transfer learning for analog neural network processors,

    K. Jia, Z. Liu, Q. Wei, F. Qiao, X. Liu, Y . Yang, H. Fan, and H. Yang, “Calibrating process variation at system level with in-situ low-precision transfer learning for analog neural network processors,” inProceedings of the 55th Annual Design Automation Conference, 2018

    work page 2018

  18. [18]

    Formally verifying analog neural networks with device mismatch variations,

    Y . Abu-Haeyeh, T. Bartelsmeier, T. Ladner, M. Althoff, L. Hedrich, and M. Olbrich, “Formally verifying analog neural networks with device mismatch variations,”Proceedings of the 28th IEEE Design, Automation and Test in Europe Conference, 2025

    work page 2025

  19. [19]

    Overview of emerging semiconductor device model methodologies: From device physics to machine learning engines,

    X. Li, Z. Wu, G. Rzepa, M. Karner, H. Xu, Z. Wu, W. Wang, G. Yang, Q. Luo, L. Wanget al., “Overview of emerging semiconductor device model methodologies: From device physics to machine learning engines,” Fundamental Research, 2024

    work page 2024

  20. [20]

    Analog multiply-accumulate cell with multi-bit resolution for all-analog ai inference accelerators,

    R. Nägele, J. Finkbeiner, V . Stadtlander, M. Grözing, and M. Berroth, “Analog multiply-accumulate cell with multi-bit resolution for all-analog ai inference accelerators,”IEEE Transactions on Circuits and Systems I: Regular Papers, 2023

    work page 2023

  21. [21]

    and Koller, Lukas and Manino, Edoardo and Nguyen, ThanhVu H

    K. Kaulen, T. Ladner, S. Bak, C. Brix, H. Duong, T. Flinkow, T. T. Johnson, L. Koller, E. Manino, T. H. Nguyenet al., “The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results,”arXiv preprint arXiv:2512.19007, 2025

    work page arXiv 2025

  22. [22]

    ARCH-COMP24 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants,

    D. M. Lopez, M. Althoff, L. Benet, C. Blab, M. Forets, Y . Jia, T. T. Johnson, M. Kranzl, T. Ladner, and L. Linauer, “ARCH-COMP24 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants,” inProceedings of the 11th Int. Workshop on Applied Verification for Continuous and Hybrid Systems, 2024

    work page 2024

  23. [23]

    Safety verification of deep neural networks,

    X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks,” inInternational Conference on Computer Aided Verification, 2017

    work page 2017

  24. [24]

    Reluplex: An efficient SMT solver for verifying deep neural networks,

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” inInternational Conference on Computer Aided Verification, 2017

    work page 2017

  25. [25]

    Efficient neural network robustness certification with general activation functions,

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” inAdvances in Neural Information Processing Systems, 2018

    work page 2018

  26. [26]

    The Marabou framework for verification and analysis of deep neural networks,

    G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji ´c, D. L. Dill, M. J. Kochenderfer, and C. Barret, “The Marabou framework for verification and analysis of deep neural networks,” inInternational Conference on Computer Aided Verification, 2019

    work page 2019

  27. [27]

    Efficient neural network verification via adaptive refinement and adversarial search,

    P. Henriksen and A. Lomuscio, “Efficient neural network verification via adaptive refinement and adversarial search,” inEuropean Conference on Artificial Intelligence, 2020

    work page 2020

  28. [28]

    An abstract domain for certifying neural networks,

    G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” inProceedings of the ACM on Programming Languages, 2019

    work page 2019

  29. [29]

    AI2: Safety and robustness certification of neural networks with abstract interpretation,

    T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “AI2: Safety and robustness certification of neural networks with abstract interpretation,” inIEEE Symposium on Security and Privacy, 2018

    work page 2018

  30. [30]

    Fast and effective robustness certification,

    G. Singh, T. Gehr, M. Mirman, M. Püschel, and M. Vechev, “Fast and effective robustness certification,”Advances in Neural Information Processing Systems, 2018

    work page 2018

  31. [31]

    NNV 2.0: The neural network verification tool,

    D. M. Lopez, S. W. Choi, H.-D. Tran, and T. T. Johnson, “NNV 2.0: The neural network verification tool,” inInternational Conference on Computer Aided Verification, 2023

    work page 2023

  32. [32]

    Automatic abstraction refinement in neural network verification using sensitivity analysis,

    T. Ladner and M. Althoff, “Automatic abstraction refinement in neural network verification using sensitivity analysis,” inProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, 2023

    work page 2023

  33. [33]

    C. M. Bishop and N. M. Nasrabadi,Pattern recognition and machine learning, 2006

    work page 2006

  34. [34]

    Sparse polynomial zonotopes: A novel set representation for reachability analysis,

    N. Kochdumper and M. Althoff, “Sparse polynomial zonotopes: A novel set representation for reachability analysis,” inIEEE Transactions on Automatic Control, 2020

    work page 2020

  35. [35]

    Formal verification of graph convolutional networks with uncertain node features and uncertain graph structure,

    T. Ladner, M. Eichelbeck, and M. Althoff, “Formal verification of graph convolutional networks with uncertain node features and uncertain graph structure,”Transactions of Machine Learning Research, 2025

    work page 2025

  36. [36]

    Out of the shadows: Exploring a latent space for neural network verification,

    L. Koller, T. Ladner, and M. Althoff, “Out of the shadows: Exploring a latent space for neural network verification,”International Conference on Learning Representations, 2026

    work page 2026

  37. [37]

    Schematic generation of programmable analog neural networks for signal proccessing,

    F. Aul, N. Katsaouni, L. Krischker, S. Schmalhofer, M. H. Schulz, and L. Hedrich, “Schematic generation of programmable analog neural networks for signal proccessing,” inInternational Conference on SMACD and 16th Conference on PRIME, 2021

    work page 2021

  38. [38]

    Model conformance for cyber-physical systems: A survey,

    H. Roehm, J. Oehlerking, M. Woehrle, and M. Althoff, “Model conformance for cyber-physical systems: A survey,”ACM Transactions on Cyber-Physical Systems, 2019

    work page 2019

  39. [39]

    Breast Cancer Wisconsin (Original),

    W. Wolberg, “Breast Cancer Wisconsin (Original),” UCI Machine Learning Repository, 1990

    work page 1990

  40. [40]

    R. A. Fisher, “Iris,” UCI Machine Learning Repository, 1936

    work page 1936

  41. [41]

    Mnist handwritten digit database,

    Y . LeCun, C. Cortes, and C. J. Burges, “Mnist handwritten digit database,” http://yann.lecun.com/exdb/mnist, 2010

    work page 2010

  42. [42]

    Cadence virtuoso spectre simulator datasheet,

    Cadence Design Systems, Inc., “Cadence virtuoso spectre simulator datasheet,” www.cadence.com, 2024

    work page 2024

  43. [43]

    An introduction to CORA 2015,

    M. Althoff, “An introduction to CORA 2015,” inProceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, 2015

    work page 2015

  44. [44]

    Reachability of uncertain linear systems using zonotopes,

    A. Girard, “Reachability of uncertain linear systems using zonotopes,” in International Workshop on Hybrid Systems: Computation and Control, 2005

    work page 2005