Buchumschlag

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Foster, Simon, Hur, Chung-Kil, Woodcock, Jim
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Brownian Motion in Isabelle/HOL
von: Laursen, Christian Pardillo, et al.
Veröffentlicht: (2024)

Verifying Numerical Methods with Isabelle/HOL
von: Bryant, Dustin, et al.
Veröffentlicht: (2025)

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

Formally Verified Animation for RoboChart using Interaction Trees
von: Ye, Kangfeng, et al.
Veröffentlicht: (2023)

Linear Programming in Isabelle/HOL
von: Parsert, Julian
Veröffentlicht: (2024)

Complex Bounded Operators in Isabelle/HOL
von: Unruh, Dominique, et al.
Veröffentlicht: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
von: Bartl, Lukas, et al.
Veröffentlicht: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
von: Guzman, Laura P. Gamboa, et al.
Veröffentlicht: (2024)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
von: Bryant, Dustin, et al.
Veröffentlicht: (2025)

Formalization of Differential Privacy in Isabelle/HOL
von: Sato, Tetsuya, et al.
Veröffentlicht: (2024)

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

Munkres' General Topology Autoformalized in Isabelle/HOL
von: Bryant, Dustin, et al.
Veröffentlicht: (2026)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
von: Ye, Kangfeng, et al.
Veröffentlicht: (2023)

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

Coco: Corecursion with Compositional Heterogeneous Productivity
von: Kim, Jaewoo, et al.
Veröffentlicht: (2025)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
von: Schmoetten, Richard, et al.
Veröffentlicht: (2024)

RoboCertProb: Property Specification for Probabilistic RoboChart Models
von: Ye, Kangfeng, et al.
Veröffentlicht: (2024)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
von: Linzi, Alessandro
Veröffentlicht: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
von: Binder, Sage, et al.
Veröffentlicht: (2024)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
von: Binder, Sage, et al.
Veröffentlicht: (2026)

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

Practical Deductive Verification of OCaml Programs (Extended Version)
von: Pereira, Mário
Veröffentlicht: (2024)

AutoDeduct: A Tool for Automated Deductive Verification of C Code
von: Amilon, Jesper, et al.
Veröffentlicht: (2025)

Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
von: Bilotta, Antonella
Veröffentlicht: (2025)

Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)
von: Ye, Kangfeng, et al.
Veröffentlicht: (2025)

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
von: Şakar, Ömer, et al.
Veröffentlicht: (2026)

Context, Judgement, Deduction
von: Coraglia, Greta, et al.
Veröffentlicht: (2021)

HaliVer: Deductive Verification and Scheduling Languages Join Forces
von: Haak, Lars B. van den, et al.
Veröffentlicht: (2024)

Cut-free Deductive System for Continuous Intuitionistic Logic
von: Geoffroy, Guillaume
Veröffentlicht: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
von: Kosaian, Katherine, et al.
Veröffentlicht: (2024)

Small Decision Trees for MDPs with Deductive Synthesis
von: Andriushchenko, Roman, et al.
Veröffentlicht: (2025)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
von: Elad, Neta, et al.
Veröffentlicht: (2023)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
von: Kammüller, Florian
Veröffentlicht: (2023)

Mechanized HOL Reasoning in Set Theory
von: Guilloud, Simon, et al.
Veröffentlicht: (2024)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
von: Batz, Kevin, et al.
Veröffentlicht: (2025)

Proof Recommendation System for the HOL4 Theorem Prover
von: Dekhil, Nour, et al.
Veröffentlicht: (2024)

Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
von: Huch, Fabian
Veröffentlicht: (2024)

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA
von: Palmskog, Karl, et al.
Veröffentlicht: (2025)

Intuitionistic monotone modal logic via translation
von: de Groot, Jim
Veröffentlicht: (2025)

A Deductive Refinement Calculus for Differential-Algebraic Programs
von: Hellwig, Jonathan, et al.
Veröffentlicht: (2026)