1089:
1079:
1069:
1059:
939:
475:
A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, C. Ferdinand. Taking Static
Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse,
490:
D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. Analyze This! Sound Static
Analysis for Integration Verification of Large-Scale Automotive Software. SAE Technical Paper 2019-01-1246, SAE World Congress 2019, Detroit, April 2019.
442:
Arnaud J. Venet and
Michael R. Lowry. 2010. Static analysis for software assurance: soundness, scalability and adaptiveness. In Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER '10). ACM, New York, NY, USA, 393-396.
425:, In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196–207, ACM.
45:
479:
D. Kästner, L. Mauborgne, N. Grafe, C. Ferdinand. Advanced Sound Static
Analysis to Detect Safety- and Security-Relevant Programming Defects. 8th International Journal on Advances in Security,
439:, Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22–24 August 2007, LNCS 4634, pp. 437–451
569:
534:
1083:
596:
1073:
1119:
391:
40:
468:
Daniel Kästner, Stephan
Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival.
462:
411:, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Volume 2566 of Lecture Notes in Computer Science, pp. 85–108, Springer.
378:
GmbH. It is used in the defense–aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is
623:
328:
421:
Bruno
Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival,
1114:
403:
Bruno
Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
290:
254:
901:
754:
662:
367:
674:
696:
405:
Design and
Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software
278:
75:
1030:
889:
740:
651:
589:
856:
770:
719:
656:
605:
286:
1058:
1020:
246:
1093:
582:
304:
The tool is tailored toward safety-critical embedded code: specific analysis techniques are used for common
239:
895:
947:
875:
1052:
348:
309:
294:
243:
185:
628:
409:
The
Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones
168:
961:
760:
324:
131:
484:
323:
Concurrent code is analyzed with a sound interleaving semantics that is aware of the concurrent
1015:
480:
458:
270:
781:
492:
444:
426:
412:
352:
344:
258:
180:
111:
1010:
861:
262:
235:
173:
1025:
973:
967:
869:
363:
317:
313:
305:
282:
1108:
703:
991:
985:
979:
847:
731:
266:
708:
687:
116:
34:
24:
881:
823:
448:
416:
332:
274:
1063:
430:
997:
788:
614:
570:
Safety-critical C code checked by static analysis tool. EDN Europe, 2013.
496:
472:. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010.
356:
152:
148:
144:
938:
927:
841:
811:
765:
340:
140:
29:
Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival
907:
835:
799:
668:
379:
375:
136:
250:
913:
829:
713:
645:
298:
124:
120:
104:
574:
817:
805:
637:
564:
371:
336:
46:
French
Institute for Research in Computer Science and Automation
578:
253:, and emits an exhaustive list of possible runtime errors and
535:"L'Avion qui "bat des ailes" a fédéré de nombreux chercheurs"
516:
557:
196:
455:
Static Analysis of Software: The Abstract Interpretation
423:
A Static Analyzer for Large Safety-Critical Software.
351:, the placement of threads to cores, and the use of
955:
946:
855:
780:
729:
686:
636:
622:
613:
191:
179:
167:
159:
130:
110:
100:
74:
52:
33:
23:
487:, vol. 11, no. 1 & 2, 149-159, IARIA, 2018.
257:violations. The defect classes covered include
590:
470:Astrée: Proving the Absence of Runtime Errors
343:execution models and can be adapted to added
8:
18:
952:
633:
619:
597:
583:
575:
17:
508:
392:List of tools for static code analysis
242:. It analyzes programs written in the
7:
374:, and is available commercial from
437:Astrée: from Research to Industry.
14:
1088:
1087:
1078:
1077:
1068:
1067:
1057:
937:
331:mechanisms. Astrée supports the
281:, etc. Astrée includes a static
41:École normale supérieure (Paris)
435:David Delmas and Jean Souyris.
902:Logic for Computable Functions
1:
1120:Static program analysis tools
287:cybersecurity vulnerabilities
565:Astrée industrial/sales page
39:Laboratoire d'Informatique,
48:(INRIA, Paris–Rocquencourt)
1136:
1039:
935:
720:Standard ML of New Jersey
96:
83:; 1 year ago
70:
1021:Christine Paulin-Mohring
368:École Normale Supérieure
362:Astrée was developed in
347:(OS) specifications. On
316:, rate limiters...) and
297:written in the language
1115:Abstract interpretation
1094:Category:Software:OCaml
449:10.1145/1882362.1882442
417:10.1007/3-540-36377-7_5
327:, their priorities and
240:abstract interpretation
453:Jean-Louis Boulanger.
407:, invited chapter. In
58:; 21 years ago
1084:Category:Family:OCaml
431:10.1145/781131.781153
370:, a joint group with
349:multi-core processors
310:finite-state machines
244:programming languages
222:tatique de logiciels
56:16 December 2002
1053:Open-source software
497:10.4271/2019-01-1246
325:threads of execution
295:proprietary software
20:
1074:Category:Family:ML
962:Lennart Augustsson
285:and helps finding
265:, dereferences of
25:Original author(s)
1102:
1101:
1016:Steven G. Johnson
1006:
1005:
923:
922:
782:Programming tools
750:
749:
463:978-1-84821-320-3
271:dangling pointers
259:divisions by zero
209:
208:
1127:
1091:
1090:
1081:
1080:
1071:
1070:
1061:
953:
941:
862:proof assistants
634:
620:
599:
592:
585:
576:
561:
560:
558:Official website
543:
542:
541:. 26 April 2005.
531:
525:
524:
513:
345:operating system
263:buffer overflows
234:mbarqués") is a
205:
202:
200:
198:
112:Operating system
91:
89:
84:
66:
64:
59:
21:
1135:
1134:
1130:
1129:
1128:
1126:
1125:
1124:
1105:
1104:
1103:
1098:
1056:
1035:
1011:Thierry Coquand
1002:
942:
933:
919:
860:
857:Theorem provers
851:
776:
746:
725:
682:
627:
624:Implementations
609:
603:
556:
555:
552:
547:
546:
533:
532:
528:
515:
514:
510:
505:
400:
388:
329:synchronization
314:digital filters
236:static analyzer
195:
174:static analyzer
92:
87:
85:
82:
81:23.10 / 2023
62:
60:
57:
53:Initial release
44:
12:
11:
5:
1133:
1131:
1123:
1122:
1117:
1107:
1106:
1100:
1099:
1097:
1048:
1046:= discontinued
1040:
1037:
1036:
1034:
1033:
1031:Simon Thompson
1028:
1026:Frank Pfenning
1023:
1018:
1013:
1007:
1004:
1003:
1001:
995:
989:
983:
977:
971:
968:Damien Doligez
965:
959:
957:
950:
944:
943:
936:
934:
932:
931:
924:
921:
920:
918:
917:
911:
905:
898:
893:
887:
886:
885:
873:
866:
864:
853:
852:
850:
845:
839:
833:
827:
821:
815:
809:
803:
797:
792:
786:
784:
778:
777:
775:
774:
768:
763:
758:
751:
748:
747:
745:
744:
737:
735:
727:
726:
724:
723:
717:
711:
706:
701:
692:
690:
684:
683:
681:
680:
679:
678:
672:
666:
660:
654:
642:
640:
631:
617:
611:
610:
604:
602:
601:
594:
587:
579:
573:
572:
567:
562:
551:
550:External links
548:
545:
544:
526:
507:
506:
504:
501:
500:
499:
488:
477:
473:
466:
451:
440:
433:
419:
399:
396:
395:
394:
387:
384:
364:Patrick Cousot
359:are analyzed.
318:floating-point
306:control theory
207:
206:
193:
189:
188:
183:
177:
176:
171:
165:
164:
161:
157:
156:
134:
128:
127:
114:
108:
107:
102:
98:
97:
94:
93:
80:
78:
76:Stable release
72:
71:
68:
67:
54:
50:
49:
37:
31:
30:
27:
13:
10:
9:
6:
4:
3:
2:
1132:
1121:
1118:
1116:
1113:
1112:
1110:
1096:
1095:
1086:
1085:
1076:
1075:
1066:
1065:
1060:
1055:
1054:
1049:
1047:
1044:
1041:
1038:
1032:
1029:
1027:
1024:
1022:
1019:
1017:
1014:
1012:
1009:
1008:
999:
996:
994:(Extended ML)
993:
990:
987:
984:
982:(Caml, OCaml)
981:
978:
975:
972:
969:
966:
963:
960:
958:
954:
951:
949:
945:
940:
929:
926:
925:
915:
912:
909:
906:
904:
903:
899:
897:
894:
891:
888:
883:
880:
879:
877:
874:
871:
868:
867:
865:
863:
858:
854:
849:
846:
843:
840:
837:
834:
831:
828:
825:
822:
819:
816:
813:
810:
807:
804:
801:
798:
796:
793:
790:
787:
785:
783:
779:
772:
769:
767:
764:
762:
759:
756:
753:
752:
742:
739:
738:
736:
734:
733:
728:
721:
718:
715:
712:
710:
707:
705:
704:Concurrent ML
702:
699:
698:
694:
693:
691:
689:
685:
676:
673:
670:
667:
664:
661:
658:
655:
653:
650:
649:
647:
644:
643:
641:
639:
635:
632:
630:
625:
621:
618:
616:
612:
607:
600:
595:
593:
588:
586:
581:
580:
577:
571:
568:
566:
563:
559:
554:
553:
549:
540:
536:
530:
527:
522:
521:astree.ens.fr
518:
512:
509:
502:
498:
494:
489:
486:
482:
478:
474:
471:
467:
464:
460:
456:
452:
450:
446:
441:
438:
434:
432:
428:
424:
420:
418:
414:
410:
406:
402:
401:
397:
393:
390:
389:
385:
383:
381:
377:
373:
369:
365:
360:
358:
354:
350:
346:
342:
338:
334:
330:
326:
321:
319:
315:
311:
307:
302:
300:
296:
292:
288:
284:
283:taint checker
280:
276:
272:
268:
264:
260:
256:
252:
248:
245:
241:
237:
233:
229:
225:
221:
217:
213:
204:
194:
190:
187:
184:
182:
178:
175:
172:
170:
166:
162:
158:
154:
150:
146:
142:
138:
135:
133:
129:
126:
122:
118:
115:
113:
109:
106:
103:
99:
95:
79:
77:
73:
69:
55:
51:
47:
42:
38:
36:
32:
28:
26:
22:
16:
1092:
1082:
1072:
1062:
1050:
1045:
1042:
992:Don Sannella
986:Robin Milner
980:Xavier Leroy
900:
848:SLAM project
794:
732:Dependent ML
730:
695:
538:
529:
520:
511:
469:
454:
436:
422:
408:
404:
398:Bibliography
366:'s group at
361:
322:
308:constructs (
303:
231:
227:
223:
219:
215:
211:
210:
160:Available in
35:Developer(s)
15:
974:Gérard Huet
709:Extended ML
688:Standard ML
608:programming
539:Le Monde.fr
353:mutex locks
186:Proprietary
1109:Categories
722:° (SML/NJ)
503:References
289:, such as
275:data races
117:Windows 10
101:Written in
63:2002-12-16
964:(Lazy ML)
956:Designers
948:Community
882:HOL Light
824:Marionnet
485:1942-2636
357:spinlocks
333:ARINC 653
320:numbers.
279:deadlocks
255:assertion
238:based on
218:nalyseur
998:Don Syme
890:Isabelle
789:Alt-Ergo
629:dialects
615:Software
465:. Wiley.
386:See also
293:. It is
132:Platform
123:64-bit,
1043:Italics
970:(OCaml)
928:GeneWeb
842:Semgrep
812:Frama-C
766:MacroML
761:Lazy ML
755:Futhark
476:France.
341:AUTOSAR
291:Spectre
199:.astree
192:Website
181:License
163:English
141:AArch64
86: (
61: (
43:(LIENS)
976:(Caml)
908:Matita
836:Poplog
800:Camlp4
795:Astrée
675:Reason
669:JoCaml
517:"Home"
483:
461:
380:Airbus
376:AbsInt
339:, and
212:Astrée
137:x86-64
19:Astrée
914:Twelf
830:MTASC
714:MLton
697:Alice
646:OCaml
299:OCaml
226:emps-
125:macOS
121:Linux
105:OCaml
1064:Book
1051:° =
1000:(F#)
988:(ML)
896:LEGO
818:Haxe
806:FFTW
638:Caml
481:ISSN
459:ISBN
372:CNRS
355:and
337:OSEK
267:null
249:and
201:.ens
169:Type
88:2023
876:HOL
870:Coq
741:ATS
652:Eff
493:doi
445:doi
427:doi
413:doi
269:or
251:C++
230:el
203:.fr
197:www
1111::
878:°
771:Ur
663:F#
657:F*
648:°
606:ML
537:.
519:.
457:.
382:.
335:,
312:,
301:.
277:,
273:,
261:,
228:ré
214:("
153:M3
151:,
149:M2
147:,
145:M1
139:;
119:,
930:°
916:°
910:°
892:°
884:°
872:°
859:,
844:°
838:°
832:°
826:°
820:°
814:°
808:°
802:°
791:°
773:°
757:°
743:°
716:°
700:°
677:°
671:°
665:°
659:°
626:,
598:e
591:t
584:v
523:.
495::
447::
429::
415::
247:C
232:e
224:t
220:s
216:A
155:)
143:(
90:)
65:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.