2012/05/16 by Pierre-Loïc Garoche, Garoche, Pierre-Loïc, Temesghen Kahsai +3 · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Modeling and Simulation Systems #Real-time simulation and control systems #Security and Verification in Computing #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1205.3758
openalex publication_date 2012/05/16 · openalex created_date 2022/08/28 · openalex updated_date 2026/07/28
The use of formal analysis tools on models or source code often requires the\navailability of auxiliary invariants about the studied system. Abstract\ninterpretation is currently one of the best approaches to discover useful\ninvariants, especially numerical ones. However, its application is limited by\ntwo orthogonal issues: (i) developing an abstract interpretation is often\nnon-trivial; each transfer function of the system has to be represented at the\nabstract level, depending on the abstract domain used; (ii) with precise but\ncostly abstract domains, the information computed by the abstract interpreter\ncan be used only once a post fix point has been reached; something that may\ntake a long time for very large system analysis or with delayed widening to\nimprove precision.\n This paper proposes a new, completely automatic, method to build abstract\ninterpreters. One of its nice features is that its produced interpreters can\nprovide sound invariants of the analyzed system before reaching the end of the\npost fix point computation, and so act as on-the-fly invariant generators.\n