pith. machine review for the scientific record. sign in

arxiv: 2605.02790 · v2 · submitted 2026-05-04 · 💻 cs.PL

Recognition: unknown

Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice

Matthew L. Daggitt , Ekaterina Komendantskaya , Alistair Sirman , Alessandro Bruni , Samuel Teuber , Josh Smart , Grant Passmore
Authors on Pith no claims yet

Pith reviewed 2026-05-08 01:30 UTC · model grok-4.3

classification 💻 cs.PL
keywords compositional verificationneural networkscyber-physical systemsinteractive theorem proversVehicle frameworkinfinite time-horizon safetyneuro-symbolic systemsformal verification
0
0 comments X

The pith

A compositional framework lets neural specifications be verified inside any chosen interactive theorem prover.

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

The paper establishes a method to build complete safety proofs for neuro-symbolic cyber-physical systems by linking neural network properties to symbolic models of discrete and continuous dynamics inside interactive theorem provers. Vehicle supplies a functional language for specifying and training the neural parts; its type checker is reused to convert those specifications into an intermediate form that multiple provers can accept with little extra work. A sympathetic reader would care because the approach removes the usual manual bridge between neural training tools and formal proofs, making infinite-horizon guarantees feasible for systems such as drones and medical devices while keeping the final model deployable.

Core claim

We present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort by reusing its bidirectional type checker to transpile neural specifications into an intermediate representation targeting multiple theorem provers. We integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra, and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, we use the Mathematical Components libraries 0

What carries the argument

Vehicle's functional interface and bidirectional type checker, which transpiles neural specifications into an intermediate representation usable by multiple interactive theorem provers.

If this is right

  • Infinite time-horizon safety proofs become possible for both discrete and continuous neuro-cyber-physical systems inside general-purpose ITPs.
  • The same neural specification can be reused across Rocq, Isabelle/HOL, Agda and Imandra with only prover-specific proof scripts added.
  • Existing mathematical libraries in the chosen ITP can be applied directly to the non-neural parts of the system.
  • The resulting verified model remains deployable because the neural component is left unchanged after training.

Where Pith is reading between the lines

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

  • The same transpilation step could be used to connect Vehicle to additional provers or to hybrid tools that combine multiple ITPs for different subsystems.
  • Training pipelines could be extended so that safety constraints written in Vehicle directly influence the optimization step before any ITP proof is attempted.
  • The approach suggests a route for verifying larger hybrid systems where some components are best handled in one prover and others in another.
  • A direct test would be to apply the existing transpiler to a new ITP not shown in the paper and measure the size of the generated interface.

Load-bearing premise

The bidirectional type checker must correctly preserve the semantics of the neural specifications during transpilation, and the target ITP libraries must suffice for the continuous dynamics without additional gaps.

What would settle it

A concrete neural specification whose transpiled form produces an ITP proof that fails to match the original network's verified behavior on some input sequence, or a continuous medical-device model whose safety claim cannot be completed inside Rocq despite using the Mathematical Components library.

Figures

Figures reproduced from arXiv: 2605.02790 by Alessandro Bruni, Alistair Sirman, Ekaterina Komendantskaya, Grant Passmore, Josh Smart, Matthew L. Daggitt, Samuel Teuber.

