The ASTREÉ Analyzer

By P. Cousot, R. Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival. 2005

483 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Hardware and Architecture, Software, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

1. Hongseok Yang
2. Cristiano Calcagno
3. Sriram K. Rajamani
4. Thomas Ball
5. Peter W. O'Hearn
6. Byron Cook
7. Dino Distefano
8. Vladimir Levin

In Hardware and Architecture

1. Swarat Chaudhuri
2. Sriram K. Rajamani
3. Thomas Ball
4. Charles Sutton
5. Miltiadis Allamanis
6. Bohus Ondrusek
7. Peter W. O'Hearn
8. Byron Cook

In Software

1. Charles Sutton
2. Miltiadis Allamanis
3. Earl T. Barr
4. Premkumar T. Devanbu
5. Rishabh Singh
6. Swarat Chaudhuri
7. Sriram K. Rajamani
8. Thomas Ball

In Program Analysis & Verification

1. Miltiadis Allamanis
2. Charles Sutton
3. Earl T. Barr
4. Cristiano Calcagno
5. Premkumar T. Devanbu
6. Peter W. O'Hearn
7. Hongseok Yang
8. Swarat Chaudhuri

Citations in the corpus

• A Survey of Machine Learning for Big Code and Naturalness (2017, methodology): “y elegant and powerful abstractions, definitions, algorithms, and proof techniques have been developed, which have led to important practical tools for program verification, bug finding, and refactoring [24, 42, 45]. It should be emphasized that these are theory-first approaches. Software constructions ”
• Continuity analysis of programs (2010, background): “Also, for purely numerical programs, robustness can be analyzed by abstract interpretation using existing domains [4, 5].”
• Secure two-party computations in ANSI C (2012, methodology): “The last decade has seen dramatic improvements in practical source code analysis tools for C such as Microsoft’s SLAM [2], the abstract interpreter ASTREE [14] and the bit-precise model checker CBMC [10].”
• Thorough static analysis of device drivers (2006, background): “In specific domains such as numerically intensive programs, the abstract interpreter can be tuned to reduce false errors to manageable limits [24].”
• The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems (2006, background): “n operators defined in [58] and [60]; We also plan to add support for more complexity-throttling techniques such as: breaking down the set of the variables of interests into “packs” of manageable size [22,35,84]; support for Cartesian factoring as defined in [55]; and the limitation of the number of c”
• Compositional shape analysis by means of bi-abduction (2009, methodology): “2006] and ASTRÉE’s proof of the absence of run-time errors in Airbus code [Cousot et al. 2005].”
• Frama-C: A software analysis perspective (2015, background): “While much remains to be done from an academic standpoint, some of the major advances in these fields are already being successfully implemented [18,41,21,47,52] – and met with growing industrial interest.”
• Proving programs robust (2011, background): “In addition, there are many efforts in the abstract interpretation literature that, while not verifying robustness explicitly, reason about the uncertainty in a program’s behavior due to floating-point rounding and sensor errors [11, 18, 8, 6, 7].”
• Moving Fast with Software Verification (2015, background): “– Astrée has famously proven the absence of runtime errors in Airbus code [8].”
• A Software Analysis Perspective (2012, background): “While much remains to be done from an academic standpoint, some of the major advances in these fields are already being successfully implemented [18,41,25,46,51] – and met with growing industrial interest.”