5 citations · 6 across the 6 of their papers we have counts for
7 papers
Munkres' General Topology Autoformalized in Isabelle/HOL
Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk +1
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Ch…
Verifying Numerical Methods with Isabelle/HOL
Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster
Modern machine learning pipelines and ODE solvers are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-p…
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher +3
We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic fo…
Relaxing safety for metric first-order temporal logic via dynamic free variables
Jonathan Julian Huerta y Munive
We define a fragment of metric first-order temporal logic formulas that guarantees the finiteness of their table representations. We extend our fragment's definition to cover the t…
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher +1
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for…
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Simon Foster, Jonathan Julián Huerta y Munive, Georg Struth
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasonin…
Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL
Jonathan Julián Huerta y Munive, Georg Struth
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the st…