A Modular Program-Transformation Framework for Reducing Specifications to Reachability
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | Beyer, Dirk, Jankola, Marek, Lingsch-Rosenfeld, Marian, Xia, Tian, Zheng, Xiyue |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
Ähnliche Einträge
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
von: Beyer, Dirk, et al.
Veröffentlicht: (2025)
von: Beyer, Dirk, et al.
Veröffentlicht: (2025)
Correctness Witnesses with Function Contracts
von: Heizmann, Matthias, et al.
Veröffentlicht: (2025)
von: Heizmann, Matthias, et al.
Veröffentlicht: (2025)
Non-termination Witnesses in Format 2.1 for ASE 2025 Article `Non-termination Witnesses and Their Validation'
von: Ádám, Zsófia, et al.
Veröffentlicht: (2025)
von: Ádám, Zsófia, et al.
Veröffentlicht: (2025)
Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
von: Baier, Daniel, et al.
Veröffentlicht: (2024)
von: Baier, Daniel, et al.
Veröffentlicht: (2024)
Resource Specifications for Resource-Manipulating Programs
von: Grannan, Zachary, et al.
Veröffentlicht: (2023)
von: Grannan, Zachary, et al.
Veröffentlicht: (2023)
Deep R Programming
von: Gagolewski, Marek
Veröffentlicht: (2022)
von: Gagolewski, Marek
Veröffentlicht: (2022)
MLIR-Forge: A Modular Framework for Language Smiths
von: Ates, Berke, et al.
Veröffentlicht: (2026)
von: Ates, Berke, et al.
Veröffentlicht: (2026)
Modeling Reachability Types with Logical Relations
von: Bao, Yuyan, et al.
Veröffentlicht: (2023)
von: Bao, Yuyan, et al.
Veröffentlicht: (2023)
On Higher-Order Reachability Games vs May Reachability
von: Asada, Kazuyuki, et al.
Veröffentlicht: (2022)
von: Asada, Kazuyuki, et al.
Veröffentlicht: (2022)
Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis
von: Yao, Peisen, et al.
Veröffentlicht: (2026)
von: Yao, Peisen, et al.
Veröffentlicht: (2026)
Synthesizing Abstract Transformers for Reduced-Product Domains
von: Kalita, Pankaj Kumar, et al.
Veröffentlicht: (2024)
von: Kalita, Pankaj Kumar, et al.
Veröffentlicht: (2024)
MoTCoder: Elevating Large Language Models with Modular of Thought for Challenging Programming Tasks
von: Li, Jingyao, et al.
Veröffentlicht: (2023)
von: Li, Jingyao, et al.
Veröffentlicht: (2023)
Functional Logic Program Transformations
von: Hanus, Michael, et al.
Veröffentlicht: (2026)
von: Hanus, Michael, et al.
Veröffentlicht: (2026)
Pathological Cases for a Class of Reachability-Based Garbage Collectors
von: Sotoudeh, Matthew
Veröffentlicht: (2025)
von: Sotoudeh, Matthew
Veröffentlicht: (2025)
Optimization of the Context-Free Language Reachability Matrix-Based Algorithm
von: Muravev, Ilia
Veröffentlicht: (2024)
von: Muravev, Ilia
Veröffentlicht: (2024)
Oracular Programming: A Modular Foundation for Building LLM-Enabled Software
von: Laurent, Jonathan, et al.
Veröffentlicht: (2025)
von: Laurent, Jonathan, et al.
Veröffentlicht: (2025)
Challenges of Multilingual Program Specification and Analysis
von: Furia, Carlo A., et al.
Veröffentlicht: (2024)
von: Furia, Carlo A., et al.
Veröffentlicht: (2024)
Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
von: Ciccalè, Marco, et al.
Veröffentlicht: (2025)
von: Ciccalè, Marco, et al.
Veröffentlicht: (2025)
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
von: Young, David, et al.
Veröffentlicht: (2024)
von: Young, David, et al.
Veröffentlicht: (2024)
Program Analysis via Multiple Context Free Language Reachability
von: Conrado, Giovanna Kobus, et al.
Veröffentlicht: (2024)
von: Conrado, Giovanna Kobus, et al.
Veröffentlicht: (2024)
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
von: He, Siyuan, et al.
Veröffentlicht: (2025)
von: He, Siyuan, et al.
Veröffentlicht: (2025)
Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
von: Foo, Darius, et al.
Veröffentlicht: (2023)
von: Foo, Darius, et al.
Veröffentlicht: (2023)
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
von: Jia, Songlin, et al.
Veröffentlicht: (2024)
von: Jia, Songlin, et al.
Veröffentlicht: (2024)
Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
von: Deng, Haotian, et al.
Veröffentlicht: (2025)
von: Deng, Haotian, et al.
Veröffentlicht: (2025)
Transformers for Program Termination
von: Alon, Yoav, et al.
Veröffentlicht: (2026)
von: Alon, Yoav, et al.
Veröffentlicht: (2026)
Validating Traces of Distributed Programs Against TLA+ Specifications
von: Cirstea, Horatiu, et al.
Veröffentlicht: (2024)
von: Cirstea, Horatiu, et al.
Veröffentlicht: (2024)
A Note on Dynamic Bidirected Dyck-Reachability with Cycles
von: Zhang, Qirun
Veröffentlicht: (2024)
von: Zhang, Qirun
Veröffentlicht: (2024)
Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
von: Xia, Shihao, et al.
Veröffentlicht: (2026)
von: Xia, Shihao, et al.
Veröffentlicht: (2026)
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
von: Beyer, Dirk, et al.
Veröffentlicht: (2022)
von: Beyer, Dirk, et al.
Veröffentlicht: (2022)
DriftScript: A Domain-Specific Language for Programming Non-Axiomatic Reasoning Agents
von: Brady, Seamus
Veröffentlicht: (2026)
von: Brady, Seamus
Veröffentlicht: (2026)
Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
von: Wu, Valentina, et al.
Veröffentlicht: (2025)
von: Wu, Valentina, et al.
Veröffentlicht: (2025)
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
von: Li, Kwing Hei, et al.
Veröffentlicht: (2025)
von: Li, Kwing Hei, et al.
Veröffentlicht: (2025)
The Master-Slave Encoder Model for Improving Patent Text Summarization: A New Approach to Combining Specifications and Claims
von: Zhou, Shu, et al.
Veröffentlicht: (2024)
von: Zhou, Shu, et al.
Veröffentlicht: (2024)
Mapple: A Domain-Specific Language for Mapping Distributed Programs
von: Wei, Anjiang, et al.
Veröffentlicht: (2025)
von: Wei, Anjiang, et al.
Veröffentlicht: (2025)
Pyrosome: Verified Compilation for Modular Metatheory
von: Jamner, Dustin, et al.
Veröffentlicht: (2025)
von: Jamner, Dustin, et al.
Veröffentlicht: (2025)
Compilation of Modular and General Sparse Workspaces
von: Zhang, Genghan, et al.
Veröffentlicht: (2024)
von: Zhang, Genghan, et al.
Veröffentlicht: (2024)
Minuska: Towards a Formally Verified Programming Language Framework
von: Tušil, Jan, et al.
Veröffentlicht: (2024)
von: Tušil, Jan, et al.
Veröffentlicht: (2024)
JoinActors: A Modular Library for Actors with Join Patterns
von: Hussein, Ayman, et al.
Veröffentlicht: (2026)
von: Hussein, Ayman, et al.
Veröffentlicht: (2026)
A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification
von: Marron, Assaf, et al.
Veröffentlicht: (2025)
von: Marron, Assaf, et al.
Veröffentlicht: (2025)
Memory Consistency and Program Transformations
von: Gopalakrishnan, Akshay, et al.
Veröffentlicht: (2024)
von: Gopalakrishnan, Akshay, et al.
Veröffentlicht: (2024)
Ähnliche Einträge
-
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
von: Beyer, Dirk, et al.
Veröffentlicht: (2025) -
Correctness Witnesses with Function Contracts
von: Heizmann, Matthias, et al.
Veröffentlicht: (2025) -
Non-termination Witnesses in Format 2.1 for ASE 2025 Article `Non-termination Witnesses and Their Validation'
von: Ádám, Zsófia, et al.
Veröffentlicht: (2025) -
Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
von: Baier, Daniel, et al.
Veröffentlicht: (2024) -
Resource Specifications for Resource-Manipulating Programs
von: Grannan, Zachary, et al.
Veröffentlicht: (2023)