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 | 42 | 2020 |
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 | 25 | 2021 |
Verifying hybrid systems with modal Kleene algebra JJ Huerta y Munive, G Struth Relational and Algebraic Methods in Computer Science: 17th International ¡K, 2018 | 25 | 2018 |
Predicate Transformer Semantics for Hybrid Systems JJH y Munive, G Struth arXiv preprint arXiv:1909.05618, 2019 | 16 | 2019 |
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 | 14 | 2020 |
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 | 12 | 2022 |
Verification components for hybrid systems JJH y Munive Archive of Formal Proofs, 2019 | 12 | 2019 |
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 | 9 | 2022 |
Algebraic verification of hybrid systems in Isabelle/HOL JJ Huerta y Munive University of Sheffield, 2020 | 9 | 2020 |
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 | 6 | 2022 |
Matrices for ODEs JJH y Munive Archive of Formal Proofs, 2020 | 6 | 2020 |
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 | 4 | 2024 |
Relaxing safety for metric first-order temporal logic via dynamic free variables JJ Huerta y Munive International Conference on Runtime Verification, 45-66, 2022 | 4 | 2022 |
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 | 2 | 2019 |
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL JJH y Munive, S Foster, M Gleirscher, G Struth, CP Laursen, T Hickman | 1 | 2024 |
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 | 1 | 2023 |
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 | | |