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
Times are displayed in time zone: (GMT) Azores change

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