Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
From MaRDI portal
Publication:5041091
DOI10.1007/978-3-030-44914-8_6MaRDI QIDQ5041091
Ilya Sergey, Andreea Costea, Amy Zhu, Nadia Polikarpova
Publication date: 13 October 2022
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2001.10723
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Automated repair of heap-manipulating programs using deductive synthesis
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Look for the proof to find the program: decorated-component-based program synthesis
- Logical reasoning for disjoint permissions
- Automating deductive verification for weak-memory programs
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Fiat
- A type system for borrowing permissions
- Temporary Read-Only Permissions for Separation Logic
- Verified Software Toolchain
- A Basis for Verifying Multi-threaded Programs
- A Deductive Approach to Program Synthesis
- Type Soundness and Race Freedom for Mezzo
- From program verification to program synthesis
- Permission accounting in separation logic
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Programming Languages and Systems