CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishInterpolants are used in program analysis, verification and synthesis, to compute over-approximations of images, refine abstractions, or generate invariants. An interpolation system takes a proof and extracts an interpolant. Known interpolation systems use colors to track symbols in proofs. We give a color-based interpolation system for ground superposition, and then we show that the color-based approach cannot handle non-ground proofs with substitutions. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to obtain an interpolant. In this way we get interpolation systems for non-ground proofs by superposition and resolution.
| Titolo: | Two-stage interpolation systems |
| Autori: | |
| Data di pubblicazione: | 2013 |
| Abstract: | Interpolants are used in program analysis, verification and synthesis, to compute over-approximations of images, refine abstractions, or generate invariants. An interpolation system takes a proof and extracts an interpolant. Known interpolation systems use colors to track symbols in proofs. We give a color-based interpolation system for ground superposition, and then we show that the color-based approach cannot handle non-ground proofs with substitutions. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to obtain an interpolant. In this way we get interpolation systems for non-ground proofs by superposition and resolution. |
| Handle: | http://hdl.handle.net/11562/611552 |
| Appare nelle tipologie: | 04.02 Abstract in Atti di convegno |
File in questo prodotto:
Copyright © 2020