Affiliations: Dipartimento di Scienze Politiche, Scienze della Comunicazione e Ingegneria dell'Informazione, Università degli Studi di Sassari, Sassari, Italy. E-mail: lpulina@uniss.it | Dipartimento di Informatica, Sistemistica e Telematica, Università degli Studi di Genova, Genova, Italy. E-mail: armando.tacchella@unige.it
Note: [] Corresponding author: Luca Pulina, Dipartimento di Scienze Politiche, Scienze della Comunicazione e Ingegneria dell'Informazione, Università degli Studi di Sassari, Viale Mancini, 5-07100 Sassari, Italy. E-mail: lpulina@uniss.it.
Abstract: In recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Computer Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulating a record of success stories and, as witnessed by the annual SMT competition, their performances and capacity are also increasing steadily. Introduced in previous contributions of ours, a new application domain providing an outstanding challenge for SMT solvers is represented by verification of Multi-Layer Perceptrons (MLPs) a widely-adopted kind of artificial neural network. In this paper we present an extensive evaluation of the current state-of-the-art SMT solvers and assess their potential in the promising domain of MLP verification.
Keywords: Empirical evaluation of SMT solvers, applications of automated reasoning, formal methods for adaptive systems
