Research output per year
Research output per year
Personal profile
Research profile
I am a researcher focused on interactive theorem-proving, formal verification and their automation. I obtained my BSc in Mathematics at the Benemérita Universidad Autónoma de Puebla (BUAP) in Puebla, México (Thesis: Studying the Foundations of Mathematics comparing some of its Axiomatizations). I later did my PhD with an integrated MSc at the University of Sheffield in Computer Science. My research interests lie around proof assistants: their foundations, automation, and practical applications. I developed a framework for verifying cyber-physical systems in the Isabelle/HOL proof assistant, contributed to the verification of generic, runtime monitoring tools, and developed automation tools for Isabelle/HOL. You can see my publications here. I have also been a postdoc at the University of Copenhagen, I did a Marie Curie (MSCA) fellowship at the Czech Technical University in Prague, worked as a Data Scientist at Twinkl Educational Publishing, and have taught logic and Isabelle/HOL in México, England, Norway, and Denmark.
Education/Academic qualification
Computer Science, PhD, Algebraic verification of hybrid systems in Isabelle/HOL, University of Sheffield
26 Sept 2016 → 28 May 2021
Keywords
- Computer Science
- deductive verification
- interactive theorem proving
- automated reasoning
- Logic in Computer Science
Fingerprint
Dive into the research topics where Jonathan Julian Huerta y Munive is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
- 1 Similar Profiles
Collaborations and top research areas from the last five years
Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
-
Munkres' General Topology Autoformalized in Isabelle/HOL
Bryant, D., Munive, J. J. H. Y., Kaliszyk, C. & Urban, J., 8 Apr 2026, arXiv, 22 p.Research output: Working paper/Preprint › Preprint
Open Access5 Downloads (Pure) -
The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs
Tan, C., Donaldson, A. F., Huerta y Munive, J. J. & Wickerson, J., 2025, 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE). IEEE (Institute of Electrical and Electronics Engineers), p. 34-45 12 p. (IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE)).Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review
3 Link opens in a new tab Citations (Scopus) -
Verifying Numerical Methods with Isabelle/HOL
Bryant, D., Munive, J. J. H. Y. & Foster, S., 25 Nov 2025, arXiv.Research output: Working paper/Preprint › Preprint
Open AccessFile28 Downloads (Pure) -
WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts
Lima, L., Huerta y Munive, J. J. & Traytel, D., 2025, Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Proceedings. Akshay, S., Niemetz, A. & Sankaranarayanan, S. (eds.). Springer, p. 76-90 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 15055 LNCS).Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review
1 Link opens in a new tab Citation (Scopus) -
Explainable Online Monitoring of Metric First-Order Temporal Logic
Lima, L., Munive, J. J. H. Y. & Traytel, D., 2024, Tools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. Finkbeiner, B. & Kovács, L. (eds.). Springer, p. 288-307 20 p. (Lecture Notes in Computer Science, Vol. 14570).Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review
Open AccessFile4 Link opens in a new tab Citations (Scopus)49 Downloads (Pure)