arXiv subjects

Franz Brauße

Publications and source records attributed to Franz Brauße.

10 recordsLinked to original sources

arXiv2025

ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

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 modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as 1) exception handling, 2) extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and 3) new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard.

cs.LO↗

arXiv2024

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation

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 a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.

math.NA↗

arXiv2024

SMLP: Symbolic Machine Learning Prover (User Manual)

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 constraints, based on SMT, constraint and NN solvers. In addition its exploration methods are guided by probabilistic and statistical methods. SMLP is a general purpose tool that requires only data suitable for ML modelling in the csv format (usually samples of the system's input/output). SMLP has been applied at Intel for analyzing and optimizing hardware designs at the analog level. Currently SMLP supports NNs, polynomial and tree models, and uses SMT solvers for reasoning and optimization at the backend, integration of specialized NN solvers is in progress.

cs.LG↗

arXiv2024

SMLP: Symbolic Machine Learning Prover

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 grey-box approach: SMLP combines statistical methods of data exploration with building and exploring machine learning models in close feedback loop with the system's response, and exploring these models by combining probabilistic and formal methods. SMLP has been applied in industrial setting at Intel for analyzing and optimizing hardware designs at the analog level. SMLP is a general purpose tool and can be applied to systems that can be sampled and modeled by machine learning models.

cs.LG↗

arXiv2023

ESBMC v7.4: Harnessing the Power of Intervals

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 of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.

cs.SE↗

arXiv2023

ESBMC v7.3: Model Checking C++ Programs using Clang AST

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 encountered challenges keeping up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of the old front-end became apparent, leading to difficult-to-maintain code. Consequently, modern C++ programs were challenging to verify. To overcome this obstacle, we redeveloped the front-end, opting for a more robust approach using clang. The new front-end efficiently traverses the Abstract Syntax Tree (AST) in-memory using clang APIs and transforms each AST node into ESBMC's Intermediate Representation. Through extensive experimentation, our results demonstrate that ESBMC v7.3 with the new front-end significantly reduces parse and conversion errors, enabling successful verification of a wide range of C++ programs, thereby outperforming previous ESBMC versions.

cs.LO↗

arXiv2021

Bayesian Optimisation with Formal Guarantees

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 representations, standard optimization techniques fail to provide validated solutions and correctness guarantees for them. In this paper we present a combination of Bayesian optimisation and SMT-based constraint solving to achieve safe and stable solutions with optimality guarantees.

cs.LG↗

arXiv2021

The ksmt calculus is a $δ$-complete decision procedure for non-linear constraints

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 $δ$-complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.

cs.LO↗

arXiv2019

A CDCL-style calculus for solving non-linear constraints

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. To deal with the non-linear components in case of conflicts we use numerically constructed restricted linearisations. This approach covers a large number of computable non-linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been evaluated on several non-linear SMT-LIB examples and the results have been compared with state-of-the-art SMT solvers.

cs.LO↗

arXiv2018

A minimal representation for continuous functions

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 specify what a "set of information" is and what "fast" should mean. Kawamura and Cook use polynomial-time computability in the sense of second-order complexity theory to define what "fast" means but do not use the most general "sets of information" this framework is able to handle. Instead they require codes to be length-monotone. This paper removes the additional premise of length-monotonicity, and instead imposes further conditions on the speed of the evaluation: The operation should now be computable in "hyper-linear" time. This means that the running time can not contain any iterations of the length function and, while an arbitrary polynomial may be applied to its value, on the argument side at most a shift by a constant is allowed. This is a very restrictive notion, but one can check that the Kawamura and Cook representation allows for hyper-linear time evaluation. The paper proves that it is not minimal with this property by providing the minimal set of information necessary for hyper-linear evaluation and proving that it is not polynomial-time equivalent to any encoding using only length-monotone names. Ultimatively, this is due to a failure of polynomial-time computability of an upper bound to a modulus of continuity. Indeed this failure seems to reflect the behavior of software based on the ideas of computable analysis appropriately and was one of the reasons for a closer investigation in the first place.

cs.LO↗