14:00‑15:00 FLoC Keynote Talk: Deepak Kapur
Location: George Square Lecture Theatre
| 14:00 | Deepak Kapur (University of New Mexico) Induction, Invariants, and Abstraction Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated. |