Verifying Hybrid Systems with Modal Kleene Algebra. - Jonathan Julián Huerta y Munive; Georg Struth (RAMiCS, 2018)

Verification Components for Hybrid Systems. - Jonathan Julián Huerta y Munive (Arch. Formal Proofs, 2019)

Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL. - Jonathan Julián Huerta y Munive; Georg Struth (CoRR, 2019)

Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. - Simon Foster 001; Jonathan Julián Huerta y Munive; Georg Struth (RAMiCS, 2020)

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Jonathan Julián Huerta y Munive; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH, 2020)

Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. - Jonathan Julián Huerta y Munive (SEFM, 2020)

Matrices for ODEs. - Jonathan Julián Huerta y Munive (Arch. Formal Proofs, 2020)

Algebraic verification of hybrid systems in Isabelle/HOL - Jonathan Julián Huerta y Munive (2020)

Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. - Simon Foster 001; Jonathan Julián Huerta y Munive; Mario Gleirscher; Georg Struth (FM, 2021)

ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Bohua Zhan; Huanhuan Sheng; Alexander Bentkamp; Xiangyu Jin; Shuling Wang 003; Simon Foster 001; Christian Pardillo Laursen; Jonathan Julián Huerta y Munive (ARCH@SAFECOMP, 2022)

VeriMon: A Formally Verified Monitoring Tool. - David A. Basin; Thibault Dardinier; Nico Hauser; Lukas Heimes; Jonathan Julián Huerta y Munive; Nicolas Kaletsch; Srdan Krstic; Emanuele Marsicano; Martin Raszyk; Joshua Schneider 001; Dawit Legesse Tirore; Dmitriy Traytel; et al. (ICTAC, 2022)

Relaxing Safety for Metric First-Order Temporal Logic via Dynamic Free Variables. - Jonathan Julián Huerta y Munive (RV, 2022)

Predicate Transformer Semantics for Hybrid Systems. - Jonathan Julián Huerta y Munive; Georg Struth (J. Autom. Reason., 2022)

ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Huanhuan Sheng; Bohua Zhan; Shuling Wang 003; Simon Foster 001; Jonathan Julián Huerta y Munive (ARCH, 2023)

WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts. - Leonardo Lima 001; Jonathan Julián Huerta y Munive; Dmitriy Traytel (ATVA (2), 2024)

Explainable Online Monitoring of Metric First-Order Temporal Logic. - Leonardo Lima 001; Jonathan Julián Huerta y Munive; Dmitriy Traytel (TACAS (1), 2024)

A Verified Proof Checker for Metric First-Order Temporal Logic. - Andrei Herasimau; Jonathan Julián Huerta y Munive; Leonardo Lima 001; Martin Raszyk; Dmitriy Traytel (Arch. Formal Proofs, 2024)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL. - Jonathan Julián Huerta y Munive; Simon Foster 001; Mario Gleirscher; Georg Struth; Christian Pardillo Laursen; Thomas Hickman (CoRR, 2024)

IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale. - Jonathan Julián Huerta y Munive; Simon Foster 001; Mario Gleirscher; Georg Struth; Christian Pardillo Laursen; Thomas Hickman (J. Autom. Reason., 2024)

The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs. - Chengsong Tan; Alastair F. Donaldson; Jonathan Julián Huerta y Munive; John Wickerson (FormaliSE, 2025)