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

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

1 2 3 4 5 6 next

  1. Apinis, Kalmer; Vene, Varmo; Vojdani, Vesal: Demand-driven interprocedural analysis for map-based abstract domains (2018)
  2. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  3. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  4. Diallo, Nafi; Ghardallou, Wided; Desharnais, Jules; Mili, Ali: Convergence: integrating termination and abort-freedom (2018)
  5. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  6. Heo, Kihong; Oh, Hakjoo; Yang, Hongseok: Learning analysis strategies for octagon and context sensitivity from labeled data generated by static analyses (2018)
  7. Journault, Matthieu; Miné, Antoine: Inferring functional properties of matrix manipulating programs by abstract interpretation (2018)
  8. Payet, Étienne; Spoto, Fausto: Checking array bounds by abstract interpretation and symbolic expressions (2018)
  9. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  10. Blazy, Sandrine; Bühler, David; Yakobowski, Boris: Structuring abstract interpreters through state and value abstractions (2017)
  11. Monat, Raphaël; Miné, Antoine: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions (2017)
  12. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  13. Blazy, Sandrine; Laporte, Vincent; Pichardie, David: An abstract memory functor for verified C static analyzers (2016)
  14. Cha, Sooyoung; Jeong, Sehun; Oh, Hakjoo: Learning a strategy for choosing widening thresholds from a large codebase (2016)
  15. Ferrara, Pietro: A generic framework for heap and value analyses of object-oriented programming languages (2016)
  16. Mastroeni, Isabella; Giacobazzi, Roberto: Weakening additivity in adjoining closures (2016)
  17. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  18. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  19. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  20. Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)

1 2 3 4 5 6 next