pith. sign in

arxiv: 2606.19532 · v1 · pith:Y4AT74VSnew · submitted 2026-06-17 · 💻 cs.LO

Vancomycert: A Certified Neuro-Symbolic Drug Delivery System (Case Study)

Alistair Sirman , Fleur Conway , Jessica Ciupa , Gusts Gustavs Gr\=inbergs , Ekaterina Komendantskaya , Thai Son Hoang , Michael Rawson , Alessandro Bruni
show 2 more authors
Vaishak Belle Michael John Williams
This is my paper

Pith reviewed 2026-06-26 18:37 UTC · model grok-4.3

classification 💻 cs.LO
keywords formal verificationneural network controllerdrug dosingvancomycinneuro-symbolic systemssafety propertiesinfinite horizontheorem proving
0
0 comments X

The pith

A neural network for vancomycin dosing is formally verified to keep concentrations below harmful levels over infinite time horizons.

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

The paper presents a case study that trains a supervised neural network on synthetic clinician data to control vancomycin doses and then formally verifies safety properties of that network. It constructs a simplified patient model tracking drug levels, temperature, and white blood cell counts, then uses the Vehicle tool inside the Rocq prover to prove that the network's input-output behavior implies the system will never exceed the supratherapeutic boundary at any future time. A sympathetic reader would care because the approach aims to combine the adaptability of neural controllers with mathematical guarantees that are essential when errors can cause organ damage or treatment failure.

Core claim

Verifying an input-output safety property of the trained neural network controller implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary; the combined property is established in Rocq by using the Vehicle back-end to integrate the neural-network proof with the system dynamics.

What carries the argument

The Vehicle interactive theorem prover back-end that links neural-network property verification to infinite-horizon system proofs inside Rocq.

If this is right

  • Automated dosing can adapt to individual patient responses while still carrying a machine-checked guarantee against overdose at any future time.
  • The same verification pipeline can be reused for other treatment policies as long as each policy satisfies the same neural-network safety property.
  • Safety holds across unbounded time horizons without requiring repeated re-verification at each step.
  • Different patient-specific parameter sets can be plugged into the model while the core safety proof remains unchanged.

Where Pith is reading between the lines

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

  • The method could be tested on other narrow-therapeutic-window drugs by swapping the pharmacokinetic model while reusing the Vehicle-Rocq integration.
  • Connecting the verified controller to continuous sensor streams might allow periodic re-checking of the model assumptions against live data.
  • The same neuro-symbolic pattern could apply to closed-loop systems such as insulin pumps or mechanical ventilators where both adaptability and long-term safety are required.

Load-bearing premise

The simplified model that tracks only drug concentration, body temperature, and white blood cell count is adequate to guarantee real-world safety for vancomycin dosing.

What would settle it

A simulation or clinical dataset in which real patient responses cause the verified network to produce supratherapeutic concentrations while the model assumptions remain satisfied.

Figures

Figures reproduced from arXiv: 2606.19532 by Alessandro Bruni, Alistair Sirman, Ekaterina Komendantskaya, Fleur Conway, Gusts Gustavs Gr\=inbergs, Jessica Ciupa, Michael John Williams, Michael Rawson, Thai Son Hoang, Vaishak Belle.

Figure 1
Figure 1. Figure 1: The difference between the concentration from a single dose C, and the total concentration CΣ. is continuous and differentiable everywhere except where t is a multiple of ttd, where it is only continuous. We must also define what information is required for accurate dosing, and what a clinically viable patient is. The information used to make an accurate dosing decision is the patient’s current concentrati… view at source ↗
read the original abstract

