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

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

1 2 3 4 5 6 next

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

1 2 3 4 5 6 next