Cover Image

A Modular Program-Transformation Framework for Reducing Specifications to Reachability

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Beyer, Dirk, Jankola, Marek, Lingsch-Rosenfeld, Marian, Xia, Tian, Zheng, Xiyue
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
by: Beyer, Dirk, et al.
Published: (2025)

Correctness Witnesses with Function Contracts
by: Heizmann, Matthias, et al.
Published: (2025)

Non-termination Witnesses in Format 2.1 for ASE 2025 Article `Non-termination Witnesses and Their Validation'
by: Ádám, Zsófia, et al.
Published: (2025)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

Resource Specifications for Resource-Manipulating Programs
by: Grannan, Zachary, et al.
Published: (2023)

Deep R Programming
by: Gagolewski, Marek
Published: (2022)

MLIR-Forge: A Modular Framework for Language Smiths
by: Ates, Berke, et al.
Published: (2026)

Modeling Reachability Types with Logical Relations
by: Bao, Yuyan, et al.
Published: (2023)

On Higher-Order Reachability Games vs May Reachability
by: Asada, Kazuyuki, et al.
Published: (2022)

Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis
by: Yao, Peisen, et al.
Published: (2026)

Synthesizing Abstract Transformers for Reduced-Product Domains
by: Kalita, Pankaj Kumar, et al.
Published: (2024)

MoTCoder: Elevating Large Language Models with Modular of Thought for Challenging Programming Tasks
by: Li, Jingyao, et al.
Published: (2023)

Functional Logic Program Transformations
by: Hanus, Michael, et al.
Published: (2026)

Pathological Cases for a Class of Reachability-Based Garbage Collectors
by: Sotoudeh, Matthew
Published: (2025)

Optimization of the Context-Free Language Reachability Matrix-Based Algorithm
by: Muravev, Ilia
Published: (2024)

Oracular Programming: A Modular Foundation for Building LLM-Enabled Software
by: Laurent, Jonathan, et al.
Published: (2025)

Challenges of Multilingual Program Specification and Analysis
by: Furia, Carlo A., et al.
Published: (2024)

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
by: Ciccalè, Marco, et al.
Published: (2025)

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
by: Young, David, et al.
Published: (2024)

Program Analysis via Multiple Context Free Language Reachability
by: Conrado, Giovanna Kobus, et al.
Published: (2024)

When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
by: He, Siyuan, et al.
Published: (2025)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
by: Foo, Darius, et al.
Published: (2023)

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
by: Jia, Songlin, et al.
Published: (2024)

Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
by: Deng, Haotian, et al.
Published: (2025)

Transformers for Program Termination
by: Alon, Yoav, et al.
Published: (2026)

Validating Traces of Distributed Programs Against TLA+ Specifications
by: Cirstea, Horatiu, et al.
Published: (2024)

A Note on Dynamic Bidirected Dyck-Reachability with Cycles
by: Zhang, Qirun
Published: (2024)

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
by: Xia, Shihao, et al.
Published: (2026)

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
by: Beyer, Dirk, et al.
Published: (2022)

DriftScript: A Domain-Specific Language for Programming Non-Axiomatic Reasoning Agents
by: Brady, Seamus
Published: (2026)

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
by: Wu, Valentina, et al.
Published: (2025)

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

The Master-Slave Encoder Model for Improving Patent Text Summarization: A New Approach to Combining Specifications and Claims
by: Zhou, Shu, et al.
Published: (2024)

Mapple: A Domain-Specific Language for Mapping Distributed Programs
by: Wei, Anjiang, et al.
Published: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
by: Jamner, Dustin, et al.
Published: (2025)

Compilation of Modular and General Sparse Workspaces
by: Zhang, Genghan, et al.
Published: (2024)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

JoinActors: A Modular Library for Actors with Join Patterns
by: Hussein, Ayman, et al.
Published: (2026)

A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification
by: Marron, Assaf, et al.
Published: (2025)

Memory Consistency and Program Transformations
by: Gopalakrishnan, Akshay, et al.
Published: (2024)