Keyword:inductive invariant

Papers
Towards an Automatic Proof of Lamport's Paxos Aman Goel and Karem A. Sakallah EasyChair Preprint no. 6510
Synchronizing Constrained Horn Clauses Dmitry Mordvinov and Grigory Fedyukovich In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning