Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

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

Mathematics Subject Classification ID

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

• Chalice
• VeriFast
• Toolchain
• Mezzo
• Viper
• Fiat
• Rust
• RustBelt

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