Buchumschlag

Formally Verified Animation for RoboChart using Interaction Trees

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Ye, Kangfeng, Foster, Simon, Woodcock, Jim
Format:	Preprint
Veröffentlicht:	2023
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

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

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

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
von: Bryant, Dustin, et al.
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)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
von: Foster, Simon, et al.
Veröffentlicht: (2024)

User-Guided Verification of Security Protocols via Sound Animation
von: Ye, Kangfeng, et al.
Veröffentlicht: (2024)

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

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
von: Monniaux, David
Veröffentlicht: (2024)

A Formally Verified Lightning Network
von: Fabiański, Grzegorz, et al.
Veröffentlicht: (2025)

Formally Verified Approximate Policy Iteration
von: Schäffeler, Maximilian, et al.
Veröffentlicht: (2024)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
von: Dvorak, Martin, et al.
Veröffentlicht: (2025)

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
von: Kohlen, Bram, et al.
Veröffentlicht: (2025)

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

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
von: Bryce, Aaron, et al.
Veröffentlicht: (2026)

A Formally Verified Procedure for Width Inference in FIRRTL
von: Wang, Keyin, et al.
Veröffentlicht: (2026)

Formally Verified Certification of Unsolvability of Temporal Planning Problems
von: Wang, David, et al.
Veröffentlicht: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
von: Guilloud, Simon, et al.
Veröffentlicht: (2025)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
von: Bryant, Randal E., et al.
Veröffentlicht: (2025)

Relational semantics for flat Heyting-Lewis Logic
von: de Groot, Jim, et al.
Veröffentlicht: (2026)

Filling in the semantics for intuitionistic conditional logic
von: Dufty, Brendan, et al.
Veröffentlicht: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
von: Coglio, Alessandro, et al.
Veröffentlicht: (2025)

Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
von: Govindankutty, Arun, et al.
Veröffentlicht: (2026)

Verifying SQL Queries using Theories of Tables and Relations
von: Mohamed, Mudathir, et al.
Veröffentlicht: (2024)

Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
von: de Groot, Jim, et al.
Veröffentlicht: (2021)

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
von: de Groot, Jim, et al.
Veröffentlicht: (2026)

Intrinsic and relative characterization results for logics with negative modalities
von: de Groot, Jim, et al.
Veröffentlicht: (2025)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK
von: de Groot, Jim, et al.
Veröffentlicht: (2024)

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

Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids
von: Dvorak, Martin
Veröffentlicht: (2026)

Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
von: Farjami, Ali, et al.
Veröffentlicht: (2026)

Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
von: Govindankutty, Arun
Veröffentlicht: (2026)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
von: Ileri, Atalay Mert, et al.
Veröffentlicht: (2024)

A Survey of Interactive Verifiable Computing: Utilizing Low-degree Polynomials
von: Wang, Angold
Veröffentlicht: (2025)

Causal-Temporal Event Graphs: A Formal Model for Recursive Agent Execution Traces
von: Foldvik, Simon
Veröffentlicht: (2026)

Satisfiability Modulo Theories for Verifying MILP Certificates
von: Wood, Kenan, et al.
Veröffentlicht: (2023)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
von: Lee, Jaeseo, et al.
Veröffentlicht: (2025)

Wait-Only Broadcast Protocols are Easier to Verify
von: Guillou, Lucie, et al.
Veröffentlicht: (2025)

Formalizing equivalences without tears
von: de Jong, Tom
Veröffentlicht: (2024)

Formalization of Amicable Numbers Theory
von: Chen, Zhipeng, et al.
Veröffentlicht: (2026)