6 papers
Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
Yiannis Charalambous, Rafael Menezes, Youcheng Sun +1
Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses th…
GPT, But Backwards: Exactly Inverting Language Model Outputs
Adrians Skapars, Edoardo Manino, Youcheng Sun +1
The task of reconstructing unknown textual inputs to language models is a fundamental auditing primitive that allows us to assess the model's vulnerability to a range of security i…
Floating-Point Neural Network Verification at the Software Level
Edoardo Manino, Bruno Farias, Rafael Sá Menezes +3
The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques canno…
Generative transformations and patterns in LLM-native approaches for software verification and falsification
VÃctor A. Braberman, Flavia Bonomo-Braberman, Yiannis Charalambous +3
The emergence of prompting as the dominant paradigm for leveraging Large Language Models (LLMs) has led to a proliferation of LLM-native software, where application behavior arises…
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…
Neural Network Verification is a Programming Language Challenge
Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin +8
Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while pr…