Figure 1
Figure 1. Figure 1: Our running example of NCPS: A model of an au view at source ↗
Figure 2
Figure 2. Figure 2: The architecture of a compositional proof for a neural-cyber-physical system, with specifications in the view at source ↗
Figure 3
Figure 3. Figure 3: The internal architecture of Vehicle and the structure of this paper. Although the dynamics of the system is better modelled continuously (e.g. using ODEs), for simplicity we will model the cyber and physical components discretely using the following functions: nextState : Observation → State → State nextState o s = State newWindSpeed newPosition newVelocity newSensor where newWindSpeed = windSpeed s + win… view at source ↗
Figure 4
Figure 4. Figure 4: Grammar for the Surface language of the Vehicle DSL presented in [23]. Listing 1 The Vehicle specification for the car’s neural network controller. type InputVector = Tensor Real [2]; sensor1 = 0; sensor2 = 1 type OutputVector = Tensor Real [1]; velocity = 0 @network controller : InputVector -> OutputVector safeInput : InputVector -> Bool safeInput x = -3.25 <= x ! sensor1 <= 3.25 and -3.25 <= x ! sensor2 … view at source ↗
Figure 5
Figure 5. Figure 5: The standard dependent-type system for the core view at source ↗
Figure 6
Figure 6. Figure 6: A Vehicle specification where Boolean expressions must be specialised before compiling to the ITP. 4 ITP Intermediate Language As a source language for compiling to ITP code, Spec StandardBuiltin is less than ideal. When translating a specifi￾cation to a dependently-typed ITP such as Agda, Rocq or Lean, for each Boolean subexpression we must decide whether to lift it to a proposition or whether it can rema… view at source ↗
Figure 7
Figure 7. Figure 7: MathComp Analysis definitions of multivariate derivative, differentiation and continuity and their mathematical counterparts. view at source ↗
Figure 8
Figure 8. Figure 8: The Rocq definition for the state and the iterative function (similar to view at source ↗
Figure 9
Figure 9. Figure 9: A graph showing how the concentrations are interpreted by view at source ↗
Figure 11
Figure 11. Figure 11: The function for the total concentration at time view at source ↗
read the original abstract

Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the "cyber" and "physical" behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model. In this paper we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort. First, we describe how Vehicle's standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle's functional interface.

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

1 major / 2 minor

Summary. The paper presents a compositional methodology for verifying neuro-symbolic cyber-physical systems. It extends the Vehicle framework's functional DSL (for specifying, training, and verifying neural components) to integrate with arbitrary interactive theorem provers by reusing its bidirectional type checker to transpile neural specifications into an intermediate representation. Concrete integrations are shown with Rocq, Isabelle/HOL, Agda, and Imandra; generic infinite-horizon safety proofs for discrete CPS with neural controllers are given in each; and a continuous medical-device case study (using Mathematical Components) yields the first such infinite-horizon safety result in a general-purpose ITP.

Significance. If the integrations hold, the result is significant: it demonstrates that Vehicle's compositionality enables the first general-purpose-ITP treatment of infinite-horizon continuous CPS safety, combining neural verification with mature ITP libraries for discrete/continuous dynamics. The explicit multi-prover examples and the medical-device case study provide concrete evidence of practicality and are strengths that should be highlighted.

major comments (1)
  1. [§3] §3 (Transpilation via bidirectional type checker): The central claim that neural specifications are faithfully encoded in target ITP statements rests on reusing the existing bidirectional type checker to produce the IR, yet the manuscript supplies no separate semantics, equivalence theorem, or counterexample validation showing that activation functions, neural constraints, and safety predicates preserve their original training/verification meaning. Any mismatch would invalidate both the discrete multi-ITP proofs and the continuous Rocq/MathComp result.
minor comments (2)
  1. [Abstract] The abstract and introduction could more explicitly state the precise scope of the semantic-preservation assumption (e.g., which fragments of Vehicle are covered by the transpiler).
  2. [§5] Figure captions for the medical-device case study should clarify which parts of the continuous dynamics are handled by MathComp versus the transpiled neural obligations.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for recognising the significance of the multi-prover integrations and the continuous medical-device case study. We address the single major comment below.

read point-by-point responses

  1. Referee: [§3] §3 (Transpilation via bidirectional type checker): The central claim that neural specifications are faithfully encoded in target ITP statements rests on reusing the existing bidirectional type checker to produce the IR, yet the manuscript supplies no separate semantics, equivalence theorem, or counterexample validation showing that activation functions, neural constraints, and safety predicates preserve their original training/verification meaning. Any mismatch would invalidate both the discrete multi-ITP proofs and the continuous Rocq/MathComp result.

    Authors: The Vehicle bidirectional type checker was already validated in prior work for preserving the semantics of neural specifications (activation functions, constraints, and predicates) when producing the IR; the current paper reuses that mechanism without modification. The IR itself is a direct, structure-preserving embedding of the typed functional expressions into the target logic, mapping standard operations (ReLU, sigmoid, etc.) to their mathematical counterparts. The successful infinite-horizon proofs in four distinct ITPs, including the first continuous case in Rocq/MathComp, provide concrete validation that no mismatch occurred. To make the preservation argument fully explicit, we will add a short subsection in §3 describing the correspondence and include a small worked example of a neural constraint translated to one target ITP. revision: partial

Circularity Check

0 steps flagged

No significant circularity in the compositional ITP integration methodology

full rationale

The paper describes an extension of the Vehicle framework to support integration with multiple ITPs (Rocq, Isabelle/HOL, Agda, Imandra) via reuse of its existing bidirectional type checker for transpilation to an IR, followed by explicit showcase proofs including the first infinite-horizon continuous safety result in Rocq/MathComp. No equations, fitted parameters, or derived predictions appear in the provided text that reduce by construction to prior inputs. The central claims rest on new tooling descriptions, library integrations, and case studies rather than self-referential definitions or load-bearing self-citations that would force the result. The methodology is presented as self-contained through the functional interface and explicit integrations, with no reduction of the verification outcomes to unverified prior quantities by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The framework relies on standard mathematical libraries already present in the target ITPs and introduces no new fitted parameters or postulated entities; the only background assumptions are the soundness of the existing theorem provers and their continuous-math libraries.

axioms (1)
  • standard math Standard axioms and libraries for real numbers and continuous dynamics in Rocq's Mathematical Components
    Invoked for the continuous medical-device case; these are pre-existing in the ITP ecosystem rather than introduced by the paper.

pith-pipeline@v0.9.0 · 5634 in / 1226 out tokens · 52890 ms · 2026-05-08T01:30:06.876409+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

84 extracted references · 61 canonical work pages

  1. [1]

    Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. 2021. Formal Synthesis of Lyapunov Neural Networks.IEEE Control. Syst. Lett.5, 3 (2021), 773–778. doi:10.1109/LCSYS.2020.3005328

    work page doi:10.1109/lcsys.2020.3005328 2021

  2. [2]

    2026.MathComp-Analysis: Mathematical Components compliant analysis library

    Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Théry. 2026.MathComp-Analysis: Mathematical Components compliant analysis library. https: //github.com/math-comp/analysis original-date: 2017-11-29T12:17:44Z

    2026

  3. [3]

    Aws Albarghouthi. 2021. Introduction to Neural Network Verification.Found. Trends Program. Lang.7, 1-2 (2021), 1–157. doi:10.1561/2500000051

    work page doi:10.1561/2500000051 2021

  4. [4]

    Michele Alberti, François Bobot, Julien Girard-Satabin, Alban Grastien, Aymeric Varasse, and Zakaria Chihani. 2025. The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification. InIntegrated Formal Methods - 20th International Conference, iFM 2025, Paris, France, November 19-21, 2025, Proceedings (LNCS, Vol. 16194), Ferrucci...

    work page doi:10.1007/978-3-032-10794-7_15 2025

  5. [5]

    Matthias Althoff. 2015. An Introduction to CORA 2015. InProc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems. EasyChair, 120–151. doi:10.29007/zbkv Manuscript submitted to ACM Compositional Neural-Cyber-Physical System Verification in the ITP of Your Choice 27

    work page doi:10.29007/zbkv 2015

  6. [6]

    PyTorch 2: Faster Ma- chine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation

    Jason Ansel, Edward Z. Yang, Horace He, Natalia Gimelshein, Animesh Jain, Michael Voznesensky, Bin Bao, Peter Bell, et al . 2024. PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Sy...

    work page doi:10.1145/3620665.3640366 2024

  7. [7]

    Anonymous authors. 2026. Tensor formalization #1535. GitHub Pull Request. Mathematical Components library

    2026

  8. [8]

    Edoardo Bacci, Mirco Giacobbe, and David Parker. 2021. Verifying Reinforcement Learning up to Infinity. InProceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, Zhi-Hua Zhou (Ed.). ijcai.org, 2154–2160. doi:10.24963/IJCAI.2021/297

    work page doi:10.24963/ijcai.2021/297 2021

  9. [9]

    Alexander Bagnall and Gordon Stewart. 2019. Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. InThe Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019. AAAI Press, 2662–2669. doi:10.1609/AAAI.V33I01.33012662

    work page doi:10.1609/aaai.v33i01.33012662 2019

  10. [10]

    Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor T. Johnson. 2020. Improved Geometric Path Enumeration for Verifying ReLU Neural Networks. InComputer Aided Verification - 32nd International Conference, CA V 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I (LNCS, Vol. 12224), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, Cham,...

    work page doi:10.1007/978-3-030-53288-8_4 2020

  11. [11]

    Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, and Clark W. Barrett. 2023. An Interactive SMT Tactic in Coq using Abductive Reasoning. InLPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023 (EPiC Series in Computing...

    work page doi:10.29007/432m 2023

  12. [12]

    Alexander Bentkamp. 2016. Expressiveness of Deep Learning.Archive of Formal Proofs(November 2016). https://isa-afp.org/entries/Deep_Learning. html, Formal proof development

    2016

  13. [13]

    Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. 2019. JuliaReach: a toolbox for set-based reachability. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, Necmiye Ozay and Pavithra Prabhakar (Eds.). ACM, New Yor...

    work page doi:10.1145/3302504.3311804 2019

  14. [14]

    Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. 2017. Formally verified differential dynamic logic. InProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, New York, NY, USA, 208–221. doi:10.1145/3018610.3018616

    work page doi:10.1145/3018610.3018616 2017

  15. [15]

    Robert S Boyer, Milton W Green, and J Strother Moore. 1990. The use of a formal simulator to verify a simple real time control program. InBeauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer, Berlin, Heidelberg, 54–66

    1990

  16. [16]

    Brucker and Amy Stell

    Achim D. Brucker and Amy Stell. 2023. Verifying Feedforward Neural Networks for Classification in Isabelle/HOL. InFormal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings (LNCS, Vol. 14000), Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer, Cham, Switzerland, 427–444. doi:10.1007/978-3-...

    work page doi:10.1007/978-3-031-27481-7_24 2023

  17. [17]

    Ya-Chien Chang, Nima Roohi, and Sicun Gao. 2019. Neural Lyapunov Control. InAdvances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garn...

    2019

  18. [18]

    Cyril Cohen, Pierre Roux, Enrico Tassi, Kazuhiko Sakaguchi, Reynald Affeldt, Laurent Théry, Erik Martin-Dorel, Georges Gonthier, et al. 2024. math-comp/math-comp: The Mathematical Components Library 2.3.0. doi:10.5281/zenodo.14237175

    work page doi:10.5281/zenodo.14237175 2024

  19. [19]

    and Daggitt, Matthew L

    Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Sinkarovs, and Haoze Wu. 2025. Neural Network Verification is a Programming Language Challenge. InProgramming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Ha...

    work page doi:10.1007/978-3-031-91118-7_9 2025

  20. [20]

    Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Nathan Van Doorn, James Wood, Ulf Norell, Donnacha Oisín Kidney, et al

    Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Nathan Van Doorn, James Wood, Ulf Norell, Donnacha Oisín Kidney, et al

  21. [21]

    Journal of Open Source Software10(116), 9241 (2025).https://doi

    The Agda Standard Library: Version 2.0.Journal of Open Source Software10, 116 (Dec. 2025), 9241. doi:10.21105/joss.09241

    work page doi:10.21105/joss.09241 2025

  22. [22]

    Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi

    Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi. 2023. Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, Robbert Krebbers, ...

    work page doi:10.1145/3573105.3575674 2023

  23. [23]

    2024 , month = jan, publisher =

    Matthew L. Daggitt, Wen Kokke, and Robert Atkey. 2024. Efficient compilation of expressive problem space specifications to neural network solvers. CoRRabs/2402.01353 (2024). arXiv:2402.01353 doi:10.48550/ARXIV.2402.01353

    work page doi:10.48550/arxiv.2402.01353 2024

  24. [24]

    LIPIcs, Volume 337, FSCD 2025 337 (2025), 2:1–2:20

    Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. 2025. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, Birmingham, UK, July 14-20, 2025 (LIPIcs, Vol. 33...

    work page doi:10.4230/lipics.fscd.2025.2 2025

  25. [25]

    Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. 2021. Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions. In Conference on Robot Learning, 8-11 November 2021, London, UK (Proceedings of Machine Learning Research, Vol. 164), Aleksandra Faust, David Hsu, and Gerhard Neumann (Eds.). PMLR, 1724–1735. https://proceedings.mlr.press/v16...

    2021

  26. [26]

    Leonardo Mendonça de Moura and Grant Olney Passmore. 2013. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. InAutomated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings (LNCS, Vol. 7898), Maria Paola Bonacina (Ed.). Springer, Berlin, Heide...

    work page doi:10.1007/978-3-642-38574-2_12 2013

  27. [27]

    Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz

    Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz. 2025. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025 (LIPIcs, Vol. 352), Yannick Forster and Chantal Ke...

    work page doi:10.4230/lipics.itp.2025.1 2025

  28. [28]

    Passmore, Ekaterina Komendantskaya, and Matthew L

    Remi Desmartin, Grant O. Passmore, Ekaterina Komendantskaya, and Matthew L. Daggitt. 2022. CheckINN: Wide Range Neural Network Verification in Imandra. InPPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22,

    2022

  29. [29]

    doi:10.1145/3551357.3551372

    ACM, New York, NY, USA, 3:1–3:14. doi:10.1145/3551357.3551372

    work page doi:10.1145/3551357.3551372

  30. [30]

    Kees Dullemond and Kasper Peeters. 1991. Introduction to tensor calculus.Kees Dullemond and Kasper Peeters(1991), 42–44

    1991

  31. [31]

    Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. InComputer Aided Verification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (LNCS, Vol. 10427), Rupak Majumdar and Viktor Kuncak...

    work page doi:10.1007/978-3-319-63390-9_7 2017

  32. [32]

    Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin T. Vechev. 2019. DL2: Training and Querying Neural Networks with Logic. InProceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97), Kamalika Chaudhuri...

    2019

  33. [33]

    Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, and Georg Struth. 2021. Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. InFormal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings (LNCS, Vol. 13047), Marieke Huisman, Corina S. Pasareanu, and Naijun...

    work page doi:10.1007/978-3-030- 2021

  34. [34]

    2025.Proceedings of 12th Int

    Goran Frehse and Matthias Althoff (Eds.). 2025.Proceedings of 12th Int. Workshop on Applied Verification for Continuous and Hybrid Systems. EPiC Series in Computing, Vol. 108. EasyChair

    2025

  35. [35]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. InAutomated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (LNCS, Vol. 9195), Amy P. Felty and Aart Middeldorp (Eds.). Springe...

    work page doi:10.1007/978-3-319-21401-6_36 2015

  36. [36]

    Herman Geuvers, Adam Koprowski, Dan Synek, and Eelis van der Weegen. 2010. Automated Machine-Checked Hybrid System Safety Proofs. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (LNCS, Vol. 6172), Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, Berlin, Heidelberg, 259–274. doi:...

    work page doi:10.1007/978-3-642-14052-5_19 2010

  37. [37]

    Johannes Hölzl, Fabian Immler, and Brian Huffman. 2013. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. InInteractive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (LNCS, Vol. 7998), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin, Heidelbe...

    work page doi:10.1007/978-3-642-39634-2_21 2013

  38. [38]

    Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. 2022. POLAR: A Polynomial Arithmetic Framework for Verifying Neural- Network Controlled Systems. InAutomated Technology for Verification and Analysis - 20th International Symposium, ATV A 2022, Virtual Event, October 25-28, 2022, Proceedings (LNCS, Vol. 13505), Ahmed Bouajjani, Lukás Holík, and Zh...

    work page doi:10.1007/978-3-031-19992-9_27 2022

  39. [39]

    Barrett, Min Zhang, and Guy Katz

    Omri Isac, Clark W. Barrett, Min Zhang, and Guy Katz. 2022. Neural Network Verification with Proof Production. In22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, Alberto Griggio and Neha Rungta (Eds.). IEEE, Piscataway, NJ, USA, 38–48. doi:10.34727/2022/ISBN.978-3-85448-053-2_9

    work page doi:10.34727/2022/isbn.978-3-85448-053-2_9 2022

  40. [40]

    Carpenter, James Weimer, Rajeev Alur, George J

    Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2021. Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning. InComputer Aided Verification - 33rd International Conference, CA V 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I (LNCS, Vol. 12759), Alexandra Silv...

    work page doi:10.1007/978-3-030-81685-8_11 2021

  41. [41]

    2003.Qualified types: theory and practice

    Mark P Jones. 2003.Qualified types: theory and practice. Number 9. Cambridge University Press, Cambridge, UK

    2003

  42. [42]

    Deep Neural Network Compression for Aircraft Collision Avoidance Systems

    Kyle D. Julian, Mykel J. Kochenderfer, and Michael P. Owen. 2019. Deep Neural Network Compression for Aircraft Collision Avoidance Systems. Journal of Guidance, Control, and Dynamics42, 3 (2019), 598–608. doi:10.2514/1.G003724

    work page doi:10.2514/1.g003724 2019

  43. [43]

    and Julian, Kyle and Kochenderfer, Mykel J

    Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. InComputer Aided Verification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I (LNCS, Vol. 10426), Rupak Majumdar and Viktor Kuncak (Eds.). Spri...

    work page doi:10.1007/978-3-319-63387-9_5 2017

  44. [44]

    Colin Kessler, Ekaterina Komendantskaya, Marco Casadio, Ignazio Maria Viola, Thomas Flinkow, Albaraa Ammar Othman, Alistair Malhotra, and Robbie McPherson. 2025. Neural Network Verification for Gliding Drone Control: A Case Study. InAI Verification - Second International Symposium, SAIV 2025, Zagreb, Croatia, July 21-22, 2025, Proceedings (LNCS, Vol. 1594...

    work page doi:10.1007/978-3-031-99991-8_9 2025

  45. [45]

    Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, and David Aspinall. 2020. Neural Networks, Secure by Construction - An Exploration of Refinement Types. InProgramming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings (LNCS, Vol. 12470), Bruno C. d. S. Oliveira (Ed.). Spr...

    work page doi:10.1007/978-3-030-64437-6_4 2020

  46. [46]

    Barrett, and Cesare Tinelli

    Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, and Cesare Tinelli. 2025. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025 (LIPIcs...

    work page doi:10.4230/lipics.itp.2025.26 2025

  47. [47]

    In: Clarke, E.M., Voronkov, A

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (LNCS, Vol. 6355), Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, Berlin, Heidelberg, 348–...

    work page doi:10.1007/978-3-642-17511-4_20 2010

  48. [48]

    Andres Löh, Conor McBride, and Wouter Swierstra. 2010. A Tutorial Implementation of a Dependently Typed Lambda Calculus.Fundam. Informaticae 102, 2 (2010), 177–207. doi:10.3233/FI-2010-304

    work page doi:10.3233/fi-2010-304 2010

  49. [49]

    Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. Johnson. 2023. NNV 2.0: The Neural Network Verification Tool. In Computer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proceedings, Part II (LNCS, Vol. 13965), Constantin Enea and Akash Lal (Eds.). Springer, Cham, Switzerland, 397–412. do...

    work page doi:10.1007/978-3-031-37703-7_19 2023

  50. [50]

    Diego Manzanas Lopez, Patrick Musau, Hoang-Dung Tran, and Taylor T. Johnson. 2019. Verification of Closed-loop Systems with Neural Network Controllers. InARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada, April 15, 2019 (EPiC Series in Computing, Vol. 61), Goran Fr...

    work page doi:10.29007/btv1 2019

  51. [51]

    Carpenter, Radoslav Ivanov, and Taylor T

    Diego Manzanas Lopez, Patrick Musau, Hoang-Dung Tran, Souradeep Dutta, Taylor J. Carpenter, Radoslav Ivanov, and Taylor T. Johnson. 2019. ARCH-COMP19 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. InARCH19. 6th International Workshop on Applied Verification of Continuous and H...

    work page doi:10.29007/rgv8 2019

  52. [52]

    Lopez-Miguel, Borja Fernández Adiego, Faiq Ghawash, and Enrique Blanco Viñuela

    Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Faiq Ghawash, and Enrique Blanco Viñuela. 2023. Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN. InEngineering Applications of Neural Networks - 24th International Conference, EAAAI/EANN 2023, León, Spain, June 14-17, 2023, Proceedings (Communications in Computer ...

    work page doi:10.1007/978-3-031-34204-2_35 2023

  53. [53]

    Érik Martin-Dorel and Guillaume Melquiond. 2016. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq.J. Autom. Reason.57, 3 (2016), 187–217. doi:10.1007/S10817-015-9350-4

    work page doi:10.1007/s10817-015-9350-4 2016

  54. [54]

    The mathlib Community. 2020. The lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, New York, NY, USA, 367–381. doi:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  55. [55]

    Garrett Morris and Mark P

    J. Garrett Morris and Mark P. Jones. 2010. Instance chains: type class programming without overlapping instances. InProceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, Paul Hudak and Stephanie Weirich (Eds.). ACM, New York, NY, USA, 375–386. doi:10.1145/1863543.1863596

    work page doi:10.1145/1863543.1863596 2010

  56. [56]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002.Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer, Berlin, Heidelberg. doi:10.1007/3-540-45949-9

    work page doi:10.1007/3-540-45949-9 2002

  57. [57]

    Ulf Norell. 2009. Dependently typed programming in Agda. InProceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, Andrew Kennedy and Amal Ahmed (Eds.). ACM, New York, NY, USA, 1–2. doi:10.1145/1481861.1481862

    work page doi:10.1145/1481861.1481862 2009

  58. [58]

    Samir Ouchani, Khaled Khebbeb, and Meriem Hafsi. 2020. Towards Enhancing Security and Resilience in CPS: A Coq-Maude based Approach. In 17th IEEE/ACS International Conference on Computer Systems and Applications, AICCSA 2020, Antalya, Turkey, November 2-5, 2020. IEEE, Piscataway, NJ, USA, 1–6. doi:10.1109/AICCSA50499.2020.9316535

    work page doi:10.1109/aiccsa50499.2020.9316535 2020

  59. [59]

    Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto

    Grant O. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto

  60. [60]

    InAutomated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II (LNCS, Vol

    The Imandra Automated Reasoning System (System Description). InAutomated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II (LNCS, Vol. 12167), Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer, Cham, Switzerland, 464–471. doi:10.1007/978-3-030-51054-1_30

    work page doi:10.1007/978-3-030-51054-1_30 2020

  61. [61]

    Ethan A Poweleit, Alexander A Vinks, and Tomoyuki Mizuno. 2023. Artificial intelligence and machine learning approaches to facilitate therapeutic drug management and model-informed precision dosing.Therapeutic drug monitoring45, 2 (2023), 143–150

    2023

  62. [62]

    Barrett, and Jeremy Avigad

    Yicheng Qian, Joshua Clune, Clark W. Barrett, and Jeremy Avigad. 2025. Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. InComputer Aided Verification - 37th International Conference, CA V 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III (LNCS, Vol. 15933), Ruzica Piskac and Zvonimir Rakamaric (Eds.). Springer, Cham, Swit...

    work page doi:10.1007/978-3-031-98682-6_10 2025

  63. [63]

    2017.Verification of Sampled-Data Systems using Coq

    Daniel Ricketts. 2017.Verification of Sampled-Data Systems using Coq. Ph. D. Dissertation. University of California, San Diego, USA. http: //www.escholarship.org/uc/item/5n1899s2

    2017

  64. [64]

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. 2025. Neural Network Verification with Branch-and-Bound for General Nonlinearities. InTools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I (LNCS, Vol. 15696), Ar...

    work page doi:10.1007/978-3-031-90643-5_17 2025

  65. [65]

    George F. Simmons. 1972.Differential Equations with Applications and Historical Notes(3 ed.). CRC Press. Manuscript submitted to ACM 30 Daggitt et al

    1972

  66. [66]

    Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2019. An abstract domain for certifying neural networks.Proc. ACM Program. Lang.3, POPL (2019), 41:1–41:30. doi:10.1145/3290354

    work page doi:10.1145/3290354 2019

  67. [67]

    Daggitt, and Robert J

    Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, and Robert J. Stewart. 2022. Differentiable Logics for Neural Network Training and Verification. In15th International Workshop, Numerical Software Verification 2022, Haifa, Israel, July 31 - August 1, and August 11, 2022, Proceedings (LNCS, Vol. 13466), Omri Isac, Radoslav Ivanov, Guy Katz, Ni...

    work page doi:10.1007/978-3-031-21222-2_5 2022

  68. [68]

    Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent types and multi-monadic effects in F. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Princ...

    work page doi:10.1145/2837614.2837655 2016

  69. [69]

    Wouter Swierstra. 2008. Data types à la carte.J. Funct. Program.18, 4 (2008), 423–436. doi:10.1017/S0956796808006758

    work page doi:10.1017/s0956796808006758 2008

  70. [70]

    Alan Talevi and Carolina L. Bellera. 2021. One-Compartment Pharmacokinetic Model. InThe ADME Encyclopedia: A Comprehensive Guide on Biopharmacy and Pharmacokinetics. Springer International Publishing, Cham, Switzerland, 1–8. doi:10.1007/978-3-030-51519-5_58-1

    work page doi:10.1007/978-3-030-51519-5_58-1 2021

  71. [71]

    Alan Talevi and Carolina L. Bellera. 2021. Two-Compartment Pharmacokinetic Model. InThe ADME Encyclopedia. Springer, Cham, Switzerland, 1–8. doi:10.1007/978-3-030-51519-5_59-1

    work page doi:10.1007/978-3-030-51519-5_59-1 2021

  72. [72]

    Samuel Teuber, Debasmita Lohar, and Bernhard Beckert. 2025. Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision. InProceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, Ahmed Irfan and Daniela Kaufmann (Eds.). TU Wien Academic Press, Vienna, Austria. ...

    work page doi:10.34727/2025/isbn.978-3-85448-084-6_12 2025

  73. [73]

    Samuel Teuber, Stefan Mitsch, and André Platzer. 2024. Provably Safe Neural Network Controllers via Differential Dynamic Logic. InAdvances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024, Amir Globersons, Lester Mackey, Danielle Belgra...

    2024

  74. [74]

    2025.The Rocq Reference Manual, version 9.1.0

    The Rocq Development Team. 2025.The Rocq Reference Manual, version 9.1.0

    2025

  75. [75]

    2016.Liquid Haskell: Haskell as a Theorem Prover

    Niki Vazou. 2016.Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation. University of California, San Diego, USA

    2016

  76. [76]

    Zico Kolter

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. InAdvances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December...

    2021

  77. [77]

    Yixuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, and Qi Zhu. 2024. POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems.IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.43, 3 (2024), 994–1007. doi:10.1109/TCAD.2023.3331215

    work page doi:10.1109/tcad.2023.3331215 2024

  78. [78]

    White, Laura Titolo, J

    Lauren M. White, Laura Titolo, J. Tanner Slagel, and César A. Muñoz. 2024. A Temporal Differential Dynamic Logic Formal Embedding. InProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy (Eds.). ACM, New Yo...

    work page doi:10.1145/3636501.3636943 2024

  79. [79]

    In: International Conference on Computer Aided Verification

    Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, et al . 2024. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. InComputer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II (LNCS, Vol. 14682), Arie Gurfinke...

    work page doi:10.1007/978-3-031-65630-9_13 2024

  80. [80]

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net. https://openreview...

    2021

Showing first 80 references.