4 citations · 4 across the 8 of their papers we have counts for
10 papers
ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST
Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha +4
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…
SMLP: Symbolic Machine Learning Prover (User Manual)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
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 m…
SMLP: Symbolic Machine Learning Prover
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
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 vec…
ESBMC v7.4: Harnessing the Power of Intervals
Rafael Menezes, Mohannad Aldughaim, Bruno Farias +9
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…
ESBMC v7.3: Model Checking C++ Programs using Clang AST
Kunjian Song, Mikhail R. Gadelha, Franz Brauße +2
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 C…
Bayesian Optimisation with Formal Guarantees
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
Application domains of Bayesian optimization include optimizing black-box functions or very complex functions. The functions we are interested in describe complex real-world system…
The ksmt calculus is a -complete decision procedure for non-linear constraints
Franz Brauße, Konstantin Korovin, Margarita V. Korovina +1
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 th…
A CDCL-style calculus for solving non-linear constraints
Franz Brauße, Konstantin Korovin, Margarita Korovina +1
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 s…
A minimal representation for continuous functions
Franz Brauße, Florian Steinberg
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 variat…
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Sewon Park, Franz Brauße, Pieter Collins +7
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides…