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.

References in zbMATH (referenced in 113 articles , 3 standard articles )

Showing results 41 to 60 of 113.
Sorted by year (citations)
  1. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  2. Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
  3. Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent: Theories, solvers and static analysis by abstract interpretation (2012)
  4. Fulara, Jędrzej: Generic abstraction of dictionaries and arrays (2012)
  5. Gawlitza, Thomas Martin; Monniaux, David: Invariant generation through strategy iteration in succinctly represented control flow graphs (2012)
  6. Goubault, Eric; Le Gall, Tristan; Putot, Sylvie: An accurate join for zonotopes, preserving affine input/output relations (2012)
  7. Lee, Oukseh; Yang, Hongseok; Petersen, Rasmus: A divide-and-conquer approach for analysing overlaid data structures (2012)
  8. Lee, Woosuk; Lee, Wonchan; Yi, Kwangkeun: Sound non-statistical clustering of static analysis alarms (2012)
  9. Miné, Antoine: Static analysis of run-time errors in embedded real-time parallel C programs (2012)
  10. Monniaux, David; Le Guen, Julien: Stratified static analysis based on variable dependencies (2012)
  11. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  12. Colón, Michael A.; Sankaranarayanan, Sriram: Generalizing the template polyhedral domain (2011)
  13. Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco: Precondition inference from intermittent assertions and application to contracts on collections (2011)
  14. Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco: A parametric segmentation functor for fully automatic and scalable array content analysis (2011)
  15. Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent: The reduced product of abstract domains and the combination of decision procedures (2011)
  16. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  17. Gawlitza, Thomas Martin; Monniaux, David: Improving strategies via SMT solving (2011)
  18. Hubert, Laurent; Barré, Nicolas; Besson, Frédéric; Demange, Delphine; Jensen, Thomas; Monfort, Vincent; Pichardie, David; Turpin, Tiphaine: Sawja: static analysis workshop for Java (2011)
  19. Miné, Antoine: Static analysis of run-time errors in embedded critical parallel C programs (2011)
  20. Nguyen, Thi Minh Tuyen; Marché, Claude: Hardware-dependent proofs of numerical programs (2011)