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.

AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDif

S. Ghilardi;
2021

Abstract

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
Interpolation; Arrays; MaxDiff; SMT
Settore INF/01 - Informatica
2021
http://ceur-ws.org/Vol-2908/paper15.pdf
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
SMT_2021_paper_15.pdf

accesso riservato

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 321.57 kB
Formato Adobe PDF
321.57 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
paper15.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 1.17 MB
Formato Adobe PDF
1.17 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/862711
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact