Relational Cell Morphing: Automated Verification of Relational Properties of Array(…)
summary
The system reduces relational verification of array programs to constrained Horn clause solving over scalars by tracking a few distinguished cells across two executions, avoiding array theories and synthesizing a merged asynchronous scheduler. It adds dynamic cell reselection and universally quantified prophecy variables to get tight relational cost bounds parameterized by positions of agreement, and it verifies 65 encodings across 8 property classes in seconds–minutes using PCSat; core technique is relational cell morphing.
AI-written summary · about