Automatic Verification of LLVM Code

2020/06/04 by Axel Legay, Dirk Nowotka, Legay, Axel +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL) #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #cs.PL #cs.SE

paper · pdf · doi:10.48550/arxiv.2006.02670

arxiv created 2020/06/04 · openalex publication_date 2020/06/04 · arxiv updated 2020/06/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

In this work we present our work in developing a software verification tool for llvm-code - Lodin - that incorporates both explicit-state model checking, statistical model checking and symbolic state model checking algorithms.

Citations

• Counterexample-guided abstraction refinement for symbolic model checking
• THE USE OF CONFIDENCE OR FIDUCIAL LIMITS ILLUSTRATED IN THE CASE OF THE BINOMIAL

Related

• Can LLMs Enable Verification in Mainstream Programming?
• Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
• InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?
• Lemur: Integrating Large Language Models in Automated Program Verification
• Model Checking