Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
From MaRDI portal
Publication:832157
DOI10.1007/978-3-030-81685-8_5zbMath1493.68053OpenAlexW3183258024MaRDI QIDQ832157
Reuben N. S. Rowe, Nadia Polikarpova, Ilya Sergey, Hila Peleg, Shachar Itzhaky
Publication date: 25 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_5
Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Uses Software
Cites Work
- Unnamed Item
- A learning-based fact selector for Isabelle/HOL
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Linear logic
- Data structures and program transformation
- Resources, concurrency, and local reasoning
- From syntactic proofs to combinatorial proofs
- Starling: lightweight concurrency verification with views
- The Tactician. A seamless, interactive tactic learner and prover for Coq
- Program synthesis using deduction-guided reinforcement learning
- Automated repair of heap-manipulating programs using deductive synthesis
- Refutation-based synthesis in SMT
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Example-directed synthesis: a type-theoretic interpretation
- Logical relations for fine-grained concurrency
- Bi-Abduction with Pure Properties for Specification Inference
- Recursive proofs for inductive tree data-structures
- Which simple types have a unique inhabitant?
- Caper
- Cyclic proofs of program termination in separation logic
- Scaling Enumerative Program Synthesis via Divide and Conquer
- A Marriage of Rely/Guarantee and Separation Logic
- Deny-Guarantee Reasoning
- A Deductive Approach to Program Synthesis
- Logic Programming with Focusing Proofs in Linear Logic
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Deep Network Guided Proof Search
- TacticToe: Learning to Reason with HOL4 Tactics
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
- Unification nets
- Structuring the verification of heap-manipulating programs
- From program verification to program synthesis
- Local rely-guarantee reasoning
- Formal certification of a compiler back-end or
- Certified assembly programming with embedded code pointers
- Compositional Shape Analysis by Means of Bi-Abduction
- Expressive modular fine-grained concurrency specification
- Impredicative Concurrent Abstract Predicates
- Communicating State Transition Systems for Fine-Grained Concurrent Resources
- Programming Languages and Systems
- Program Logics for Certified Compilers
- Time credits and time receipts in Iris
- Automated synthesis of functional programs with auxiliary functions
