Instantiation Schemes for Nested Theories

07/25/2011
by   Mnacho Echenim, et al.
0

This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset