Publications

Thesis: Algebraic Verification of Hybrid Systems in Isabelle/HOL https://etheses.whiterose.ac.uk/28886/

Journal Articles

  1. Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen and Thomas Hickman. IsaVODEs: Interactive Verification of Cyber-Physical Systemsat Scale. Journal of Automated Reasoning, 68(21), 2024. https://doi.org/10.1007/s10817-024-09709-2
  2. Jonathan Julián Huerta y Munive and Georg Struth. Predicate Transformer Semantics for Hybrid Systems. Journal of Automated Reasoning, 66(1):93–139, 2022. https://doi.org/10.1007/s10817-021-09607-x

Software in Active Devlopment

  1. Jonathan Julián Huerta y Munive (2023). DeepIsaHOL (Version 2024.11.18). https://github.com/yonoteam/DeepIsaHOL
  2. Chengsong Tan, Jonathan Julián Huerta y Munive (2025). Supersketch and Superfix. https://github.com/ChengsongTan/super_sketch_and_super_fix
  3. Simon Foster, Frank Zeyda, Kangfeng Ye, Jonathan Julián Huerta y Munive, Pedro Ribeiro, James Baxter, Burkhart Wolff, Chung-Kil Hur, Christian Pardillo Laursen, Fang Yan. Isabelle/UTP (2020). https://github.com/isabelle-utp

Competition Reports

  1. Stefan Mitsch, Huanhuan Sheng, Bohua Zhan, Shuling Wang, Simon Foster and Jonathan Julián Huerta y Munive. ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving. In Goran Frehse and Matthias Althoff, editors, ARCH23. 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), volume 96 of EPiC Series in Computing, pages 170-188. EasyChair, 2023. https://doi.org/10.29007/57g4
  2. Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen and Jonathan Julián Huerta y Munive. ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. In Goran Frehse, Matthias Althoff, Erwin Schoitsch and Jeremie Guiochet, editors, ARCH22. 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), volume 90 of EPiC Series in Computing, pages 185–203. EasyChair, 2022. https://doi.org/10.29007/4lxf
  3. Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, and Naijun Zhan. ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. In Goran Frehse and Matthias Althoff, editors, ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), volume 74 of EPiC Series in Computing, pages 153–174. EasyChair, 2020. https://doi.org/10.29007/bdq9

Artefacts

  1. Chengsong Tan, Alastair Donaldson, Jonathan Julián Huerta y Munive, and John Wickerson. (2024). Artefact for the scientific article “The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs” (1.0.1). For Formal methods in Software Engineering (FormaliSE), Ottawa, Ontario, Canada. In Zenodo. https://doi.org/10.5281/zenodo.14275602
  2. Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk and Dmitriy Traytel. A Verified Proof Checker for Metric First-Order Temporal Logic. AFP, 2024. https://www.isa-afp.org/entries/MFOTL_Checker.html
  3. Jonathan Julián Huerta y Munive. Matrices for ODEs. AFP, 2020. https://isa-afp.org/entries/Matrices_for_ODEs.html
  4. Jonathan Julián Huerta y Munive. Verification components for hybrid systems. AFP, 2019. https://isa-afp.org/entries/Hybrid_Systems_VCs.html

Conference Articles

  1. Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson, The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs, Formalise 2025, Ottawa, Canada, 2025, IEEE/ACM, pp. 34-45. https://doi.org/10.1109/FormaliSE66629.2025.00010
  2. Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel. (2025). WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts. ATVA 2024. LNCS volume 15055. Springer. https://doi.org/10.1007/978-3-031-78750-8_4
  3. Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel. Explainable Online Monitoring of Metric First-Order Temporal Logic. TACAS 2024. LNCS, vol 14570. Springer. https://doi.org/10.1007/978-3-031-57246-3_16
  4. David Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srđan Krstić, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila Zingg. Verimon: A Formally Verified Monitoring Tool. ICTAC 2022, Tbilisi, 2022, volume 13572 of LNCS, pages 1-6. Springer. https://doi.org/10.1007/978-3-031-17715-6_1
  5. Jonathan Julián Huerta y Munive. Relaxing Safety for Metric First-Order Temporal Logic via Dynamic Free Variables. RV2022, Tbilisi, 2022. https://doi.org/10.1007/978-3-031-17196-3_3
  6. Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, and Georg Struth. Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. In Formal Methods (FM 2021), volume LNCS 13047, pages 367–386, 2021. https://doi.org/10.1007/978-3-030-90870-6_20
  7. Jonathan Julián Huerta y Munive. Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. In SEFM 2020, volume 12310 of LNCS, pages 77–92. Springer, 2020. https://doi.org/10.1007/978-3-030-58768-0_5
  8. Simon Foster, Jonathan Julián Huerta y Munive, and Georg Struth. Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. In RAMiCS 2020, pages 169–186, 2020. https://doi.org/10.1007/978-3-030-43520-2_11
  9. Jonathan Julián Huerta y Munive and Georg Struth. Verifying Hybrid Systems with Modal Kleene Algebra. In RAMiCS 2018, volume 11194 of LNCS, pages 225–243. Springer, 2018. https://doi.org/10.1007/978-3-030-02149-8_14