Buchumschlag

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Zhang, Cheng, Fu, Qiancheng, Ji, Hang, Del Valle, Ines Santacruz, Silva, Alexandra, Gaboardi, Marco
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Programming Languages 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

Weighted GKAT: Completeness and Complexity
von: Van Koevering, Spencer, et al.
Veröffentlicht: (2025)

Kleene algebra with commutativity conditions is undecidable
von: de Amorim, Arthur Azevedo, et al.
Veröffentlicht: (2024)

Domain Reasoning in TopKAT
von: Zhang, Cheng, et al.
Veröffentlicht: (2024)

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

Denotational Semantics for Probabilistic and Concurrent Programs
von: Zilberstein, Noam, et al.
Veröffentlicht: (2025)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
von: Zilberstein, Noam, et al.
Veröffentlicht: (2023)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
von: Kappé, Tobias, et al.
Veröffentlicht: (2023)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
von: Zilberstein, Noam, et al.
Veröffentlicht: (2024)

A Demonic Outcome Logic for Randomized Nondeterminism
von: Zilberstein, Noam, et al.
Veröffentlicht: (2024)

A Probabilistic Choreography Language for PRISM
von: Carbone, Marco, et al.
Veröffentlicht: (2025)

Verifying Functional Correctness Properties At the Level of Java Bytecode
von: Paganoni, Marco, et al.
Veröffentlicht: (2024)

Reasoning About Exceptional Behavior At the Level of Java Bytecode
von: Paganoni, Marco, et al.
Veröffentlicht: (2024)

Equational Bit-Vector Solving via Strong Gröbner Bases
von: Song, Jiaxin, et al.
Veröffentlicht: (2024)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
von: Montesi, Fabrizio, et al.
Veröffentlicht: (2026)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
von: Batz, Kevin, et al.
Veröffentlicht: (2024)

Symmetric Proofs of Parameterized Programs
von: Cheng, Ruotong, et al.
Veröffentlicht: (2026)

Complete Local Reasoning About Parameterized Programs Over Topologies
von: Cheng, Ruotong, et al.
Veröffentlicht: (2026)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
von: Cheng, Ruotong, et al.
Veröffentlicht: (2025)

Leveraging Large Language Models to Boost Dafny's Developers Productivity
von: Silva, Álvaro, et al.
Veröffentlicht: (2024)

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

Towards a Higher-Order Bialgebraic Denotational Semantics
von: Goncharov, Sergey, et al.
Veröffentlicht: (2026)

A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes
von: Różowski, Wojciech, et al.
Veröffentlicht: (2026)

A programming language characterizing quantum polynomial time
von: Hainry, Emmanuel, et al.
Veröffentlicht: (2022)

Quantum Programming in Polylogarithmic Time
von: Ferrari, Florent, et al.
Veröffentlicht: (2025)

A feasible and unitary quantum programming language
von: Díaz-Caro, Alejandro, et al.
Veröffentlicht: (2023)

The Decision Problem for Regular First-Order Theories
von: Mathur, Umang, et al.
Veröffentlicht: (2024)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
von: Judson, Samuel, et al.
Veröffentlicht: (2023)

CF-GKAT: Efficient Validation of Control-Flow Transformations
von: Zhang, Cheng, et al.
Veröffentlicht: (2024)

Inferring multiple helper Dafny assertions with LLMs
von: Silva, Álvaro, et al.
Veröffentlicht: (2025)

Contract Usage and Evolution in Android Mobile Applications
von: Ferreira, David R., et al.
Veröffentlicht: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
von: Kaye, George
Veröffentlicht: (2025)

Impredicativity in Linear Dependent Type Theory
von: Speight, Sam, et al.
Veröffentlicht: (2026)

Internalizing Representation Independence with Univalence
von: Angiuli, Carlo, et al.
Veröffentlicht: (2020)

Crash-Stop Failures in Asynchronous Multiparty Session Types
von: Barwell, Adam D., et al.
Veröffentlicht: (2023)

Structural Temporal Logic for Mechanized Program Verification
von: Ioannidis, Eleftherios, et al.
Veröffentlicht: (2024)

Positive Sharing and Abstract Machines
von: Accattoli, Beniamino, et al.
Veröffentlicht: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
von: Grandury, Marcos, et al.
Veröffentlicht: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
von: Kobayashi, Kentaro, et al.
Veröffentlicht: (2025)

CSLib: The Lean Computer Science Library
von: Barrett, Clark, et al.
Veröffentlicht: (2026)

Recursive Mutexes in Separation Logic
von: Du, Ke, et al.
Veröffentlicht: (2026)