Pith. sign in

REVIEW 4 major objections 5 minor 96 references

Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read A Demon-versus-Angel game carries infinite-horizon safety of neural controllers through finite-precision rounding, via decidable real-arithmetic checks and code synthesized inside the verified error bound.

desk verdict A solid extension of VerSAILLE to finite-precision safety via a game-based robustness criterion; the main reduction relies on a hand-proved Pullback Axiom that deserves careful checking before publication. read the letter →

arxiv 2507.22760 v1 pith:W6S77JZX submitted 2025-07-30 eess.SY cs.AIcs.LGcs.LOcs.SY

Samuel Teuber , Debasmita Lohar , Bernhard Beckert This is my paper
classification eess.SYcs.AIcs.LGcs.LOcs.SY MSC 68Q6003B70
keywords differentialdynamiclogicgameneural-network-controlledcyber-physicalsystemsinfinite-horizonsafetyroundofferrorsfixed-pointarithmeticangelicperturbationsmixed-precisiontuning
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

Differential Dynamic Logic can prove infinite-time horizon safety for neural-network-controlled systems, but only under idealized real-valued semantics; on real hardware, rounding errors at nearly every operation can silently void the guarantee. This paper claims that formal safety can be carried through to actual fixed-point implementations by modeling finite-precision effects — in sensing, actuation, and computation — as a bounded adversary in a hybrid game: a good Demon chooses control actions, a bad Angel injects perturbations. It proves that both the robustness of the control envelope and the infinite-horizon safety of a concrete neural implementation reduce to decidable real-arithmetic formulas, and that a sound mixed-precision fixed-point implementation can be synthesized inside the verified error bound, closing the loop from proof to deployable code. A reader should care because the method is demonstrated on ACC and vertical collision-avoidance control, where a previously proven 'safe' real-valued envelope turns out to fail under arbitrarily small output perturbations.

What carries the argument

The load-bearing mechanism is the Pullback Axiom (Lemma 2), a rule derived by hand from the $K_{\langle\rangle}$ axiom of differential dynamic logic: $\forall\bar{x}^{+}(\psi \to \langle\alpha\rangle\xi) \land \exists\bar{x}^{+}(\psi \land \forall\bar{x}(\xi \to \phi)) \to \langle\alpha\rangle\phi$, with side conditions requiring that $\bar{x}$ contain all variables of $\langle\alpha\rangle\phi$ and that $\bar{x}^{+}$ be exactly the free variables of $\psi \land \xi$ outside $\bar{x}$. The axiom lets the proof pull the post-control state back into the current state, transforming the game-theoretic robustness condition into the decidable real-arithmetic formula (4); first-order real arithmetic admits quantifier elimination and SMT solving, so undecidable game-logic validity is bypassed. The supporting machinery comprises angelic perturbations formalized as pairs of discrete, loop-free hybrid programs; controller-monitor formulas from the monitor-synthesis method [41] that are exact for such programs; the agreement of game-logic and dynamic-logic semantics on duality-free formulas; and reuse of the original safety proof's loop invariant as the inductive invariant of the game. The quantifier structure $\forall\bar{x}_0\,\forall x_1\,\exists\bar{x}_2\,\forall\bar{x}_3$ of formula (4) mirrors the game's turn order: the first universal quantifier absorbs the pre-perturbation, the existential quantifier is the Demon's choice of a control action, and the final universal quantifier is the post-perturbation.

What would settle it

Machine-check the appendix's hand-written proof of the Pullback Axiom in the uniform-substitution calculus of a hybrid-systems theorem prover, discharging both side conditions ($\bar{x} \supseteq V(\langle\alpha\rangle\phi)$ and $\bar{x}^{+} = FV(\psi \land \xi) \setminus \bar{x}$) for the exact instantiations used in the robot and ACC robustness proofs; if the derivation does not go through, the reduction of game robustness to decidable real arithmetic is unsound. The empirical side can be tested independently: for the revised ACC envelope, search reachable states for a perturbation pair $(\varepsilon_p, \varepsilon_v)$ within the verified bound that satisfies the antecedent of formula (6) yet drives the system outside the safe set, a concrete hit exposing an error in the monitor or perturbation model rather than in the theorem.

Watch

Extended reading notes

Core claim

The paper's central claim is that a provably safe differential-dynamic-logic model of a neural feedback system remains trustworthy when the controller runs in finite-precision arithmetic, provided the control envelope is robust to bounded perturbations and the implementation's worst-case rounding error stays inside the verified bound. Robustness (Definition 3) is a game property: in the hybrid game $(\mathit{angel}_{pre};(\mathit{ctl})^{d};\mathit{angel}_{post};\mathit{env})^{*}$, the good Demon, who controls the choices inside the envelope $\mathit{ctl}$ through the duality superscript $d$, must have a winning strategy to keep the safety predicate, while the bad Angel chooses perturbations before and after the controller and controls the environment. Theorem 1 reduces this game-theoretic condition to the validity of a decidable real-arithmetic formula with quantifier prefix $\forall\bar{x}_0\,\forall x_1\,\exists\bar{x}_2\,\forall\bar{x}_3$, built from the loop invariant and from controller-monitor formulas for the envelope and the perturbation programs; the existential quantifier is exactly the Demon's choice of a safe action, and the universal quantifiers are the Angel's perturbing moves. Theorem 2 reduces infinite-horizon safety of a concrete implementation under the same perturbations to the validity of formula (6), which real-valued neural-network verifiers can prove or refute directly, a counterexample being a concrete input-perturbation pair. Together with a fixed-point implementation synthesized by mixed-precision tuning whose worst-case error is bounded by the perturbation magnitude, this yields an end-to-end, infinite-horizon safety guarantee for the deployed controller. The paper is driven by the observation that this robustness is necessary, not a nicety: the continuous ACC envelope from prior work and the unidirectional robot envelope are provably safe in real arithmetic yet fail under arbitrarily small output perturbations.

