- 🔭 I’m currently working on: https://github.com/adilanwar2399/ESBMC-ibmc.git
- 🌱 I’m currently learning:
- ⇒ Prompt Engineering Techniques
- ⇒ Invariant Synthesis Techniques
- ⇒ Bounded Model Checking Theory
- ⇒ Software Verification Theory
- ⇒ SMT Solvers Theory
- 💬 Ask me about: Bounded Model Checking, Invariant Generation, Prompt Engineering Techniques, LLMs and Software Verification.
- 📫 How to reach me:
- ⇒ Email: [email protected]
Hi, my name is Adil and welcome to my github page. Here you will find my contributions.
I am a Postgraduate Doctoral Researcher at the University of Manchester. I am a software engineer with a specialisation in computer security. I am proficient in many programming languages like: python, java, c and c++. My research areas involve: Software Security and Verification, Formal Methods (Automated Reasoning) and Artificial Intelligence (LLMs).
@inproceedings{10.1145/3691620.3695512,
author = {Pirzada, Muhammad A. A. and Reger, Giles and Bhayat, Ahmed and Cordeiro, Lucas C.},
title = {LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling},
year = {2024},
isbn = {9798400712487},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3691620.3695512},
doi = {10.1145/3691620.3695512},
abstract = {We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node asserting invariants of the loop. We generate these invariants using Large Language Models (LLMs) and use a first-order theorem prover to ensure the correctness of the generated statements. We thus transform programs to loop-free variants in a sound manner. Our experimental results show that the resulting tool, ESBMC ibmc, is competitive with state-of-the-art formal verifiers for programs with unbounded loops, significantly improving the number of programs verified by the industrial-strength software verifier ESBMC and verifying programs that state-of-the-art software verifiers such as SeaHorn and VeriAbs could not.},
booktitle = {Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering},
pages = {1395–1407},
numpages = {13},
keywords = {program verification, large language models, bounded model checking, invariant generation},
location = {Sacramento, CA, USA},
series = {ASE '24}
}