Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this thesis, we tackle the problems of SMT and VMT over the theories of polynomials over the reals (NRA), over the integers (NIA), and of NRA augmented with transcendental functions (NTA). We propose a new abstraction-refinement approach called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract domain limited to linear arithmetic with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver, and in the nuXmv VMT model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach. Moreover, the proposed technique is an enabler for the (nonlinear) VMT problems arising in practical scenarios with design environments such as Simulink. This capability has been achieved by integrating nuXmv with Simulink using a compilation-based approach and is evaluated on an industrial-level case study.

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions / Irfan, Ahmed. - (2018), pp. 1-238.

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

Irfan, Ahmed
2018-01-01

Abstract

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this thesis, we tackle the problems of SMT and VMT over the theories of polynomials over the reals (NRA), over the integers (NIA), and of NRA augmented with transcendental functions (NTA). We propose a new abstraction-refinement approach called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract domain limited to linear arithmetic with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver, and in the nuXmv VMT model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach. Moreover, the proposed technique is an enabler for the (nonlinear) VMT problems arising in practical scenarios with design environments such as Simulink. This capability has been achieved by integrating nuXmv with Simulink using a compilation-based approach and is evaluated on an industrial-level case study.
2018
XXIX
2018-2019
Ingegneria e scienza dell'Informaz (29/10/12-)
Information and Communication Technology
Cimatti, Alessandro
Sebastiani, Roberto
Griggio, Alberto
no
Inglese
Settore INF/01 - Informatica
Settore MAT/02 - Algebra
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
Settore MAT/01 - Logica Matematica
File in questo prodotto:
File Dimensione Formato  
thesis.pdf

accesso aperto

Tipologia: Tesi di dottorato (Doctoral Thesis)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 10.15 MB
Formato Adobe PDF
10.15 MB Adobe PDF Visualizza/Apri
declaration.pdf

Solo gestori archivio

Tipologia: Tesi di dottorato (Doctoral Thesis)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.02 MB
Formato Adobe PDF
1.02 MB 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/368604
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact