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