The ASTREÉ Analyzer. ASTRÉE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical real-time software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.

References in zbMATH (referenced in 71 articles , 3 standard articles )

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

1 2 3 4 next

  1. Ferrara, Pietro: A generic framework for heap and value analyses of object-oriented programming languages (2016)
  2. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  3. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015)
  4. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  5. Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)
  6. Cousot, Patrick; Cousot, Radhia: A Galois connection calculus for abstract interpretation (2014)
  7. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  8. Wu, Xueguang; Chen, Liqian; Wang, Ji: An abstract domain to infer symbolic ranges over nonnegative parameters (2014)
  9. Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
  10. Sharma, Rahul; Gupta, Saurabh; Hariharan, Bharath; Aiken, Alex; Liang, Percy; Nori, Aditya V.: A data driven approach for algebraic loop invariants (2013)
  11. Amato, Gianluca; Parton, Maurizio; Scozzari, Francesca: Discovering invariants via simple component analysis (2012)
  12. Beckschulze, Eva; Kowalewski, Stefan; Brauer, Jörg: Access-based localization for octagons (2012)
  13. Bouaziz, Mehdi: \ssfTreeKs: a functor to make numerical abstract domains scalable (2012)
  14. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Acceleration of the abstract fixpoint computation in numerical program analysis (2012)
  15. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  16. Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
  17. Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent: Theories, solvers and static analysis by abstract interpretation (2012)
  18. Fulara, Jędrzej: Generic abstraction of dictionaries and arrays (2012)
  19. Gawlitza, Thomas Martin; Monniaux, David: Invariant generation through strategy iteration in succinctly represented control flow graphs (2012)
  20. Goubault, Eric; Le Gall, Tristan; Putot, Sylvie: An accurate join for zonotopes, preserving affine input/output relations (2012)

1 2 3 4 next