Neural network controllers for autonomous decision-making are well-established in cyber-physical systems, yet their deployment in safety-critical healthcare settings remains largely unverified. This paper presents a methodology and case study for the formal verification of a neural network controller for antibiotic dosing, motivated by the challenge of systems that must be simultaneously adaptive and provably safe across unbounded time horizons. We construct a simplified yet clinically-interpretable model that tracks drug concentration, body temperature, and white blood cell count. Vancomycin is selected as a representative antibiotic, widely prescribed for severe infections yet carrying a narrow therapeutic window, where supratherapeutic concentrations risk nephrotoxicity and subtherapeutic dosing risks treatment failure. A supervised neural network controller is trained on synthetic clinician-style dosing data. We establish formal verification of input-output safety properties, specifically verifying a property of a neural network that implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary. This system property is proven in Rocq using the Vehicle interactive theorem prover back-end to integrate the different proof systems. The end result is a verification pipeline that allows for a wide variety of treatment approaches whilst maintaining safety for each specific patient.

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

2 major / 2 minor

Summary. The paper presents a case study on a neuro-symbolic verification pipeline for a neural network controller in vancomycin dosing. It constructs a simplified three-variable model (drug concentration, body temperature, white blood cell count), trains a supervised NN on synthetic clinician-style data, and claims to prove in Rocq (via the Vehicle backend) an input-output safety property of the NN that implies an infinite-horizon guarantee that automated dosing never exceeds the supratherapeutic boundary.

Significance. If the central verification claim holds with a complete invariant for the closed-loop dynamics, the work would provide a concrete demonstration of machine-checked proofs for adaptive yet provably safe medical controllers, strengthening the case for neuro-symbolic methods in safety-critical CPS. The integration of Vehicle with Rocq for multi-system proofs is a technical strength worth highlighting.

major comments (2)
  1. [Abstract] Abstract: the claim that 'verifying a property of a neural network ... implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary' is load-bearing for the central result, yet the manuscript supplies no model equations, no proof outline, and no description of an invariant lemma establishing that closed-loop trajectories remain inside the NN's verified input domain for all future time. Without this, the implication from the NN property to infinite-horizon safety does not follow even inside the model.
  2. [Model description] Model description section: the assertion that the simplified three-variable model 'adequately captures the dynamics needed to guarantee real-world safety' is not supported by any comparison to standard pharmacokinetic equations, parameter fitting to clinical data, or sensitivity analysis; this directly undermines the transfer of the Rocq proof to the stated clinical motivation.
minor comments (2)
  1. [Training] The description of the synthetic training data generation lacks detail on how clinician-style dosing policies were encoded and whether any regularization was applied to avoid overfitting to the safety boundary.
  2. [Notation] Notation for the state variables (concentration, temperature, WBC count) and the NN input domain should be introduced with explicit bounds before the verification claim is stated.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed comments, which highlight important gaps in the presentation of our central claims. We address each major comment below and commit to revisions that strengthen the manuscript without overstating the scope of this case study.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that 'verifying a property of a neural network ... implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary' is load-bearing for the central result, yet the manuscript supplies no model equations, no proof outline, and no description of an invariant lemma establishing that closed-loop trajectories remain inside the NN's verified input domain for all future time. Without this, the implication from the NN property to infinite-horizon safety does not follow even inside the model.

    Authors: We agree that the implication from the verified NN property to an infinite-horizon safety guarantee is load-bearing and requires explicit support. The manuscript does present the three-variable model equations in the Model Description section and states that the NN property is verified via Vehicle in Rocq, but we acknowledge that a self-contained proof outline and the invariant lemma (showing that closed-loop trajectories remain in the verified input domain) are not described in sufficient detail. We will add a dedicated subsection in the Verification section that states the invariant, sketches its preservation under the dynamics, and explains the composition with the NN property. This addresses the gap directly. revision: yes

  2. Referee: [Model description] Model description section: the assertion that the simplified three-variable model 'adequately captures the dynamics needed to guarantee real-world safety' is not supported by any comparison to standard pharmacokinetic equations, parameter fitting to clinical data, or sensitivity analysis; this directly undermines the transfer of the Rocq proof to the stated clinical motivation.

    Authors: The manuscript describes the model as simplified and clinically interpretable for the purpose of the verification case study, not as a claim of real-world deployment. We do not assert that it guarantees real-world safety; the safety claim is scoped to the model. Nevertheless, the referee's point is well-taken regarding transferability. We will revise the Model Description section to include a short comparison to standard one-compartment vancomycin pharmacokinetic models and to report a basic sensitivity analysis over the model parameters. We cannot add parameter fitting to clinical data because the training set is synthetic clinician-style data by design; this limitation will be stated explicitly. revision: partial

