1 citations · 4 across the 13 of their papers we have counts for
7 papers · 1 filter
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…
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…
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…
FuSeBMC AI: Acceleration of Hybrid Approach through Machine Learning
Kaled M. Alshmrany, Mohannad Aldughaim, Chenfeng Wei +3
We present FuSeBMC-AI, a test generation tool grounded in machine learning techniques. FuSeBMC-AI extracts various features from the program and employs support vector machine and…
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…