Load-bearing premise

The argument leans on the Pullback Axiom — a rule derived by hand from a standard axiom of differential dynamic logic and never machine-checked, which drags the post-control state back into the current state — and if that rule is unsound, or is applied where its side conditions fail, the reduction of game robustness to a decidable real-arithmetic formula collapses.

Editorial extensions

If this is right

  • Control envelopes that are provably safe in real arithmetic still need a robustness check before they can certify controllers running on real hardware; the paper shows that the continuous ACC envelope from earlier work and the unidirectional robot envelope fail under arbitrarily small output perturbations, and it revises the ACC envelope to make a finite-precision guarantee possible.
  • Verifying a neural network under perturbation reduces to the real-arithmetic specification (6), which existing real-valued NN verifiers can discharge, and refuting it yields a concrete input-perturbation counterexample, keeping the hard reasoning in decidable arithmetic.
  • Any fixed-point implementation whose worst-case rounding error is bounded by the verified perturbation magnitude inherits the infinite-horizon safety guarantee; the paper synthesizes mixed-precision fixed-point code within that bound and compiles it to FPGA hardware, reporting latencies between 567 and 656 cycles.
  • Liveness is a special case of robustness: with trivial (skip) perturbations, the robustness game asks exactly whether the envelope offers a safe action in every reachable state.
  • Because the real-arithmetic conditions depend only on the envelope's monitor formulas and the perturbation model, the same pipeline extends beyond neural networks to other controller classes, as the paper states.

Reading between the lines

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

  • Because formula (4) is only a sufficient condition for robustness, a failed check leaves the cause ambiguous — an unreachable spurious counterexample always remains possible. The paper's own completeness remark (with $pre \leftrightarrow \chi_{inv}$ every counterexample is genuine) points to an automated extension: synthesize stronger loop invariants until the criterion becomes exact, turning the
  • The Demon-versus-Angel robustness game is a general template for 'the controller still works under bounded disturbance' that reaches beyond finite precision; sizing actuator tolerances, comparing candidate envelopes by perturbation margin, or deriving fallback-trigger conditions are natural uses the paper only gestures at.
  • The single non-machine-checked step in the end-to-end chain is the hand-derived Pullback Axiom; formalizing Lemma 2 in the prover's own calculus would make the whole pipeline, from envelope proof through NN verification to synthesis, uniformly machine-checked, which is the natural next assurance milestone.
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

4 major / 5 minor

Summary. This paper proposes a method to extend infinite-time horizon safety guarantees for neural-network-controlled cyber-physical systems (NNCSs) from idealized real-valued differential dynamic logic (dL) to finite-precision implementations. The authors model sensing, actuation, and computational perturbations as bounded 'angelic' hybrid programs and define control-envelope robustness as a differential game in which a good Demon chooses control actions against a bad Angel's perturbations. The main theoretical results are Theorem 1, which reduces envelope robustness to a decidable real-arithmetic condition (Eq. 4), and Theorem 2, which reduces safety of a concrete implementation under perturbation to a decidable formula (Eq. 6). These conditions are used in an end-to-end pipeline: mixed-precision fixed-point implementations are synthesized with Daisy and compiled with Vivado HLS. The method is evaluated on an adaptive cruise control (ACC) system and a vertical airborne collision avoidance system (VCAS), producing fixed-point implementations with measured latency and verified safety under bounded perturbations.

Significance. If the theorems are correct, this is a valuable step toward closing the gap between formal infinite-horizon guarantees for NNCSs and their actual finite-precision implementations. The paper's strengths include a clean game-theoretic formulation of robustness, the use of established tools (KeYmaera X, N3V, Daisy, Vivado HLS) in realistic case studies, and an honest acknowledgment that Theorem 1 provides only a sufficient criterion for robustness. The quantitative evaluation shows that perturbation-aware verification remains feasible for networks of practical size. The claim that robustness is a necessary condition for any implementation safety under perturbation is conceptually important for guiding the verification workflow.

