Instantiation Schemes for Nested Theories

This article 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...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2013-06, Vol.14 (2), p.1-34
Main Authors: Echenim, Mnacho, Peltier, Nicolas
Format: Article
Language:English
Subjects:
Arrays
Computer Science
Logic in Computer Science
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This article 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.
ISSN:1529-3785
1557-945X
DOI:10.1145/2480759.2480763