11 citations · 11 across the 2 of their papers we have counts for
2 papers
cs.LO2016
Formula Slicing: Inductive Invariants from Preconditions
Egor George Karpenkov, David Monniaux
We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and ma…
cs.LO2015★ 11 cited
Program Analysis with Local Policy Iteration
George Karpenkov, David Monniaux, Philipp Wendler
We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterati…