Verasco

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.


References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Casso, Ignacio; Morales, José F.; López-García, P.; Hermenegildo, Manuel V.: Testing your (static analysis) truths (2021)
  2. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  3. Boulmé, Sylvain; Maréchal, Alexandre: Refinement to certify abstract interpretations: illustrated on linearization for polyhedra (2019)
  4. Darais, David; Van Horn, David: Constructive Galois connections (2019)
  5. D’Silva, Vijay; Urban, Caterina: Abstract interpretation as automated deduction (2017)
  6. Jourdan, Jacques-Henri: Sparsity preserving algorithms for octagons (2017)
  7. Maréchal, Alexandre; Périn, Michaël: Efficient elimination of redundancies in polyhedra by raytracing (2017)
  8. Sharma, Tushar; Reps, Thomas: Sound bit-precise numerical domains (2017)
  9. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  10. Blazy, Sandrine; Laporte, Vincent; Pichardie, David: An abstract memory functor for verified C static analyzers (2016)
  11. Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
  12. Jourdan, Jacques-Henri; Laporte, Vincent; Blazy, Sandrine; Leroy, Xavier; Pichardie, David: A formally-verified C static analyzer (2015) ioport