2005/08/24 by Tristan Denmat, Denmat, Tristan, Arnaud Gotlieb +4
Computer Science · #D.2.6 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.cs/0508108
In A. Serebrenik and S. Munoz-Hernandez (editors), Proceedings of the 15th Workshop on Logic-based methods in Programming Environments October 2005, Sitges. cs.PL/0508078
arxiv created 2005/08/24 · openalex publication_date 2005/08/24 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
A program invariant is a property that holds for every execution of the program. Recent work suggest to infer likely-only invariants, via dynamic analysis. A likely invariant is a property that holds for some executions but is not guaranteed to hold for all executions. In this paper, we present work in progress addressing the challenging problem of automatically verifying that likely invariants are actual invariants. We propose a constraint-based reasoning approach that is able, unlike other approaches, to both prove or disprove likely invariants. In the latter case, our approach provides counter-examples. We illustrate the approach on a motivating example where automatically generated likely invariants are verified.