major comments (4)
  1. [Appendix, Lemma 2] The Pullback Axiom is the load-bearing step that turns the dGL game condition (Eq. 3) into the decidable real-arithmetic formula (Eq. 4) in Theorem 1, yet its statement is ambiguous and its proof is only a sketch. The side conditions 'Äïö‰ï¸ï±ø≕ï¸øðï¸ï°ðï¸ðùï¸ÿýï¸ðôï¸þðï¸øø' mixing vectors and sets of variables makes it unclear exactly which variables the axiom requires α to leave untouched. The proof step 'Via V' asserts that α only changes variables bound by the universal quantifier, but this is not made precise, and the subsequent universal instantiation under the box modality requires careful ghost-variable bookkeeping. Because Theorem 1 directly depends on this axiom, the central reduction from robustness to decidable real arithmetic is not fully verified as written. Please restate the axiom with explicit side conditions on the sets of modified variables, and provide a complete derivation in the dL proof calculus (ideally machine-checked in KeYmaera X) rather than a paper-and-pencil sketch.
  2. [Appendix, Proof of Theorem 1] The proof of Theorem 1 contains several steps marked 'via a Monotonicity argument' and 'simple reasoning' that are not detailed enough to verify, particularly the transformation that introduces and then eliminates the angelpost modality, the use of ghost variables, and the final conversion from the Pullback Axiom instantiation to Formula (4). Since the theorem is the basis for the robustness pre-check and the paper's claim that robustness is a decidable sufficient condition, this proof must be expanded so that each inference rule is explicit, or supplemented by a machine-checked proof artifact. Without this, a reviewer cannot fully certify the soundness of the central claim.
  3. [Section IV-D] The paper repeatedly states that robustness of the control envelope is a necessary condition for safety of any implementation under perturbation (e.g., in the ACC continuous case study and in the discussion of ctl1_1), but this implication is never stated as a formal lemma or proved. It is a short argument from Definition 3 and the fact that an implementation's actions are a subset of the envelope, but it should be made explicit and proved (or at least stated as a corollary of Theorem 2) because it is used to interpret negative results and to justify the pre-verification robustness check.
  4. [Section V] The end-to-end guarantee relies on matching the perturbation bounds assumed in the safety proofs with the worst-case error bounds computed by Daisy for the fixed-point implementations. The paper does not explicitly document how sensor input quantization (the δ_p perturbation in angelpre) is accounted for in Daisy's error analysis, nor does it confirm that the input ranges used by Daisy coincide with the invariant region used in the NN verification. Please state these details and, if necessary, provide the exact error-bound certificates from Daisy for the reported case studies, so that the claimed 'complete end-to-end solution' is fully supported.
minor comments (5)
  1. [Section III-A2] Typo: 'alligns' should be 'aligns'.
  2. [Section IV-A] Typo: 'computated' should be 'computed'.
  3. [Section IV-D] Typo: 'pertrubations' should be 'perturbations'.
  4. [Section IV-A] The formula for implR is typeset ambiguously as 'v+ = − 1 0.01(p+10) +M'; the intended expression is likely v+ = -1/(0.01(p+10)) + M. Please correct the typesetting.
  5. [Table I] The perturbation bounds for the VCAS rows are written as '25−3', which is ambiguous; if this denotes 2^-5 or 2^-3, please write it in standard mathematical notation (e.g., 2^{-5}).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the dGL-to-real-arithmetic reductions are proven from the dL calculus, and the perturbation bounds are explicit assumptions rather than fitted predictions.

full rationale

The derivation chain is self-contained rather than circular. Theorem 1 (Section IV-C) proves that the real-arithmetic Formula (4) implies the game-theoretic robustness property of Definition 3 using the dGL proof calculus and the Pullback Axiom (Lemma 2). The Pullback Axiom is not an imported uniqueness result or an ansatz; the paper supplies a derivation from the K< > axiom of dL. Even if that hand-written lemma is a soundness risk, it is not an input fitted to the target conclusion. Theorem 2 (Section IV-D) similarly derives the perturbed safety property (Formula 5) from the decidable condition (Formula 6) via monotonicity, ghost variables, and the definition of the controller monitor, without presupposing the conclusion. The perturbation bounds delta are explicit assumptions used to instantiate the theorems; they are not selected by fitting the safety proof, and Daisy's roundoff-error certificates are computed independently from the synthesized implementation rather than used to define the safety property. The paper's self-citations to VerSAILLE [32] and N3V [75] are dependencies on previously published theorems and tools, not unverified self-justifying premises that force the result. The claim that robustness is a necessary condition for finite-precision dL-based NN verification is a direct logical consequence of Definition 3 and the controller-monitor definition, not a hidden equivalence with the sufficient criterion. Overall, no prediction or first-principles result reduces by construction to its own inputs.

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

The approach is a verification methodology, not a physical theory. The main free parameters are the user-chosen perturbation bounds, which define the scope of the guarantee; the derived results are conditional on those bounds and on the soundness of the cited tools (dL/dGL calculus, ModelPlex, Daisy, N3V).

free parameters (5)
  • δv (robot output perturbation bound) = 0.25
    Chosen by hand for the robot example to make robustness provable; the envelope is robust for δv ≤ Vmax/2 and the implementation safety proof uses δv = 0.25.
  • δp (robot sensor perturbation bound) = 0.25
    Chosen by hand for the robot example, used in the KeYmaera X proof of Formula (6) for all four combinations.
  • δ_ACC_cont = 1.0
    Perturbation bound for continuous ACC; Daisy must meet this error bound; chosen as the worst-case error bound for the case study.
  • δ_ACC_disc = 0.01
    Perturbation bound for discrete ACC; chosen so that 32-bit uniform precision suffices to meet the error requirement.
  • δ_VCAS = 2^-5 (as printed: '25−3')
    Perturbation bound for VCAS case studies; 42-bit uniform precision was required to meet it.
assumptions (5)
  • standard math Soundness of the dL and dGL proof calculi and their axioms, including the K<> axiom used in Lemma 2.
    The theorems' proofs in the Appendix rely on the dL/dGL proof calculus from [43], [44], [47].
  • domain assumption ModelPlex controller, pre, and post monitors are exact for concrete, discrete, loop-free hybrid programs.
    Used in Theorem 1 and 2 to replace programs χpre, χctrl, χpost with equivalent first-order formulas; exactness is claimed via [41], [52].
  • domain assumption Angelic perturbations are restricted to concrete, discrete, loop-free hybrid programs, so that exact monitors exist and the real-arithmetic criteria are decidable.
    Definition 2 and the sentence 'Our formulation induces decidable real-arithmetic conditions applicable to any discrete, loop-free angelic perturbation.'
  • domain assumption Daisy's mixed-precision fixed-point error bounds are sound for truncation rounding and the targeted FPGA synthesis flow.
    Section IV-E uses Daisy to bound the worst-case roundoff error; soundness is inherited from [39].
  • domain assumption Soundness of the NN verifier N3V (and its underlying solvers Z3, PicoSAT, nnenum) for the produced polynomial specifications.
    Section V-A and IV-D rely on N3V to prove Formula (6) for the NN case studies.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision." pith.science (2026). https://pith.science/paper/W6S77JZX

