Cover Image

ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Pirzada, Muhammad A. A., Wang, Weiqi, Charalambous, Yiannis, Korovin, Konstantin, Cordeiro, Lucas C.
Format:	Preprint
Published:	2026
Subjects:	Software Engineering Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Automated Repair of AI Code with Large Language Models and Formal Verification
by: Charalambous, Yiannis, et al.
Published: (2024)

Supporting Software Formal Verification with Large Language Models: An Experimental Study
by: Wang, Weiqi, et al.
Published: (2025)

UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification
by: Charalambous, Yiannis, et al.
Published: (2025)

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
by: Tihanyi, Norbert, et al.
Published: (2023)

ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
by: Dantas, Pierre, et al.
Published: (2026)

Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
by: Hähnle, Reiner, et al.
Published: (2025)

AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
by: Zhou, Xiaofeng, et al.
Published: (2026)

Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview
by: Tihanyi, Norbert, et al.
Published: (2025)

Floating-Point Neural Network Verification at the Software Level
by: Manino, Edoardo, et al.
Published: (2025)

Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
by: Richter, Cedric, et al.
Published: (2025)

ReqInOne: A Large Language Model-Based Agent for Software Requirements Specification Generation
by: Zhu, Taohong, et al.
Published: (2025)

Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
by: Corazza, Jan, et al.
Published: (2025)

Smart Contracts Formal Verification: A Systematic Literature Review
by: Davila, Rene, et al.
Published: (2025)

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
by: Liu, Yuwei, et al.
Published: (2026)

Automated Invariant Generation for Solidity Smart Contracts
by: Liu, Ye, et al.
Published: (2024)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
by: Wojtak, Connor, et al.
Published: (2025)

Using LLMs to Facilitate Formal Verification of RTL
by: Orenes-Vera, Marcelo, et al.
Published: (2023)

Using Assurance Cases to Guide Verification and Validation of Research Software
by: Smith, W. Spencer, et al.
Published: (2024)

Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
by: Faria, João Pascoal, et al.
Published: (2026)

SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
by: Ma, Lezhi, et al.
Published: (2026)

PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
by: Liu, Ye, et al.
Published: (2024)

Agentic Verification of Software Systems
by: Tu, Haoxin, et al.
Published: (2025)

Formal Verification of Consistency for Systems with Redundant Controllers
by: Johansson, Bjarne, et al.
Published: (2024)

Pros and Cons! Evaluating ChatGPT on Software Vulnerability
by: Yin, Xin
Published: (2024)

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
by: Basile, Davide
Published: (2025)

WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
by: Läufer, Konstantin, et al.
Published: (2024)

Software Engineering as a Domain to Formalize
by: Meyer, Bertrand
Published: (2025)

Ranking LLM-Generated Loop Invariants for Program Verification
by: Chakraborty, Saikat, et al.
Published: (2023)

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
by: Menezes, Rafael Sá, et al.
Published: (2024)

ProofWright: Towards Agentic Formal Verification of CUDA
by: Chatterjee, Bodhisatwa, et al.
Published: (2025)

Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
by: Sousa, Tiago, et al.
Published: (2024)

Selene: Pioneering Automated Proof in Software Verification
by: Zhang, Lichen, et al.
Published: (2024)

Combining Tests and Proofs for Better Software Verification
by: Huang, Li, et al.
Published: (2026)

Structural Abstraction and Selective Refinement for Formal Verification
by: Luckeneder, Christoph, et al.
Published: (2025)

Assurance Case Development for Evolving Software Product Lines: A Formal Approach
by: Murphy, Logan, et al.
Published: (2025)

DafnyBench: A Benchmark for Formal Software Verification
by: Loughridge, Chloe, et al.
Published: (2024)

Specification Vibing for Automated Program Repair
by: Zhu, Taohong, et al.
Published: (2026)

From Verification to Herding: Exploiting Software's Sparsity of Influence
by: Menzies, Tim, et al.
Published: (2026)

Scalable Deductive Verification of Data-Level Parallel Programs
by: Haak, Lars B. van den, et al.
Published: (2026)

Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?
by: Chaliasos, Stefanos, et al.
Published: (2023)