Several approaches toward quantifier-free interpolation algorithms of theories involving arrays have been proposed by extending the language using a binary function skolemizing the extensionality principle. In FoSSaCS 2021, the last three authors studied the enrichment of the McCarthy’s theory of extensional arrays with a maxdiff operation. This paper discusses the implementation of the interpolation algorithm proposed in FoSSaCS 2021 using the Z3 API. The implementation allows the user to choose iZ3, Mathsat, or SMTInterpol as interpolation engines. The tool returns a formula in SMTLIB2 format, which allows compatibility with model checkers and invariant generators using such a format. We compare our algorithm with state-of-the-art interpolation engines. Our experiments using unsatisfiable formulæ extracted with the model checker UAutomizer show the feasibility of our tool. For that purpose, we used C programs from the ReachSafety-Arrays and MemSafety-Arrays tracks of SV-COMP
AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDif / J. Castellanos Joo, S. Ghilardi, A. Gianola, D. Kapur (CEUR WORKSHOP PROCEEDINGS). - In: Satisfiability Modulo Theories 2021 / [a cura di] A. Nadel, A. Niemetz. - [s.l] : CEUR-WS.org, 2021. - pp. 40-52 (( convegno 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021) tenutosi a Los Angeles nel 2021.
|Titolo:||AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDif|
|Parole Chiave:||Interpolation; Arrays; MaxDiff; SMT|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2021|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|