@misc{pith2026250722760,
  author       = {Pith},
  title        = {Pith review of: Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W6S77JZX}},
  note         = {Machine review of arXiv:2507.22760}
}
read the original abstract

As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations -- in sensing, actuation, and computation -- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.

Figures

Figures reproduced from arXiv: 2507.22760 by the authors.

Figure 2
Figure 2. A robot at distance p controls its velocity v and avoids an obstacle (p ≥ 0). a) Ground Robot Example: The robot, at distance p ∈ R to an obstacle, moves along a corridor (see [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 1
Figure 1. Overview of approach which assumes a safe [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

96 extracted references · 78 canonical work pages

  1. [1]

    Safe reinforcement learning via formal meth- ods: Toward safe control through proof and learning,

    N. Fulton and A. Platzer, “Safe reinforcement learning via formal meth- ods: Toward safe control through proof and learning,” in Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI- 18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Int...

    2018

  2. [2]

    Safe deep reinforcement learning for adaptive cruise control by impos- ing state-specific safe sets,

    M. Brosowsky, F. Keck, J. Ketterer, S. Isele, D. Slieter, and M. Zöllner, “Safe deep reinforcement learning for adaptive cruise control by impos- ing state-specific safe sets,” in2021 IEEE Intelligent Vehicles Symposium (IV), pp. 488–495, 2021

    2021

  3. [3]

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

    T. T. Johnson, D. M. Lopez, L. Benet, M. Forets, S. Guadalupe, C. Schilling, R. Ivanov, T. J. Carpenter, J. Weimer, and I. Lee, “ARCH- COMP21 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants,” in 8th International Workshop on Applied Verification of Continuous and Hybrid Systems ...

    2021

  4. [4]

    Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems

    K. D. Julian and M. J. Kochenderfer, “Guaranteeing safety for neural network-based aircraft collision avoidance systems,” vol. abs/1912.07084, 2019

    work page Pith review arXiv 1912

  5. [5]

    Policy compression for aircraft collision avoidance systems,

    K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer, “Policy compression for aircraft collision avoidance systems,” in 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), pp. 1–10, 2016

    2016

  6. [6]

    Efficient neural network robustness certification with general activation functions,

    H. Zhang, T. Weng, P. Chen, C. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” in Advances in Neural Information Processing Systems 31: Annual Con- ference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada (S. Bengio, H. M. Wallach, H. Larochelle, ...

    2018

  7. [7]

    Automatic perturbation analysis for scalable certified robustness and beyond,

    K. Xu, Z. Shi, H. Zhang, Y . Wang, K. Chang, M. Huang, B. Kailkhura, X. Lin, and C. Hsieh, “Automatic perturbation analysis for scalable certified robustness and beyond,” in Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (H. Larochelle, M. Ra...

    2020

  8. [8]

    Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,

    K. Xu, H. Zhang, S. Wang, Y . Wang, S. Jana, X. Lin, and C. Hsieh, “Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,” in 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021 , 2021

    2021

Show all 96 references
  1. [9]

    Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C. Hsieh, and J. Z. Kolter, “Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,” in Advances in Neural Information Processing Systems 34: Annual Conference on Neural I...

    2021

  2. [10]

    Efficient neural network verification via adaptive refinement and adversarial search,

    P. Henriksen and A. R. Lomuscio, “Efficient neural network verification via adaptive refinement and adversarial search,” in ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020...

    2020

  3. [11]

    DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis,

    P. Henriksen and A. Lomuscio, “DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis,” in Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27...

    2021

  4. [12]

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

    G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” in Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I (...

    2017

  5. [13]

    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. Zeljic, D. L. Dill, M. J. Kochenderfer, and C. W. Barrett, “The Marabou framework for verification and analysis of deep neural networks,” in Computer Aided Verification - 31st Inter...

    2019

  6. [14]

    Branch and bound for piecewise linear neural network verification,

    R. Bunel, J. Lu, I. Turkaslan, P. H. S. Torr, P. Kohli, and M. P. Kumar, “Branch and bound for piecewise linear neural network verification,” J. Mach. Learn. Res. , vol. 21, pp. 42:1–42:39, 2020

    2020

  7. [15]

    Improved geometric path enumeration for verifying ReLU neural networks,

    S. Bak, H. Tran, K. Hobbs, and T. T. Johnson, “Improved geometric path enumeration for verifying ReLU neural networks,” in Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I (S. K. Lahiri and C. Wa...

    2020

  8. [16]

    nnenum: Verification of ReLU neural networks with optimized abstraction refinement,

    S. Bak, “nnenum: Verification of ReLU neural networks with optimized abstraction refinement,” in NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings (A. Dutle, M. M. Moscato, L. Titolo, C. A. Muñoz, and I. Perez, eds.), vol...

    2021

  9. [17]

    General cutting planes for bound-propagation-based neural network verification,

    H. Zhang, S. Wang, K. Xu, L. Li, B. Li, S. Jana, C. Hsieh, and J. Z. Kolter, “General cutting planes for bound-propagation-based neural network verification,” in Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 20...

    2022

  10. [18]

    Neural network verification with branch-and-bound for general nonlinearities,

    Z. Shi, Q. Jin, Z. Kolter, S. Jana, C. Hsieh, and H. Zhang, “Neural network verification with branch-and-bound for general nonlinearities,” CoRR, vol. abs/2405.21063, 2024

    2024 arXiv

  11. [19]

    Marabou 2.0: A versatile formal analyzer of neural networks,

    H. Wu, O. Isac, A. Zeljic, T. Tagomori, M. L. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, S. Bassan, P. Huang, O. Lahav, M. Wu, M. Zhang, E. Komendantskaya, G. Katz, and C. W. Barrett, “Marabou 2.0: A versatile formal analyzer of neural networks,” in Computer Aided Veri...

    2024

  12. [20]

    JuliaReach: a toolbox for set-based reachability,

    S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: a toolbox for set-based reachability,” in Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019 (N. Oza...

    2019

  13. [21]

    Verification of neural- network control systems by integrating taylor models and zonotopes,

    C. Schilling, M. Forets, and S. Guadalupe, “Verification of neural- network control systems by integrating taylor models and zonotopes,” pp. 8169–8177, 2022

    2022

  14. [22]

    Star-based reachability analysis of deep neural networks,

    H. Tran, D. M. Lopez, P. Musau, X. Yang, L. V . Nguyen, W. Xiang, and T. T. Johnson, “Star-based reachability analysis of deep neural networks,” in Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings (M. H. ter B...

    2019

  15. [23]

    NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems,

    H. Tran, X. Yang, D. M. Lopez, P. Musau, L. V . Nguyen, W. Xiang, S. Bak, and T. T. Johnson, “NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems,” in Computer Aided Verification - 32nd International Conference, CAV 20...

    2020

  16. [24]

    Reachable set estimation for neural network control systems: A simulation-guided approach,

    W. Xiang, H. Tran, X. Yang, and T. T. Johnson, “Reachable set estimation for neural network control systems: A simulation-guided approach,” IEEE Trans. Neural Networks Learn. Syst. , vol. 32, no. 5, pp. 1821–1830, 2021

    2021

  17. [25]

    Verifying the safety of autonomous systems with neural network controllers,

    R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verifying the safety of autonomous systems with neural network controllers,” ACM Trans. Embed. Comput. Syst. , vol. 20, no. 1, pp. 7:1– 7:26, 2021

    2021

  18. [26]

    Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning,

    R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning,” in Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Pr...

    2021

  19. [27]

    ReachNN: Reachability analysis of neural-network controlled systems,

    C. Huang, J. Fan, W. Li, X. Chen, and Q. Zhu, “ReachNN: Reachability analysis of neural-network controlled systems,” ACM Trans. Embed. Comput. Syst., vol. 18, no. 5s, pp. 106:1–106:22, 2019

    2019

  20. [28]

    ReachNN*: A tool for reachability analysis of neural-network controlled systems,

    J. Fan, C. Huang, X. Chen, W. Li, and Q. Zhu, “ReachNN*: A tool for reachability analysis of neural-network controlled systems,” in Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceed- ings ...

    2020

  21. [29]

    Reachability analysis for neural feedback systems using regressive polynomial rule inference,

    S. Dutta, X. Chen, and S. Sankaranarayanan, “Reachability analysis for neural feedback systems using regressive polynomial rule inference,” in Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, Apri...

    2019

  22. [30]

    Formal verification of neural agents in non-deterministic environments,

    M. E. Akintunde, E. Botoeva, P. Kouvaros, and A. Lomuscio, “Formal verification of neural agents in non-deterministic environments,” Auton. Agents Multi Agent Syst. , vol. 36, no. 1, p. 6, 2022

    2022

  23. [31]

    OVERT: an algorithm for safety verification of neural network control policies for nonlinear systems,

    C. Sidrane, A. Maleki, A. Irfan, and M. J. Kochenderfer, “OVERT: an algorithm for safety verification of neural network control policies for nonlinear systems,” Journal of Machine Learning Research , vol. 23, no. 117, pp. 1–45, 2022

    2022

  24. [32]

    Provably safe neural network controllers via differential dynamic logic,

    S. Teuber, S. Mitsch, and A. Platzer, “Provably safe neural network controllers via differential dynamic logic,” in Advances in Neural Infor- mation Processing Systems (A. Globerson, L. Mackey, A. Fan, C. Zhang, D. Belgrave, J. Tomczak, and U. Paquet, eds.), Curran Associates,...

    2024

  25. [33]

    Discrete choice in the presence of numerical uncertainties,

    D. Lohar, E. Darulova, S. Putot, and E. Goubault, “Discrete choice in the presence of numerical uncertainties,” IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., vol. 37, no. 11, pp. 2381–2392, 2018

    2018

  26. [34]

    Compiling kb- sized machine learning models to tiny iot devices,

    S. Gopinath, N. Ghanathe, V . Seshadri, and R. Sharma, “Compiling kb- sized machine learning models to tiny iot devices,” in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019 (K. S. M...

    2019

  27. [35]

    Deep learning with limited numerical precision,

    S. Gupta, A. Agrawal, K. Gopalakrishnan, and P. Narayanan, “Deep learning with limited numerical precision,” in Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 (F. R. Bach and D. M. Blei, eds.), vol. 37 of JMLR Wor...

    2015

  28. [36]

    Scalable verification of quantized neural networks,

    T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized neural networks,” in Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Inno- vative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Sy...

    2021

  29. [37]

    Sound mixed fixed-point quantization of neural networks,

    D. Lohar, C. Jeangoudoux, A. V olkova, and E. Darulova, “Sound mixed fixed-point quantization of neural networks,” ACM Trans. Embed. Comput. Syst., vol. 22, no. 5s, pp. 136:1–136:26, 2023

    2023

  30. [38]

    Towards precision-aware safe neural-controlled cyber-physical systems,

    H. Thevendhriya, S. Ghosh, and D. Lohar, “Towards precision-aware safe neural-controlled cyber-physical systems,” IEEE Embedded Systems Letters (ESL), 2024

    2024

  31. [39]

    Sound mixed-precision optimiza- tion with rewriting,

    E. Darulova, E. Horn, and S. Sharma, “Sound mixed-precision optimiza- tion with rewriting,” in Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2018, Porto, Portugal, April 11-13, 2018 (C. Gill, B. Sinopoli, X. Liu, and P. Tabuada, eds....

    2018

  32. [40]

    Vivado design suite,

    Vivado Lab Solutions, “Vivado design suite,” 2021

    2021

  33. [41]

    Modelplex: verified runtime validation of verified cyber-physical system models,

    S. Mitsch and A. Platzer, “Modelplex: verified runtime validation of verified cyber-physical system models,” Formal Methods Syst. Des. , vol. 49, no. 1-2, pp. 33–74, 2016

    2016

  34. [42]

    Veriphy: verified controller executables from verified cyber-physical system models,

    R. Bohrer, Y . K. Tan, S. Mitsch, M. O. Myreen, and A. Platzer, “Veriphy: verified controller executables from verified cyber-physical system models,” in Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, ...

    2018

  35. [43]

    Differential dynamic logic for hybrid systems,

    A. Platzer, “Differential dynamic logic for hybrid systems,” J. Autom. Reason., vol. 41, no. 2, pp. 143–189, 2008

    2008

  36. [44]

    Differential game logic,

    A. Platzer, “Differential game logic,” ACM Trans. Comput. Log., vol. 17, no. 1, p. 1, 2015

    2015

  37. [45]

    A complete uniform substitution calculus for differential dynamic logic,

    A. Platzer, “A complete uniform substitution calculus for differential dynamic logic,” J. Autom. Reas. , vol. 59, no. 2, pp. 219–265, 2017

    2017

  38. [46]

    Differential equation invariance axiomatiza- tion,

    A. Platzer and Y . K. Tan, “Differential equation invariance axiomatiza- tion,” J. ACM, vol. 67, no. 1, pp. 6:1–6:66, 2020

    2020

  39. [47]

    The complete proof theory of hybrid systems,

    A. Platzer, “The complete proof theory of hybrid systems,” in Pro- ceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, pp. 541–550, {IEEE} Computer Society, 2012

    2012

  40. [48]

    Harel, First-Order Dynamic Logic , vol

    D. Harel, First-Order Dynamic Logic , vol. 68 of LNCS. Heidelberg: Springer, 1979

    1979

  41. [49]

    Harel, D

    D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic. MIT Press, 2000

    2000

  42. [50]

    Platzer, Logical Foundations of Cyber-Physical Systems

    A. Platzer, Logical Foundations of Cyber-Physical Systems . Cham: Springer, 2018

    2018

  43. [51]

    Differential refinement logic,

    S. M. Loos and A. Platzer, “Differential refinement logic,” in LICS (M. Grohe, E. Koskinen, and N. Shankar, eds.), (New York, NY , USA), pp. 505–514, ACM, 2016

    2016

  44. [52]

    Uniform substitution for differential refine- ment logic,

    E. Prebet and A. Platzer, “Uniform substitution for differential refine- ment logic,” in IJCAR (C. Benzmüller, M. J. Heule, and R. A. Schmidt, eds.), vol. 14740 of LNCS, (Cham), pp. 196–215, Springer, 2024

    2024

  45. [53]

    Automatic verification of control system implementations,

    A. A. Martinez, R. Majumdar, I. Saha, and P. Tabuada, “Automatic verification of control system implementations,” in Proceedings of the 10th International conference on Embedded software, EMSOFT 2010, Scottsdale, Arizona, USA, October 24-29, 2010 (L. P. Carloni and S. Tripakis...

    2010

  46. [54]

    Rigorous floating-point mixed-precision tuning,

    W. Chiang, M. Baranowski, I. Briggs, A. Solovyev, G. Gopalakrishnan, and Z. Rakamaric, “Rigorous floating-point mixed-precision tuning,” pp. 300–315, 2017

    2017

  47. [55]

    Mixed precision tuning with salsa,

    N. Damouche and M. Martel, “Mixed precision tuning with salsa,” pp. 185–194, 2018

    2018

  48. [56]

    Fixed- point code synthesis based on constraint generation,

    S. Bessaï, D. Ben Khalifa, H. Benmaghnia, and M. Martel, “Fixed- point code synthesis based on constraint generation,” in Design and Architecture for Signal and Image Processing - 15th International Work- shop, DASIP 2022, Budapest, Hungary, June 20-22, 2022, Proceedings (K. D...

    2022

  49. [57]

    Yesterday, my program worked. today, it does not. why?,

    A. Zeller, “Yesterday, my program worked. today, it does not. why?,” in Software Engineering - ESEC/FSE’99, 7th European Software Engineer- ing Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1...

    1999

  50. [58]

    Z3: an efficient SMT solver,

    L. M. de Moura and N. S. Bjørner, “Z3: an efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Buda...

    2008

  51. [59]

    Arithmetic solving in Z3,

    N. S. Bjørner and L. Nachmanson, “Arithmetic solving in Z3,” in Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I (A. Gurfinkel and V . Ganesh, eds.), vol. 14681 ofLNCS, (Cham), pp. 26– 41, Springer, 2024

    2024

  52. [60]

    Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description),

    G. Kremer, A. Reynolds, C. W. Barrett, and C. Tinelli, “Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description),” in Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Procee...

    2022

  53. [61]

    Mathematica, Version 14.1

    W. R. Inc., “Mathematica, Version 14.1.” Champaign, IL, 2024

    2024

  54. [62]

    Critically assessing the state of the art in neural network verification,

    M. König, A. W. Bosman, H. H. Hoos, and J. N. van Rijn, “Critically assessing the state of the art in neural network verification,” J. Mach. Learn. Res., vol. 25, pp. 12:1–12:53, 2024

    2024

  55. [63]

    First three years of the international verification of neural networks competition (VNN-COMP),

    C. Brix, M. N. Müller, S. Bak, T. T. Johnson, and C. Liu, “First three years of the international verification of neural networks competition (VNN-COMP),” Int. J. Softw. Tools Technol. Transf. , vol. 25, no. 3, pp. 329–339, 2023

    2023

  56. [64]

    The fifth international veri- fication of neural networks competition (VNN-COMP 2024): Summary and results,

    C. Brix, S. Bak, T. T. Johnson, and H. Wu, “The fifth international veri- fication of neural networks competition (VNN-COMP 2024): Summary and results,” CoRR, vol. abs/2412.19985, 2024

    2024 arXiv

  57. [65]

    A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system,

    J. Jeannin, K. Ghorbal, Y . Kouskoulas, A. C. Schmidt, R. W. Gardner, S. Mitsch, and A. Platzer, “A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system,” Int. J. Softw. Tools Technol. Transf., vol. 19, no. 6, pp. 717–741, 2017

    2017

  58. [66]

    A formally verified plasma vertical position control algorithm,

    M. Wu, J. C. Rosenberg, and N. Fulton, “A formally verified plasma vertical position control algorithm,” in Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings (M. H. ter Beek and D. Nick...

    2020

  59. [67]

    Formal development of safe automated driving using differential dynamic logic,

    Y . Selvaraj, W. Ahrendt, and M. Fabian, “Formal development of safe automated driving using differential dynamic logic,” IEEE Trans. Intell. Veh., vol. 8, no. 1, pp. 988–1000, 2023

    2023

  60. [68]

    The image computation problem in hybrid systems model checking,

    A. Platzer and E. M. Clarke, “The image computation problem in hybrid systems model checking,” in Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3-5, 2007, Proceedings (A. Bemporad, A. Bicchi, and G. C. Buttazzo, eds.), vol....

    2007

  61. [69]

    KeYmaera X: an axiomatic tactical theorem prover for hybrid systems,

    N. Fulton, S. Mitsch, J. Quesel, M. Völp, and A. Platzer, “KeYmaera X: an axiomatic tactical theorem prover for hybrid systems,” in Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (A. P. Felty...

    2015

  62. [70]

    Verified train controllers for the federal railroad administration train kinematics model: Balancing competing brake and track forces,

    A. Kabra, S. Mitsch, and A. Platzer, “Verified train controllers for the federal railroad administration train kinematics model: Balancing competing brake and track forces,” IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., vol. 41, no. 11, pp. 4409–4420, 2022

    2022

  63. [71]

    European train control system: A case study in formal verification,

    A. Platzer and J. Quesel, “European train control system: A case study in formal verification,” in Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings (K. K. ...

    2009

  64. [72]

    A formal safety net for waypoint-following in ground robots,

    R. Bohrer, Y . K. Tan, S. Mitsch, A. Sogokon, and A. Platzer, “A formal safety net for waypoint-following in ground robots,” IEEE Robotics Autom. Lett., vol. 4, no. 3, pp. 2910–2917, 2019

    2019

  65. [73]

    Verification of autonomous neural car control with KeYmaera X,

    E. Prebet, S. Teuber, and A. Platzer, “Verification of autonomous neural car control with KeYmaera X,” in Rigorous State-Based Methods - 11th International Conference, ABZ 2025, Düsseldorf, Germany, Proceedings (M. Leuschel and F. Ishikawa, eds.), vol. 15728 ofLNCS, Springer, 2025

    2025

  66. [74]

    CESAR: control enve- lope synthesis via angelic refinements,

    A. Kabra, J. Laurent, S. Mitsch, and A. Platzer, “CESAR: control enve- lope synthesis via angelic refinements,” in Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on T...

    2024

  67. [75]

    samysweb/NCubeV: v0.9,

    S. Teuber, S. Mitsch, and A. Platzer, “samysweb/NCubeV: v0.9,” Oct. 2024

    2024

  68. [76]

    PicoSAT essentials,

    A. Biere, “PicoSAT essentials,” J. Satisf. Boolean Model. Comput. , vol. 4, no. 2-4, pp. 75–97, 2008

    2008

  69. [77]

    Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance,

    J. E. Holland, M. J. Kochenderfer, and W. A. Olson, “Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance,” Air Traffic Control Quarterly , vol. 21, no. 3, pp. 275–297, 2013

    2013

  70. [78]

    Next generation airborne collision avoidance system,

    M. J. Kochenderfer, J. E. Holland, and J. P. Chryssanthacopoulos, “Next generation airborne collision avoidance system,” Lincoln Laboratory Journal, vol. 19, no. 1, pp. 17–33, 2012

    2012

  71. [79]

    POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems,

    C. Huang, J. Fan, X. Chen, W. Li, and Q. Zhu, “POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems,” in Automated Technology for Verification and Analysis - 20th Inter- national Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proc...

    2022

  72. [80]

    Generation of Lyapunov functions by neural networks,

    N. Noroozi, P. Karimaghaee, F. Safaei, and H. Javadi, “Generation of Lyapunov functions by neural networks,” in Proceedings of the World Congress on Engineering , vol. 2008, 2008

    2008

  73. [81]

    The Lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems,

    S. M. Richards, F. Berkenkamp, and A. Krause, “The Lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems,” in 2nd Annual Conference on Robot Learning, CoRL 2018, Zürich, Switzerland, 29-31 October 2018, Proceedings , vol. 87 of Procee...

    2018

  74. [82]

    Automated and formal syn- thesis of neural barrier certificates for dynamical models,

    A. Peruffo, D. Ahmed, and A. Abate, “Automated and formal syn- thesis of neural barrier certificates for dynamical models,” in Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conf...

    2021

  75. [83]

    Formal synthesis of Lyapunov neural networks,

    A. Abate, D. Ahmed, M. Giacobbe, and A. Peruffo, “Formal synthesis of Lyapunov neural networks,” IEEE Control. Syst. Lett. , vol. 5, no. 3, pp. 773–778, 2021

    2021

  76. [84]

    FOSSIL: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks,

    A. Abate, D. Ahmed, A. Edwards, M. Giacobbe, and A. Peruffo, “FOSSIL: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks,” in HSCC ’21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nash...

    2021

  77. [85]

    Approximate conformance checking for closed-loop systems with neural network controllers,

    P. Habeeb, L. Gupta, and P. Prabhakar, “Approximate conformance checking for closed-loop systems with neural network controllers,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 43, no. 11, pp. 4322–4333, 2024

    2024

  78. [86]

    Verifying equivalence properties of neural networks with relu activation functions,

    M. K. Büning, P. Kern, and C. Sinz, “Verifying equivalence properties of neural networks with relu activation functions,” in Principles and Prac- tice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedin...

    2020

  79. [87]

    Reludiff: Differential verification of deep neural networks,

    B. Paulsen, J. Wang, and C. Wang, “Reludiff: Differential verification of deep neural networks,” Proceedings - International Conference on Software Engineering , pp. 714–726, 2020. arXiv: 2001.03662 ISBN: 9781450371216

    2020 arXiv

  80. [88]

    QVIP: an ilp-based formal verification approach for quantized neural networks,

    Y . Zhang, Z. Zhao, G. Chen, F. Song, M. Zhang, T. Chen, and J. Sun, “QVIP: an ilp-based formal verification approach for quantized neural networks,” in 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022,...

    2022

  81. [89]

    Towards efficient verification of quantized neural networks,

    P. Huang, H. Wu, Y . Yang, I. Daukantas, M. Wu, Y . Zhang, and C. W. Barrett, “Towards efficient verification of quantized neural networks,” in Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial...

    2024

  82. [90]

    Fast and efficient bit-level precision tuning,

    A. Adjé, D. Ben Khalifa, and M. Martel, “Fast and efficient bit-level precision tuning,” in Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings (C. Dragoi, S. Mukherjee, and K. S. Namjoshi, eds.), vol. 12913 of LNCS, (Ch...

    2021

  83. [91]

    Shiftry: RNN inference in 2KB of RAM,

    A. Kumar, V . Seshadri, and R. Sharma, “Shiftry: RNN inference in 2KB of RAM,” Proc. ACM Program. Lang., vol. 4, no. OOPSLA, pp. 182:1– 182:30, 2020

    2020

  84. [92]

    Energy-efficient neural network ac- celerator based on outlier-aware low-precision computation,

    E. Park, D. Kim, and S. Yoo, “Energy-efficient neural network ac- celerator based on outlier-aware low-precision computation,” in 45th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2018, Los Angeles, CA, USA, June 1-6, 2018 (M. Annavaram, T. M. Pinksto...

    2018

  85. [93]

    Bit fusion: Bit-level dynamically composable archi- tecture for accelerating deep neural network,

    H. Sharma, J. Park, N. Suda, L. Lai, B. Chau, V . Chandra, and H. Esmaeilzadeh, “Bit fusion: Bit-level dynamically composable archi- tecture for accelerating deep neural network,” in 45th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2018, Los Angeles,...

    2018

  86. [94]

    DRQ: dynamic region-based quantization for deep neural network acceleration,

    Z. Song, B. Fu, F. Wu, Z. Jiang, L. Jiang, N. Jing, and X. Liang, “DRQ: dynamic region-based quantization for deep neural network acceleration,” in 47th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2020, Virtual Event / Valencia, Spain, May 30 - June ...

    2020

  87. [95]

    Rigorous floating-point to fixed-point quantization of deep neural networks on STM32 micro-controllers,

    D. B. Khalifa and M. Martel, “Rigorous floating-point to fixed-point quantization of deep neural networks on STM32 micro-controllers,” in 2024 10th International Conference on Control, Decision and Informa- tion Technologies (CoDIT), pp. 1201–1206, 2024

    2024

  88. [96]

    Reflections on 10 years of flopoco,

    F. de Dinechin, “Reflections on 10 years of flopoco,” in 26th IEEE Symposium on Computer Arithmetic, ARITH 2019, Kyoto, Japan, June 10-12, 2019 (N. Takagi, S. Boldo, and M. Langhammer, eds.), pp. 187– 189, IEEE, 2019. APPENDIX dL MODEL OF THE RUNNING EXAMPLE The robot’s physic...

    2019

Pith tools

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