ASTREE

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 113 articles , 3 standard articles )

Showing results 81 to 100 of 113.
Sorted by year (citations)
  1. Grund, Daniel; Reineke, Jan: Abstract interpretation of FIFO replacement (2009)
  2. Kuliamin, V. V.: Integration of verification methods for program systems (2009)
  3. Logozzo, Francesco: Class invariants as abstract interpretation of trace semantics (2009)
  4. Monniaux, David P.: Automatic modular abstractions for linear constraints (2009)
  5. Allamigeon, Xavier; Hymans, Charles: Static analysis by abstract interpretation: Application to the detection of heap overflows. (2008) ioport
  6. Bouissou, Olivier; Martel, Matthieu: A hybrid denotational semantics for hybrid systems (2008)
  7. Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Monniaux, David; Rival, Xavier: Combination of abstractions in the ASTRÉE static analyzer (2008) ioport
  8. Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)
  9. Pichardie, David: Building certified static analysers by modular construction of well-founded lattices (2008)
  10. Simon, Axel: Splitting the control flow with Boolean flags (2008)
  11. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007) ioport
  12. Blanchet, Bruno; Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Monniaux, David; Rival, Xavier: A static analyzer for large safety-critical software (2007) ioport
  13. Simon, Axel; King, Andy: Taming the wrapping of integer arithmetic (2007)
  14. Allamigeon, Xavier; Godard, Wenceslas; Hymans, Charles: Static analysis of string manipulations in critical embedded C programs (2006)
  15. Besson, Frédéric; Jensen, Thomas; Pichardie, David: Proof-carrying code from certified abstract interpretation and fixpoint compression (2006)
  16. Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok: Beyond reachability: shape abstraction in the presence of pointer arithmetic (2006)
  17. Dams, Dennis R.; Namjoshi, Kedar S.: Orion: high-precision methods for static error analysis of C and C++ programs (2006)
  18. Gallagher, John P.; Puebla, Germán; Albert, Elvira: Converting one type-based abstract domain to another (2006)
  19. Halbwachs, N.; Merchat, D.; Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations (2006)
  20. Kroening, Daniel; Sharygina, Natasha: Approximating predicate images for bit-vector logic (2006)