Cover Image

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Munive, Jonathan Julián Huerta y, Foster, Simon, Gleirscher, Mario, Struth, Georg, Laursen, Christian Pardillo, Hickman, Thomas
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Mathematical Software
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Verifying Numerical Methods with Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2025)

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

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

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

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling
by: Altuntas, Alper, et al.
Published: (2025)

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

Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
by: Foster, Simon, et al.
Published: (2020)

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

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

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

Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2
by: Kaufmann, Matt, et al.
Published: (2025)

Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
by: Zhang, Junchao
Published: (2025)

AutoDeduct: A Tool for Automated Deductive Verification of C Code
by: Amilon, Jesper, et al.
Published: (2025)

Proceedings 14th International Conference on Automated Deduction in Geometry
by: Quaresma, Pedro, et al.
Published: (2024)

Tunable Automation in Automated Program Verification
by: Bai, Alexander Y., et al.
Published: (2025)

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

Formalizing UML State Machines for Automated Verification -- A Survey
by: André, Étienne, et al.
Published: (2024)

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)

Early Validation of High-level Requirements on Cyber-Physical Systems
by: Vašíček, Ondřej
Published: (2025)

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

LeanBET: Formally-verified surface area calculations in Lean
by: Ugwuanyi, Ejike D., et al.
Published: (2026)

A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics
by: Fages, François
Published: (2024)

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)

Solvability of Approximate Reach-Avoid Games
by: Gleirscher, Mario
Published: (2025)

Automated Verification of Silq Quantum Programs using SMT Solvers
by: Lewis, Marco, et al.
Published: (2024)

Satisfiability.jl: Satisfiability Modulo Theories in Julia
by: Soroka, Emiko, et al.
Published: (2023)

Varanus: Runtime Verification for CSP
by: Luckcuck, Matt, et al.
Published: (2025)

TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System
by: Dai, Steve, et al.
Published: (2025)

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

Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations
by: Zhang, Changjian, et al.
Published: (2023)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
by: Wojtak, Connor, et al.
Published: (2025)

Smart Contracts Formal Verification: A Systematic Literature Review
by: Davila, Rene, et al.
Published: (2025)

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

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

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
by: Somorjai, Márk, et al.
Published: (2024)

ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
by: Dantas, Pierre, et al.
Published: (2026)

Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
by: Zhang, Yuanrui
Published: (2024)