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 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

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. Jonathan Julián Huerta y Munive. Matrices for ODEs. AFP, 2020. https://isa-afp.org/entries/Matrices_for_ODEs.html
  2. 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. Lima, Leonardo, Huerta y Munive, Jonathan Julian, Traytel, Dmitriy. 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
  2. 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
  3. 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
  4. 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 Proc. 24th Intl. Symp. on Formal Methods (FM 2021), volume LNCS 13047, pages 367–386, 2021. https://doi.org/10.1007/978-3-030-90870-6_20
  5. 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
  6. 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
  7. 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