Imagen de Portada

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Zhang, Cheng, Fu, Qiancheng, Ji, Hang, Del Valle, Ines Santacruz, Silva, Alexandra, Gaboardi, Marco
Formato:	Preprint
Publicado:	2026
Materias:	Programming Languages Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Weighted GKAT: Completeness and Complexity
por: Van Koevering, Spencer, et al.
Publicado: (2025)

Kleene algebra with commutativity conditions is undecidable
por: de Amorim, Arthur Azevedo, et al.
Publicado: (2024)

Domain Reasoning in TopKAT
por: Zhang, Cheng, et al.
Publicado: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
por: Wang, Keyin, et al.
Publicado: (2026)

Denotational Semantics for Probabilistic and Concurrent Programs
por: Zilberstein, Noam, et al.
Publicado: (2025)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
por: Zilberstein, Noam, et al.
Publicado: (2023)

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

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
por: Zilberstein, Noam, et al.
Publicado: (2024)

A Demonic Outcome Logic for Randomized Nondeterminism
por: Zilberstein, Noam, et al.
Publicado: (2024)

A Probabilistic Choreography Language for PRISM
por: Carbone, Marco, et al.
Publicado: (2025)

Verifying Functional Correctness Properties At the Level of Java Bytecode
por: Paganoni, Marco, et al.
Publicado: (2024)

Reasoning About Exceptional Behavior At the Level of Java Bytecode
por: Paganoni, Marco, et al.
Publicado: (2024)

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

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
por: Montesi, Fabrizio, et al.
Publicado: (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)
por: Batz, Kevin, et al.
Publicado: (2024)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

Complete Local Reasoning About Parameterized Programs Over Topologies
por: Cheng, Ruotong, et al.
Publicado: (2026)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
por: Cheng, Ruotong, et al.
Publicado: (2025)

Leveraging Large Language Models to Boost Dafny's Developers Productivity
por: Silva, Álvaro, et al.
Publicado: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
por: Monniaux, David
Publicado: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
por: Goncharov, Sergey, et al.
Publicado: (2026)

A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes
por: Różowski, Wojciech, et al.
Publicado: (2026)

A programming language characterizing quantum polynomial time
por: Hainry, Emmanuel, et al.
Publicado: (2022)

Quantum Programming in Polylogarithmic Time
por: Ferrari, Florent, et al.
Publicado: (2025)

A feasible and unitary quantum programming language
por: Díaz-Caro, Alejandro, et al.
Publicado: (2023)

The Decision Problem for Regular First-Order Theories
por: Mathur, Umang, et al.
Publicado: (2024)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
por: Judson, Samuel, et al.
Publicado: (2023)

CF-GKAT: Efficient Validation of Control-Flow Transformations
por: Zhang, Cheng, et al.
Publicado: (2024)

Inferring multiple helper Dafny assertions with LLMs
por: Silva, Álvaro, et al.
Publicado: (2025)

Contract Usage and Evolution in Android Mobile Applications
por: Ferreira, David R., et al.
Publicado: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
por: Kaye, George
Publicado: (2025)

Impredicativity in Linear Dependent Type Theory
por: Speight, Sam, et al.
Publicado: (2026)

Internalizing Representation Independence with Univalence
por: Angiuli, Carlo, et al.
Publicado: (2020)

Crash-Stop Failures in Asynchronous Multiparty Session Types
por: Barwell, Adam D., et al.
Publicado: (2023)

Structural Temporal Logic for Mechanized Program Verification
por: Ioannidis, Eleftherios, et al.
Publicado: (2024)

Positive Sharing and Abstract Machines
por: Accattoli, Beniamino, et al.
Publicado: (2025)

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

Expressive Power of One-Shot Control Operators and Coroutines
por: Kobayashi, Kentaro, et al.
Publicado: (2025)

CSLib: The Lean Computer Science Library
por: Barrett, Clark, et al.
Publicado: (2026)

Recursive Mutexes in Separation Logic
por: Du, Ke, et al.
Publicado: (2026)