Follow
Jonathan Julian Huerta y Munive
Jonathan Julian Huerta y Munive
Verified email at cvut.cz - Homepage
Title
Cited by
Cited by
Year
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
S Foster, JJH y Munive, G Struth
International Conference on Relational and Algebraic Methods in Computer ¡K, 2020
422020
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
S Foster, JJ Huerta y Munive, M Gleirscher, G Struth
International Symposium on Formal Methods, 367-386, 2021
252021
Verifying hybrid systems with modal Kleene algebra
JJ Huerta y Munive, G Struth
Relational and Algebraic Methods in Computer Science: 17th International ¡K, 2018
252018
Predicate Transformer Semantics for Hybrid Systems
JJH y Munive, G Struth
arXiv preprint arXiv:1909.05618, 2019
162019
Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
JJ Huerta y Munive
Software Engineering and Formal Methods: 18th International Conference, SEFM ¡K, 2020
142020
VeriMon: A Formally Verified Monitoring Tool
D Basin, T Dardinier, N Hauser, L Heimes, JJ Huerta y Munive, ...
International Colloquium on Theoretical Aspects of Computing, 1-6, 2022
122022
Verification components for hybrid systems
JJH y Munive
Archive of Formal Proofs, 2019
122019
Predicate transformer semantics for hybrid systems: verification components for Isabelle/HOL
JJ Huerta y Munive, G Struth
Journal of Automated Reasoning 66 (1), 93-139, 2022
92022
Algebraic verification of hybrid systems in Isabelle/HOL
JJ Huerta y Munive
University of Sheffield, 2020
92020
ARCH-COMP22 category report: Hybrid systems theorem proving
S Mitsch, B Zhan, H Sheng, A Bentkamp, X Jin, S Wang, S Foster, ...
ARCH22 90, 185-203, 2022
62022
Matrices for ODEs
JJH y Munive
Archive of Formal Proofs, 2020
62020
Explainable Online Monitoring of Metric First-Order Temporal Logic
L Lima, JJ Huerta y Munive, D Traytel
International Conference on Tools and Algorithms for the Construction and ¡K, 2024
42024
Relaxing safety for metric first-order temporal logic via dynamic free variables
JJ Huerta y Munive
International Conference on Runtime Verification, 45-66, 2022
42022
ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving
S Mitsch, JJH y Munive, X Jin, B Zhan, S Wang, N Zhan
ARCH20, 141-161, 2019
22019
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
JJH y Munive, S Foster, M Gleirscher, G Struth, CP Laursen, T Hickman
12024
ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving
S Mitsch, H Sheng, B Zhan, S Wang, S Foster, JJH y Munive
Proceedings of 10th International Workshop on Applied 96, 170-188, 2023
12023
IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale
JJ Huerta y Munive, S Foster, M Gleirscher, G Struth, C Pardillo Laursen, ...
Journal of Automated Reasoning 68 (4), 21, 2024
2024
Isabelle/RL Project Proposal: Reinforcement learning on the Isabelle proof assistant
JJH y Munive
2024
A Verified Proof Checker for Metric First-Order Temporal Logic
A Herasimau, JJH y Munive, L Lima, M Raszyk, D Traytel
Arch. Formal Proofs 2024, 2024
2024
WHYMON: A Runtime Monitoring Tool with Explanations as Verdicts
L Lima, JJH y Munive, D Traytel
The system can't perform the operation now. Try again later.
Articles 1–20