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 1 to 20 of 113.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  2. Chawdhary, Aziem; Robbins, Ed; King, Andy: Incrementally closing octagons (2019)
  3. Crawford-Kahrl, Peter; Cummins, Bree; Gedeon, Tomas: Comparison of combinatorial signatures of global network dynamics generated by two classes of ODE models (2019)
  4. Darais, David; Van Horn, David: Constructive Galois connections (2019)
  5. Gronski, Jessica; Ben Sassi, Mohamed-Amin; Becker, Stephen; Sankaranarayanan, Sriram: Template polyhedra and bilinear optimization (2019)
  6. Apinis, Kalmer; Vene, Varmo; Vojdani, Vesal: Demand-driven interprocedural analysis for map-based abstract domains (2018)
  7. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  8. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  9. Diallo, Nafi; Ghardallou, Wided; Desharnais, Jules; Mili, Ali: Convergence: integrating termination and abort-freedom (2018)
  10. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  11. Heo, Kihong; Oh, Hakjoo; Yang, Hongseok: Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses (2018)
  12. Journault, Matthieu; Miné, Antoine: Inferring functional properties of matrix manipulating programs by abstract interpretation (2018)
  13. Payet, Étienne; Spoto, Fausto: Checking array bounds by abstract interpretation and symbolic expressions (2018)
  14. Titolo, Laura; Feliú, Marco A.; Moscato, Mariano; Muñoz, César A.: An abstract interpretation framework for the round-off error analysis of floating-point programs (2018)
  15. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  16. Blazy, Sandrine; Bühler, David; Yakobowski, Boris: Structuring abstract interpreters through state and value abstractions (2017)
  17. Miné, Antoine: Static analysis of embedded real-time concurrent software with dynamic priorities (2017)
  18. Monat, Raphaël; Miné, Antoine: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions (2017)
  19. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  20. Blazy, Sandrine; Laporte, Vincent; Pichardie, David: An abstract memory functor for verified C static analyzers (2016)

1 2 3 4 5 6 next