In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions, and are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear functions. Suitable numerical techniques are used to ensure that the abstractions of the transcendental functions are sound even in presence of irrationals. Our experimental evaluation on benchmarks from verification and mathematics demonstrates the potential of our approach, showing that it compares favorably with delta-satisfiability/interval propagation and methods based on theorem proving.

Satisfiability Modulo Transcendental Functions via Incremental Linearization / Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto. - 10395:(2017), pp. 95-113. (Intervento presentato al convegno International Conference on Automated Deduction (CADE) tenutosi a Gothenburg,Sweden nel 6-11 August 2017) [10.1007/978-3-319-63046-5_7].

Satisfiability Modulo Transcendental Functions via Incremental Linearization

Cimatti, Alessandro;Griggio, Alberto;Irfan, Ahmed;Roveri, Marco;Sebastiani, Roberto
2017-01-01

Abstract

In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions, and are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear functions. Suitable numerical techniques are used to ensure that the abstractions of the transcendental functions are sound even in presence of irrationals. Our experimental evaluation on benchmarks from verification and mathematics demonstrates the potential of our approach, showing that it compares favorably with delta-satisfiability/interval propagation and methods based on theorem proving.
2017
Automated Deduction – CADE 26
Cham, Svizzera
Springer
978-3-319-63045-8
978-3-319-63046-5
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
Satisfiability Modulo Transcendental Functions via Incremental Linearization / Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto. - 10395:(2017), pp. 95-113. (Intervento presentato al convegno International Conference on Automated Deduction (CADE) tenutosi a Gothenburg,Sweden nel 6-11 August 2017) [10.1007/978-3-319-63046-5_7].
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 356.5 kB
Formato Adobe PDF
356.5 kB Adobe PDF Visualizza/Apri

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/11572/181489
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 11
social impact