Zobrazeno 1 - 10
of 37
pro vyhledávání: '"BRAUSSE, FRANZ"'
Autor:
Li, Xianzhiyu, Song, Kunjian, Gadelha, Mikhail R., Brauße, Franz, Menezes, Rafael S., Korovin, Konstantin, Cordeiro, Lucas C.
This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by mode
Externí odkaz:
http://arxiv.org/abs/2406.17862
SMLP: Symbolic Machine Learning Prover an open source tool for exploration and optimization of systems represented by machine learning models. SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability con
Externí odkaz:
http://arxiv.org/abs/2405.10215
Symbolic Machine Learning Prover (SMLP) is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a
Externí odkaz:
http://arxiv.org/abs/2402.01415
Autor:
Menezes, Rafael, Aldughaim, Mohannad, Farias, Bruno, Li, Xianzhiyu, Manino, Edoardo, Shmarov, Fedor, Song, Kunjian, Brauße, Franz, Gadelha, Mikhail R., Tihanyi, Norbert, Korovin, Konstantin, Cordeiro, Lucas C.
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis
Externí odkaz:
http://arxiv.org/abs/2312.14746
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it enc
Externí odkaz:
http://arxiv.org/abs/2308.05649
Application domains of Bayesian optimization include optimizing black-box functions or very complex functions. The functions we are interested in describe complex real-world systems applied in industrial settings. Even though they do have explicit re
Externí odkaz:
http://arxiv.org/abs/2106.06067
ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the ksmt calculus and show that it is a $\delta$-complete decision proce
Externí odkaz:
http://arxiv.org/abs/2104.13269
Publikováno v:
In Theoretical Computer Science 9 October 2023 975
In this paper we propose a novel approach for checking satisfiability of non-linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL style calculus, using a composition of symbolical and numerical methods
Externí odkaz:
http://arxiv.org/abs/1905.09227
Autor:
Brauße, Franz, Steinberg, Florian
Kawamura and Cook specified the least set of information about a continuous function on the unit interval which is needed for fast function evaluation. This paper presents a variation of their result. To make the above statement precise, one has to s
Externí odkaz:
http://arxiv.org/abs/1703.10044