Circularity Check

0 steps flagged

No significant circularity; verification is independent of training data

full rationale

The paper trains a supervised neural network on synthetic clinician-style dosing data, then separately establishes formal verification of input-output safety properties in Rocq using the Vehicle back-end. The abstract states that a verified NN property 'implies an infinite-horizon proof' of safety, but this is presented as a theorem-prover result rather than a statistical prediction or self-referential definition. No equations or steps reduce the safety claim to fitted parameters by construction, and no load-bearing self-citations are quoted that would make the central result equivalent to prior author work. The derivation chain is self-contained against external benchmarks (theorem proving) and receives the default non-circular finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract provides insufficient detail to enumerate free parameters or invented entities; the central claim rests on the domain assumption that the three-variable model is adequate for safety.

axioms (1)
  • domain assumption The simplified model tracking drug concentration, body temperature, and white blood cell count is clinically interpretable and representative for safety verification purposes.
    Invoked to justify that the verified property transfers to clinical relevance.

pith-pipeline@v0.9.1-grok · 5774 in / 1109 out tokens · 30086 ms · 2026-06-26T18:37:25.319093+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

37 extracted references · 23 canonical work pages

  1. [1]

    In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

    Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: FOSSIL: a soft- ware tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. pp. 1–11. HSCC ’21, Association for Computing Machinery (2021).https://doi.or...

    work page doi:10.1145/3447928.3456646 2021

  2. [2]

    Affeldt, R., Bertot, Y., Bruni, A., Cohen, C., Kerjean, M., Mahboubi, A., Rouh- ling, D., Roux, P., Sakaguchi, K., Stone, Z., Strub, P.Y., Théry, L.: MathComp- analysis: Mathematical components compliant analysis library (2026),https: //github.com/math-comp/analysis

    2026

  3. [3]

    CoRR abs/1803.08375(2018),http://arxiv.org/abs/1803.08375

    Agarap, A.F.: Deep learning using rectified linear units (relu). CoRR abs/1803.08375(2018),http://arxiv.org/abs/1803.08375

    Pith/arXiv arXiv 2018

  4. [4]

    Journal of Infection and Public Health15(5), 589– 593 (2022).https://doi.org/10.1016/j.jiph.2022.04.007

    Al-Maqbali, J.S., Shukri, Z.A., Sabahi, N.A., Al-Riyami, I., Al Alawi, A.M.: Van- comycin therapeutic drug monitoring (TDM) and its association with clinical out- comes: A retrospective cohort. Journal of Infection and Public Health15(5), 589– 593 (2022).https://doi.org/10.1016/j.jiph.2022.04.007

    work page doi:10.1016/j.jiph.2022.04.007 2022

  5. [5]

    Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada

    Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control Barrier Functions: Theory and Applications. In: 2019 18th European Control Conference (ECC). pp. 3420–3431. IEEE, Naples, Italy (Jun 2019).https://doi.org/10.23919/ECC.2019.8796030,https:// ieeexplore.ieee.org/document/8796030/

    work page doi:10.23919/ecc.2019.8796030 2019

  6. [6]

    Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results (2024), https://arxiv.org/abs/2412.19985

    arXiv 2024

  7. [7]

    In: Shoham, S., Vizel, Y

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural Network Robustness as a Verification Property: A Principled Case Study. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. pp. 219–231. Springer International Publishing, Cham (2022).https://doi.org/10. 1007/978-3-031-13185-1_11

    2022

  8. [8]

    International Journal of Medical Infor- matics149, 104403 (2021).https://doi.org/10.1016/j.ijmedinf.2021.104403, https://www.sciencedirect.com/science/article/pii/S1386505621000290

    Chun, J.Y., Song, K.H., Lee, D.e., Hwang, J.H., Jung, H.G., Heo, E., Kim, H.s., Yoon, S., Park, J.S., Choe, P.G., Chung, J.Y., Park, W.B., Bang, J.H., Hwang, H., Park, K.U., Park, S.W., Kim, N.J., Oh, M.d., Kim, E.S., Kim, H.B.: Impact of a computerised clinical decision support system on vancomycin loading and the risk of nephrotoxicity. International Jo...

    work page doi:10.1016/j.ijmedinf.2021.104403 2021

  9. [9]

    In: Narodytska, N., Amir, G., Katz, G., Isac, O

    Daggitt, M., Kokke, W., Komendantskaya, E., Atkey, R., Arnaboldi, L., Slusarz, N., Casadio, M., Coke, B., Lee, J.: The vehicle tutorial: Neural network verification with vehicle. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems. Kalpa Publications in Computing, vol....

    work page doi:10.29007/5s2x 2023

  10. [10]

    Daggitt, M., Kokke, W., Ślusarz, N., Atkey, R., Casadio, M., Komendantskaya, E.: Vehicle (Feb 2026),https://github.com/vehicle-lang/vehicle

    2026

  11. [11]

    In: Formal Structures for Computation and Deduction 2025

    Daggitt, M.L., Kokke, W., Atkey, R., Komendantskaya, E., Slusarz, N., Arnaboldi, L.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic programs. In: Formal Structures for Computation and Deduction 2025. No. arXiv:2401.06379, arXiv (2025).https://doi.org/10.48550/arXiv.2401.06379, http://arxiv.org/abs/2401.06379 Vancomycert: Certifi...

    work page doi:10.48550/arxiv.2401.06379 2025

  12. [12]

    Safe Control With Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control,

    Dawson, C., Gao, S., Fan, C.: Safe Control With Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control. IEEE Transactions on Robotics39(3), 1749–1767 (Jun 2023). https://doi.org/10.1109/TRO.2022.3232542,https://ieeexplore.ieee.org/ document/10015199/

    work page doi:10.1109/tro.2022.3232542 2023

  13. [13]

    In: Majumdar, R., Kunčak, V

    Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.: SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification, vol. 10427, pp. 126–133. Springer International Publishing, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_7,https://link.springer. com/10.100...

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

  14. [14]

    Flinkow, T., Casadio, M., Kessler, C., Monahan, R., Komendantskaya, E.: A gen- eral framework for property-driven machine learning (2025),https://arxiv.org/ abs/2505.00466

    arXiv 2025

  15. [15]

    Atmospheric Environment 32(14), 2627–2636 (1998).https://doi.org/10.1016/S1352-2310(97)00447-0, https://www.sciencedirect.com/science/article/pii/S1352231097004470

    Gardner, M., Dorling, S.: Artificial neural networks (the multilayer perceptron)— a review of applications in the atmospheric sciences. Atmospheric Environment 32(14), 2627–2636 (1998).https://doi.org/10.1016/S1352-2310(97)00447-0, https://www.sciencedirect.com/science/article/pii/S1352231097004470

    work page doi:10.1016/s1352-2310(97)00447-0 1998

  16. [16]

    In: Silva, A., Leino, K.R.M

    Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 249–262. Springer InternationalPublishing(2021).https://doi.org/10.1007/978-3-030-81685-8_ 11

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

  17. [17]

    In: 8th International Workshop on Applied Ver- ification of Continuous and Hybrid Systems (ARCH21)

    Johnson,T.T.,ManzanasLopez,D.,Benet,L.,Forets,M.,Guadalupe,S.,Schilling, C., Ivanov, R., Carpenter, T.J., Weimer, J., Lee, I.: ARCH-COMP21 category re- port: Artificial intelligence and neural network control systems (AINNCS) for con- tinuous and hybrid systems plants. In: 8th International Workshop on Applied Ver- ification of Continuous and Hybrid Syste...

    work page doi:10.29007/kfk9 2021

  18. [18]

    Dill, Kyle Julian, and Mykel J

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An effi- cient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Springer International Publishing (2017).https://doi.org/10.1007/978-3-319-63387-9_5

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

  19. [19]

    In: International conference on computer aided verification

    Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., et al.: The marabou framework for verification and analysis of deep neural networks. In: International conference on computer aided verification. pp. 443–452. Springer (2019)

    2019

  20. [20]

    Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., Wu, H.: The 6th international verifica- tion of neural networks competition (VNN-COMP 2025): Summary and results (2025).https://doi.org/10.48550/arXiv.2512.19007,http://arxiv.org/abs/ 2512.19007

    work page doi:10.48550/arxiv.2512.19007 2025

  21. [21]

    Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization (2017),https: //arxiv.org/abs/1412.6980

    Pith/arXiv arXiv 2017

  22. [22]

    Wouter Kool, Herke van Hoof, and Max Welling

    M, K., LA, C., O, B., AC, G., AA., F.: The artificial intelligence clinician learns optimal treatment strategies for sepsis in intensive care. Nat Med24(11), 1716– 1720 (Nov 2018).https://doi.org/10.1038/s41591-018-0213-5

    work page doi:10.1038/s41591-018-0213-5 2018

  23. [23]

    Clinical Pharmacokinetics51(1), 1–13 (2012).https://doi.org/10.2165/11596390-000000000-00000 22 Sirman et al

    Marsot, A., Boulamery, A., Bruguerolle, B., Simon, N.: Vancomycin: a review of population pharmacokinetic analyses. Clinical Pharmacokinetics51(1), 1–13 (2012).https://doi.org/10.2165/11596390-000000000-00000 22 Sirman et al

    work page doi:10.2165/11596390-000000000-00000 2012

  24. [24]

    International Journal of Medical Informatics124, 1–5 (2019).https://doi.org/10.1016/j.ijmedinf.2019.01.002,https://www

    Pereboom, M., Mulder, I.J., Verweij, S.L., van der Hoeven, R.T.M., Becker, M.L.: A clinical decision support system to improve adequate dosing of gen- tamicin and vancomycin. International Journal of Medical Informatics124, 1–5 (2019).https://doi.org/10.1016/j.ijmedinf.2019.01.002,https://www. sciencedirect.com/science/article/pii/S1386505618309213

    work page doi:10.1016/j.ijmedinf.2019.01.002 2019

  25. [25]

    Platzer, A.: A complete uniform substitution calculus for differential dy- namic logic. J. Autom. Reas.59(2), 219–265 (2017).https://doi.org/10.1007/ s10817-016-9385-1

    2017

  26. [26]

    Therapeutic Drug Monitoring45(2), 143 (Apr 2023).https: //doi.org/10.1097/FTD.0000000000001078

    Poweleit, E.A., Vinks, A.A., Mizuno, T.: Artificial Intelligence and Machine Learn- ing Approaches to Facilitate Therapeutic Drug Management and Model-Informed Precision Dosing. Therapeutic Drug Monitoring45(2), 143 (Apr 2023).https: //doi.org/10.1097/FTD.0000000000001078

    work page doi:10.1097/ftd.0000000000001078 2023

  27. [27]

    Roy, A., Antony, A., Gimelli, A., Daggitt, M.L.: Vnn-lib 2.0: Rigorous foundations for neural network verification (2026),https://arxiv.org/abs/2605.07451

    Pith/arXiv arXiv 2026

  28. [28]

    In: Advances in Neural Information Processing Systems

    Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems. vol. 31. Curran Associates, Inc. (2018),https://papers.nips.cc/paper_files/ paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html

    2018

  29. [29]

    Sirman, A., Bruni, A.: Vancomycert Rocq Files (Mar 2026),https://github.com/ lstrsrmn/medical-nn-proof

    2026

  30. [30]

    In: The ADME Encyclopedia: A Comprehensive Guide on Biopharmacy and Pharmacoki- netics, pp

    Talevi, A., Bellera, C.L.: One-Compartment Pharmacokinetic Model. In: The ADME Encyclopedia: A Comprehensive Guide on Biopharmacy and Pharmacoki- netics, pp. 1–8. Springer International Publishing, Cham (2021).https://doi. org/10.1007/978-3-030-51519-5_58-1

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

  31. [31]

    In: 38th Annual Conference on Neural Informa- tion Processing Systems (2024).https://doi.org/10.48550/arXiv.2402.10998, http://arxiv.org/abs/2402.10998

    Teuber, S., Mitsch, S., Platzer, A.: Provably safe neural network controllers via differential dynamic logic. In: 38th Annual Conference on Neural Informa- tion Processing Systems (2024).https://doi.org/10.48550/arXiv.2402.10998, http://arxiv.org/abs/2402.10998

    work page doi:10.48550/arxiv.2402.10998 2024

  32. [32]

    In: Com- puter Aided Verification: 32nd International Conference, CAV 2020, Los Ange- les, CA, USA, July 21–24, 2020, Proceedings, Part I

    Tran, H.D., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Com- puter Aided Verification: 32nd International Conference, CAV 2020, Los Ange- les, CA, USA, July 21–24, 2020, Proceedings, Part I. pp. ...

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

  33. [33]

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, Z.: Beta- CROWN: 35th conference on neural information processing systems, NeurIPS

  34. [34]

    29909–29921 (2021), https://www.scopus.com/pages/publications/85131954698

    Advances in Neural Information Processing Systems 34 - 35th Conference on Neural Information Processing Systems, NeurIPS 2021 pp. 29909–29921 (2021), https://www.scopus.com/pages/publications/85131954698

    arXiv 2021

  35. [35]

    Frontiers in Pharmacology14, 1252757 (2023).https://doi.org/10.3389/fphar.2023.1252757

    Yoon, S., Guk, J., Lee, S.G., Chae, D., Kim, J.H., Park, K.: Model-informed pre- cision dosing in vancomycin treatment. Frontiers in Pharmacology14, 1252757 (2023).https://doi.org/10.3389/fphar.2023.1252757

    work page doi:10.3389/fphar.2023.1252757 2023

  36. [36]

    Zhang, H., Kazma, M.H., Ma, M., Johnson, T.T., Taha, A.F.: Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems (Mar 2026).https://doi.org/10.48550/arXiv.2603.13509,http://arxiv.org/ abs/2603.13509, arXiv:2603.13509 [eess]

    work page doi:10.48550/arxiv.2603.13509 2026

  37. [37]

    BMC Pharmacology Vancomycert: Certified Neural Dosing 23 & Toxicology26, 192 (2025).https://doi.org/10.1186/s40360-025-01035-6, https://pmc.ncbi.nlm.nih.gov/articles/PMC12625610/

    Zhang, T., Yi, J., Cheng, H., Han, X., Wang, Y., Xie, J., Yang, Q., Hu, S., Dong, Y.: Revised therapeutic window for vancomycin in pediatric patients: evi- dence from a retrospective therapeutic drug monitoring study. BMC Pharmacology Vancomycert: Certified Neural Dosing 23 & Toxicology26, 192 (2025).https://doi.org/10.1186/s40360-025-01035-6, https://pmc...

    work page doi:10.1186/s40360-025-01035-6 2025