Auflistung nach Schlagwort "SMT solver"
1 - 2 von 2
Treffer pro Seite
Sortieroptionen
- ZeitschriftenartikelFunctional verification of cyber-physical systems containing machine-learnt components(it - Information Technology: Vol. 63, No. 4, 2021) Moradkhani, Farzaneh; Fränzle, MartinFunctional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.
- WorkshopbeitragSMT Solvers – A PromisingWay for Verifying User Interfaces?(Mensch und Computer 2022 - Workshopband, 2022) Bruchertseifer, Jens; Weyers, BenjaminEvaluating user interfaces of interactive applications in terms of correctness has always been a lengthy and error-prone task, as it would be executed by humans. This has led to this aspect of development being severely neglected, which poses a fundamental problem in terms of usability. In this work, we present a novel approach based on the creation of a formal representation from a given user interface, which is transformed into a reference net and finally converted into an SMT formula. As SMT formulae can be evaluated easily using highly efficient SMT solvers, this approach promises good efficiency in real-world scenarios.