Cover Image

Verifying Numerical Methods with Isabelle/HOL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bryant, Dustin, Munive, Jonathan Julian Huerta y, Foster, Simon
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Munkres' General Topology Autoformalized in Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2026)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
by: Munive, Jonathan Julián Huerta y, et al.
Published: (2024)

Brownian Motion in Isabelle/HOL
by: Laursen, Christian Pardillo, et al.
Published: (2024)

Linear Programming in Isabelle/HOL
by: Parsert, Julian
Published: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
by: Foster, Simon, et al.
Published: (2024)

Complex Bounded Operators in Isabelle/HOL
by: Unruh, Dominique, et al.
Published: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
by: Bartl, Lukas, et al.
Published: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
by: Guzman, Laura P. Gamboa, et al.
Published: (2024)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
by: Hulak, David B., et al.
Published: (2026)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
by: Bryant, Dustin, et al.
Published: (2025)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
by: Schmoetten, Richard, et al.
Published: (2024)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
by: Linzi, Alessandro
Published: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
by: Binder, Sage, et al.
Published: (2026)

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
by: Kim, Jinwook
Published: (2026)

Formally Verified Animation for RoboChart using Interaction Trees
by: Ye, Kangfeng, et al.
Published: (2023)

Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
by: Bilotta, Antonella
Published: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Mechanized HOL Reasoning in Set Theory
by: Guilloud, Simon, et al.
Published: (2024)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
by: Huch, Fabian
Published: (2024)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
by: Kammüller, Florian
Published: (2023)

GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
by: Myreen, Magnus O., et al.
Published: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
by: Guilloud, Simon, et al.
Published: (2025)

Numerical Considerations in Weighted Model Counting
by: Bryant, Randal E.
Published: (2025)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
by: Bryant, Randal E., et al.
Published: (2025)

On the Formalization of Network Topology Matrices in HOL
by: Aksoy, Kubra, et al.
Published: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Type Inference for Isabelle2Cpp
by: Jiang, Dongchen, et al.
Published: (2024)

Teaching Higher-Order Logic Using Isabelle
by: Lund, Simon Tobias, et al.
Published: (2024)

Wait-Only Broadcast Protocols are Easier to Verify
by: Guillou, Lucie, et al.
Published: (2025)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)

An Imperative Language for Verified Exact Real-Number Computation
by: Bauer, Andrej, et al.
Published: (2024)

Verifying SQL Queries using Theories of Tables and Relations
by: Mohamed, Mudathir, et al.
Published: (2024)

VerifyThis 2019: A Program Verification Competition (Extended Report)
by: Dross, Claire, et al.
Published: (2020)

Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
by: Barenbaum, Pablo
Published: (2026)

Verifying Global Two-Safety Properties in Neural Networks with Confidence
by: Athavale, Anagha, et al.
Published: (2024)

Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
by: Losavio, Lidia, et al.
Published: (2025)