Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alternative to interpolation.
Maryna Viazovska, Abhinav Kumar
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir