4 citations · 8 across the 12 of their papers we have counts for
12 papers
BLOOM-WILT: Logit Tilting for Behaviour Elicitation in Automated LLM Auditing
Adrians Skapars, Edoardo Manino
Users of a deployed language model routinely encounter behaviours that have never been observed during testing, since deployment puts the model through orders of magnitude more int…
Encrypted Neural Networks without Overflows
Philipp Kern, Lorenzo Rovida, Samuel Teuber +3
The popular Cheon-Kim-Kim-Song (CKKS) scheme enables efficient private inference in neural networks by evaluating them on encrypted data. Since CKKS only supports addition, multipl…
The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results
Konstantin Kaulen, Tobias Ladner, Stanley Bak +8
This report summarizes the 6th International Verification of Neural Networks Competition (VNN-COMP 2025), held as a part of the 8th International Symposium on AI Verification (SAIV…
Floating-Point Neural Network Verification at the Software Level
Edoardo Manino, Bruno Farias, Rafael Sá Menezes +2
The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques canno…
GPT, But Backwards: Exactly Inverting Language Model Outputs
Adrians Skapars, Edoardo Manino, Youcheng Sun +1
Recent work shows that distinct inputs produce distinct hidden representations in LLMs, so the input can in principle be recovered from them. Yet, no existing method can reliably d…
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…
Was it Slander? Towards Exact Inversion of Generative Language Models
Adrians Skapars, Edoardo Manino, Youcheng Sun +1
Training large language models (LLMs) requires a substantial investment of time and money. To get a good return on investment, the developers spend considerable effort ensuring tha…
Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov +3
Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack…
Verifying components of Arm(R) Confidential Computing Architecture with ESBMC
Tong Wu, Shale Xiong, Edoardo Manino +2
Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to ve…
Automated Repair of AI Code with Large Language Models and Formal Verification
Yiannis Charalambous, Edoardo Manino, Lucas C. Cordeiro
The next generation of AI systems requires strong safety guarantees. This report looks at the software implementation of neural networks and related memory safety properties, inclu…
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…
NeuroCodeBench: a plain C neural network benchmark for software verification
Edoardo Manino, Rafael Sá Menezes, Fedor Shmarov +1
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal,…