Targeted Synthesis for Programming with Data Invariants
John Sarracino, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia, Polikarpova

TL;DR
This paper introduces Targeted Synthesis, a novel compile-time technique for integrating and maintaining data invariants within imperative programs, improving robustness and reducing manual effort.
Contribution
It presents a language co-design approach and a new core calculus, Spyder, enabling invariant support without complex reasoning, and demonstrates its effectiveness on web-inspired programs.
Findings
Spyder efficiently compiles and maintains data invariants.
Supports a language with iterators without requiring quantified reasoning.
Successfully applied to web-inspired imperative programs.
Abstract
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult because the programmer must manually account for all the locations and configurations that break an invariant. Moreover, implicit invariants are brittle under code-evolution: when the invariants and data structures change, the programmer must repeat the process of manually repairing all of the code locations where invariants are violated. A much better approach is to introduce data invariants as a language feature and rely on language support to maintain invariants. To handle this challenge, we introduce Targeted Synthesis, a technique for integrating data invariants with invariant-agnostic imperative code at compile-time. This technique is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Security and Verification in Computing
