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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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

Showing results 61 to 80 of 113.
Sorted by year (citations)
  1. Siegel, Stephen F.; Zirkel, Timothy K.: FEVS: a functional equivalence verification suite for high-performance scientific computing (2011)
  2. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Abstract fixpoint computations with numerical acceleration methods (2010)
  3. Brillout, Angelo; He, Nannan; Mazzucchi, Michele; Kroening, Daniel; Purandare, Mitra; Rümmer, Philipp; Weissenbacher, Georg: Mutation-based test case generation for Simulink models (2010)
  4. Buss, Marcio; Brand, Daniel; Sreedhar, Vugranam; Edwards, Stephen A.: A novel analysis space for pointer analysis and its application for bug finding (2010)
  5. Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent: A scalable segmented decision tree abstract domain (2010)
  6. Fulara, Jędrzej; Durnoga, Konrad; Jakubczyk, Krzysztof; Schubert, Aleksy: Relational abstract domain of weighted hexagons (2010)
  7. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  8. Logozzo, Francesco; Fähndrich, Manuel: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses (2010)
  9. Lopez-Garcia, Pedro; Darmawan, Luthfi; Bueno, Francisco: A framework for verification and debugging of resource usage properties: resource usage verification (2010)
  10. Monniaux, David: A minimalistic look at widening operators (2010)
  11. Monniaux, David: Automatic modular abstractions for template numerical constraints (2010)
  12. Peleska, Jan: Integrated and automated abstract interpretation, verification and testing of C/C++ modules (2010)
  13. Seidl, Helmut: Praktische Programmverifikation durch statische Analyse (2010) ioport
  14. Simon, Axel; King, Andy: The two variable per inequality abstract domain (2010)
  15. Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea: Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness (2009)
  16. Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea: Applications of polyhedral computations to the analysis and verification of hardware and software systems (2009)
  17. Bertot, Yves: Structural abstract interpretation: a formal study using Coq (2009)
  18. Bouissou, Olivier: Proving the correctness of the implementation of a control-command algorithm (2009)
  19. Bubel, Richard; Hähnle, Reiner; Weiß, Benjamin: Abstract interpretation of symbolic execution with explicit state updates (2009)
  20. Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier: Why does Astrée scale up? (2009)