Imagen de Portada

An Encoding for CLP Problems in SMT-LIB

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Amrollahi, Daneshvar, Hojjat, Hossein, Rümmer, Philipp
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

An SMT-LIB Theory of Finite Fields
por: Hader, Thomas, et al.
Publicado: (2024)

Towards SMT Solver Stability via Input Normalization
por: Amrollahi, Daneshvar, et al.
Publicado: (2024)

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

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
por: Bharti, Varun, et al.
Publicado: (2025)

Craig Interpolation in Program Verification
por: Rümmer, Philipp
Publicado: (2026)

Verifying Solutions to Semantics-Guided Synthesis Problems
por: Murphy, Charlie, et al.
Publicado: (2024)

Almost-Sure Termination by Guarded Refinement
por: Gregersen, Simon Oddershede, et al.
Publicado: (2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
por: Haselwarter, Philipp G., et al.
Publicado: (2024)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
por: Li, Kwing Hei, et al.
Publicado: (2025)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
por: Haselwarter, Philipp G., et al.
Publicado: (2026)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
por: Aguirre, Alejandro, et al.
Publicado: (2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
por: Haselwarter, Philipp G., et al.
Publicado: (2024)

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

Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems
por: Mendez, Julian Alfredo
Publicado: (2023)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
por: Jiang, Hongjian, et al.
Publicado: (2025)

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

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
por: Civini, Emanuele, et al.
Publicado: (2026)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
por: Esen, Zafer, et al.
Publicado: (2025)

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
por: Anand, Ashwani, et al.
Publicado: (2026)

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)

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

An Introduction to Different Approaches to Initial Semantics
por: Lamiaux, Thomas, et al.
Publicado: (2024)

More Church-Rosser Proofs in BELUGA
por: Momigliano, Alberto, et al.
Publicado: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
por: Goncharov, Sergey, et al.
Publicado: (2024)

A Nominal Approach to Probabilistic Separation Logic
por: Li, John M., et al.
Publicado: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
por: Beutner, Raven, et al.
Publicado: (2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
por: Hu, Jason Z. S., et al.
Publicado: (2024)

Hybrid Intersection Types for PCF (Extended Version)
por: Barenbaum, Pablo, et al.
Publicado: (2024)

Verifying Lock-free Search Structure Templates
por: Patel, Nisarg, et al.
Publicado: (2024)

Functional Array Programming in an Extended Pi-Calculus
por: Hüttel, Hans, et al.
Publicado: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
por: Pincus, Jared, et al.
Publicado: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
por: Verscht, Lena, et al.
Publicado: (2024)

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

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
por: Jang, Junyoung, et al.
Publicado: (2024)

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
por: Accattoli, Beniamino
Publicado: (2024)

Useful Evaluation: Syntax and Semantics (Technical Report)
por: Barenbaum, Pablo, et al.
Publicado: (2024)

Linear Contextual Metaprogramming and Session Types
por: Ângelo, Pedro, et al.
Publicado: (2024)

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

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
por: Soldevila, Mallku, et al.
Publicado: (2024)