Verasco swMATH ID: 19985 Software Authors: Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie Description: Verasco is a static analyzer for the CompCert subset of ISO C 1999 that establishes the absence of run-time errors in analyzed programs. The analyzer is based on abstract interpretation and combines several abstract domains, non-relational (integer intervals, floating-point intervals, integer congruences, points-to properties) and relational (integer linear inequalities, symbolic equalities). Verasco enjoys a modular structure roughly inspired by that of Astrée. The major novelty of Verasco, compared with other static analysis tools, is that it is entirely specified and proved sound using the Coq proof assistant. Verasco’s proof guarantees, with mathematical certainty, that programs that analyze without alarms are free of run-time errors. Homepage: http://compcert.inria.fr/verasco/ Related Software: Coq; z3; ASTREE; Toolchain; LLVM; HACL*; Ciao; CiaoPP; QuickCheck; Haskell; Fiat; Galculator; NaCl; CompCert; CVC4; VCC; AProVE; Infer; KITTeL; Ctrl Cited in: 12 Publications all top 5 Cited by 33 Authors 2 Blazy, Sandrine 2 Maréchal, Alexandre 2 Pichardie, David 1 Aschermann, Cornelius 1 Besson, Frédéric 1 Boulmé, Sylvain 1 Brockschmidt, Marc 1 Casso, Ignacio 1 Darais, David 1 D’silva, Vijay 1 Franceschino, Lucas 1 Frohn, Florian 1 Fuhs, Carsten 1 Gandhi, Rajeev 1 Giesl, Jürgen 1 Hensel, Jera 1 Hermenegildo, Manuel V. 1 Jourdan, Jacques-Henri 1 Laporte, Vincent 1 López-García, Pedro 1 Morales, Jose Francisco 1 Narasimhan, Priya 1 Périn, Michael 1 Reps, Thomas W. 1 Schneider-Kamp, Peter 1 Sharma, Tushar 1 Ströder, Thomas 1 Talpin, Jean-Pierre 1 Tan, Jiaqi 1 Tay, Hui Jun 1 Urban, Caterina 1 VanHorn, David A. 1 Wilke, Pierre Cited in 2 Serials 4 Journal of Automated Reasoning 1 Journal of Functional Programming all top 5 Cited in 6 Fields 11 Computer science (68-XX) 2 Convex and discrete geometry (52-XX) 1 Mathematical logic and foundations (03-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year