(2018.07.10 15:00pm N222)Deepak Kapur:Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons, ...
Time：2018-07-09 Source：KLMM
Title： Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons, ...
Speaker： Deepak Kapur (University of New Mexico)
Time&Venue： 2018.07.10 15:00pm N222
Abstract:： In a paper in 2006, Kapur, Majumdar and Zarba observed a connection between quantifier elimination and interpolant generation which was probably well-known but not explicitly reported in the literature on automated reasoning and formal methods. Since then I have been investigating how to develop heuristics for quantifier elimination to generate interpolants. Particularly, there is no need to have access to a proof to generate interpolants, a methodology widely used in the formal methods community.
I will start with an interpolant generation algorithm in the quantifier-free theory of equality over uninterpreted symbols. Even though there are many algorithms reported in the literature, there is little investigation about their complexity.Interpolants generated are simple and can be efficiently represented using new symbols defined in terms of common symbols. This is followed by an interpolant generation algorithm for octagonal formulas, which is of complexity O(n^3), where n is the number of variables; an interpolant generated is a conjunction of octagonal formulas. Combination methods for interpolant generation over subtheories can be developed as well. Another interesting outcome is an efficient algorithm for generating congruence closure of conditional equations.
Home
Chinese
Contact
About