ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 11:30 - 12:00 at Skeel - Session 7 Chair(s): Delphine Demange

In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it is guaranteed to eventually find predicates sufficient to prove the property, when such exist. However, existing complete methods require deciding if a proof of the counterexample’s spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs a heavy overhead. We address the issue by showing that the language restriction can be relaxed so that the refinement process is restricted to infer proofs from some finite language. We show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and be complete by restricting only the theory-level reasoning in SMT to emit restricted partial interpolants.

Thu 16 Apr

esop-2015-papers
10:30 - 12:30: ESOP - Session 7 at Skeel
Chair(s): Delphine DemangeIRISA / University of Rennes 1
esop-2015-papers10:30 - 11:00
Talk
Sam LindleyUniversity of Edinburgh, J. Garrett MorrisThe University of Edinburgh
esop-2015-papers11:00 - 11:30
Talk
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford
esop-2015-papers11:30 - 12:00
Talk
Tachio TerauchiJAIST, Hiroshi UnnoUniversity of Tsukuba
esop-2015-papers12:00 - 12:30
Talk
Aws AlbarghouthiUniversity of Wisconsin - Madison, Josh BerdineMicrosoft Research, Byron CookMicrosoft Research, Zachary KincaidUniversity of Toronto