6 papers
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang +2
Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. Howev…
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous +2
Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by…
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…