359:, where its founders had developed a generic and generative framework for binary-level static program analyzers and optimizers. An important component of this framework is the Program Analyzer Generator PAG, which allows to automatically generate static analyzers from a mathematical specification of the abstract domains and transfer functions. The first version of PAG was released in 1995. With PAG/WWW, a free academic version of PAG is available which has been used worldwide in numerous teaching courses.
22:
69:
399:("real-time embedded software static analyzer"). It has been used successfully on the flight control software of the AIRBUS A340 and A380, where it raised no false alarms, even for complex computations involving floating-point numbers. In April 2008, Astrée was able to prove the absence of any runtime error in a C version of the automatic docking software of the
366:
analysis was launched, followed by the aiT WCET Analyzer product line in 2002. In 2004, only half a year after its launch, aiT was awarded a
European Information Society Technology Prize for "groundbreaking products that represent the best of European innovation in information society technologies".
460:
Wilhelm, Reinhard; Engblom, Jakob; Ermedahl, Andreas; Holsti, Niklas; Thesing, Stephan; Whalley, David; Bernat, Guillem; Ferdinand, Christian; Heckmann, Reinhold; Mitra, Tulika; Mueller, Frank; Puaut, Isabelle; Puschner, Peter; Staschulat, Jan; Stenström, Per (2008). "The Worst-Case
Execution-Time
390:
at the
Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by
339:) architectures. Since 2015 AbsInt offers commercial licenses, provides industrial-strength support and maintenance, and contributes to the advancement of the tool. For the development of CompCert,
304:. Its intended use is the compilation of safety-critical and mission-critical software written in C and meeting high levels of assurance. It produces machine code for the
286:
analysis tool that combines static path analysis and static value analysis with non-intrusive real-time instruction-level tracing to bound the worst-case execution time (
543:
Technical
Support to the National Highway Traffic Safety Administration (NHTSA) on the Reported Toyota Motor Corporation (TMC) Unintended Acceleration (UA) Investigation
240:. It is used in the Defense/Aerospace, Medical, Industrial Control, Electronic, Telecom/Datacom and Transportation industries. Astrée originates from the group of
230:. The analysis results are valid for all inputs and each task execution. StackAnalyzer is used in the Aerospace, Medical, Telecom and Transportation industries.
609:
Black, Paul; Walia, Kanwardeep (2020). NISTIR8304 -- SATE VI Ockham Sound
Analysis Criteria (Report). US National Institute of Standards and Technology (NIST).
236:
is a static program analyzer that proves the absence of run-time errors in safety-critical embedded applications written or automatically generated in
786:
447:
Efficient
Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors
212:
252:
and is developed and distributed by AbsInt under license from the CNRS/ENS. In the 6th Static
Analysis Tool Exposition (SATE VI) of
179:. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of
662:
79:
383:, making it the first embedded-software development environment worldwide to feature WCET and stack analysis at the model level.
776:
771:
400:
737:
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
276:
781:
679:. Proceedings of the 5th International Workshop on Worst-case Execution Time (WCET '05), Mallorca, Spain. pp. 21–24.
372:
34:
506:
Ferdinand, Christian; Wilhelm, Reinhard (1999). "Fast and
Efficient Cache Behavior Prediction for Real-Time Systems".
191:. Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.
226:
StackAnalyzer determines the maximum stack usage of the tasks in embedded applications and can prove the absence of
418:, such as DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, and others.
42:
675:
Souyris, Jean; Le Pavec, Ervan; Himbert, Guillaume; JĂ©gu, Victor; Borios, Guillaume; Heckmann, Reinhold (2005).
556:
Ferdinand, Christian; Heckmann, Reinhold (2007). "Static Memory and
Execution Time Analysis of Embedded Code".
38:
249:
692:
Combining a High-Level Design Tool for Safety-Critical
Systems with a Tool for WCET Analysis on Executables
404:
272:
233:
363:
739:. Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 238–252.
344:
287:
283:
207:. It directly analyzes binary executables and takes the intrinsic cache and pipeline behavior of the
200:
135:
Founders: Christian Ferdinand, Daniel Kästner, Marc Langenbach, Florian Martin, Stephan Thesing, and
690:
Ferdinand, C.; Heckmann, R.; Le Sergent, T.; Lopes, D.; Martin, B.; Fornari, X.; Martin, F. (2008).
475:
640:
630:
Alt, Martin; Martin, Florian (1995). "Generation of Efficient Interprocedural Analyzers with PAG".
376:
426:
422:
309:
220:
188:
635:
470:
371:, the world's largest passenger aircraft. In 2006, the Analyzers successfully passed the first
237:
355:
AbsInt is a 1998 spin-off from the Department for Programming Languages and Compilers at the
380:
8:
707:
Proceedings of the 14th Intl. Static Analysis Symposium (SAS'07), Kongens Lyngby, Denmark
677:
Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation
411:
356:
184:
523:
488:
407:. Since 2009 Astrée is commercially available from AbsInt under license from ENS/CNRS.
204:
527:
449:. Proceedings of the 29th International System Safety Conference ISSC2011 Las Vegas.
256:(2020), Astrée was confirmed to satisfy the SATE VI Ockham Sound Analysis Criteria.
645:
610:
597:
565:
558:
SAE 2006 Transactions Journal of Passenger Cars — Electronic and Electrical Systems
515:
492:
480:
180:
136:
387:
241:
227:
208:
724:. Proceedings of 13th Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey.
519:
172:
116:
765:
649:
146:
aiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver
484:
632:
Proceedings of the 2nd International Symposium on Static Analysis (SAS '95)
340:
615:
569:
386:
The development of Astrée started from scratch in November 2001 by Prof.
368:
379:. In 2010, aiT and StackAnalyzer were integrated into SCADE Suite from
291:
268:
705:
Delmas, D.; Souyris, J. (2007). "ASTRÉE: from research to industry".
694:. 4th European Congress ERTS — Embedded Real Time Software, Toulouse.
259:
RuleChecker is a static program analyzer that automatically checks C/
367:
In 2004, aiT was used to analyze the flight-control software of the
290:). This approach works for a wide range of modern high-performance (
587:. Embedded Real Time Software and Systems Congress ERTS², Toulouse.
301:
297:
31:
may have been created or edited in return for undisclosed payments
313:
305:
264:
176:
122:
689:
410:
AbsInt has participated in many research projects funded by the
199:
aiT WCET Analyzer statically computes safe upper bounds for the
336:
332:
324:
223:
in the electronic throttle control systems of Toyota vehicles.
68:
709:. Lecture Notes for Computer Science 4634, Springer: 437–451.
392:
328:
260:
187:. AbsInt specializes in software-verification tools based on
459:
21:
719:
415:
317:
253:
245:
216:
674:
582:
321:
754:
155:
722:
Space software validation using Abstract Interpretation
343:
and the development team of CompCert received the 2021
263:
code for compliance with coding guidelines including
461:
Problem — Overview of Methods and Survey of Tools".
397:
Analyseur statique de logiciels temps-réel embarqués
37:. It may require cleanup to comply with Knowledge's
362:In 2001, the StackAnalyzer product line for static
634:. Lecture Notes in Computer Science (983): 33–50.
555:
763:
505:
444:
171:is a software-development tools vendor based in
720:Bouissou, O.; Conquet, E.; et al. (2009).
583:Kästner, D.; Wilhelm, S.; et al. (2010).
463:ACM Transactions on Embedded Computing Systems
279:, and Adaptive Autosar C++ Coding Guidelines.
213:National Highway Traffic Safety Administration
728:
704:
585:Astrée: Proving the Absence of Runtime Errors
734:
403:(ATV) used for transporting payloads to the
608:
67:
713:
639:
629:
614:
474:
416:German Ministry of Education and Research
735:Cousot, Patrick; Cousot, Radhia (1977).
395:(Paris-Rocquencourt). Astrée stands for
576:
438:
221:Study on Sudden Unintended Acceleration
787:Software companies established in 1998
764:
698:
683:
598:SATE VI Ockham Sound Analysis Criteria
401:Jules Verne Automated Transfer Vehicle
534:
80:Gesellschaft mit beschränkter Haftung
668:
540:
425:, a semantics-based methodology for
300:is a formally verified optimizing C
15:
445:Kästner, D.; Ferdinand, C. (2011).
13:
623:
549:
499:
453:
14:
798:
746:
62:AbsInt Angewandte Informatik GmbH
663:ict-prize.org in web.archive.org
545:(Technical report). p. 151.
421:The name AbsInt is derived from
20:
656:
602:
591:
560:. SAE Technical Paper Series.
1:
777:Software companies of Germany
772:Static program analysis tools
432:
33:, a violation of Knowledge's
7:
782:Companies based in Saarland
405:International Space Station
194:
99:; 26 years ago
89:Software Verification Tools
10:
803:
350:
665:, retrieved on 29.09.2023
541:NASA (January 18, 2011).
345:ACM Software System Award
201:worst-case execution time
150:
142:
129:
111:
93:
85:
75:
66:
650:10.1007/3-540-60360-3_31
520:10.1023/a:1008186323068
485:10.1145/1347375.1347389
427:static program analysis
423:abstract interpretation
282:TimeWeaver is a hybrid
211:into account. The U.S.
189:abstract interpretation
181:Prof. Reinhard Wilhelm
377:Mälardalen University
277:ISO/IEC TS 17961:2013
43:neutral point of view
616:10.6028/NIST.IR.8304
570:10.4271/2006-01-1499
381:Esterel Technologies
412:European Commission
373:WCET Tool Challenge
357:Saarland University
185:Saarland University
63:
61:
508:Real-Time Systems
205:real-time systems
166:
165:
59:
58:
794:
758:
757:
755:Official website
741:
740:
732:
726:
725:
717:
711:
710:
702:
696:
695:
687:
681:
680:
672:
666:
660:
654:
653:
643:
627:
621:
620:
618:
606:
600:
595:
589:
588:
580:
574:
573:
553:
547:
546:
538:
532:
531:
514:(2–3): 131–181.
503:
497:
496:
478:
457:
451:
450:
442:
162:
159:
157:
137:Reinhard Wilhelm
107:
105:
100:
71:
64:
60:
54:
51:
39:content policies
24:
16:
802:
801:
797:
796:
795:
793:
792:
791:
762:
761:
753:
752:
749:
744:
733:
729:
718:
714:
703:
699:
688:
684:
673:
669:
661:
657:
628:
624:
607:
603:
596:
592:
581:
577:
554:
550:
539:
535:
504:
500:
476:10.1.1.458.3540
458:
454:
443:
439:
435:
375:carried out by
353:
219:used it in its
197:
154:
132:
125:
119:
103:
101:
98:
55:
49:
46:
41:, particularly
25:
12:
11:
5:
800:
790:
789:
784:
779:
774:
760:
759:
748:
747:External links
745:
743:
742:
727:
712:
697:
682:
667:
655:
641:10.1.1.37.9598
622:
601:
590:
575:
548:
533:
498:
452:
436:
434:
431:
388:Patrick Cousot
352:
349:
294:) processors.
242:Patrick Cousot
228:stack overflow
209:microprocessor
196:
193:
164:
163:
152:
148:
147:
144:
140:
139:
133:
130:
127:
126:
121:
115:
113:
109:
108:
95:
91:
90:
87:
83:
82:
77:
73:
72:
57:
56:
28:
26:
19:
9:
6:
4:
3:
2:
799:
788:
785:
783:
780:
778:
775:
773:
770:
769:
767:
756:
751:
750:
738:
731:
723:
716:
708:
701:
693:
686:
678:
671:
664:
659:
651:
647:
642:
637:
633:
626:
617:
612:
605:
599:
594:
586:
579:
571:
567:
563:
559:
552:
544:
537:
529:
525:
521:
517:
513:
509:
502:
494:
490:
486:
482:
477:
472:
468:
464:
456:
448:
441:
437:
430:
428:
424:
419:
417:
413:
408:
406:
402:
398:
394:
389:
384:
382:
378:
374:
370:
365:
360:
358:
348:
346:
342:
338:
334:
330:
326:
323:
319:
315:
311:
307:
303:
299:
295:
293:
289:
285:
280:
278:
274:
270:
266:
262:
257:
255:
251:
247:
243:
239:
235:
231:
229:
224:
222:
218:
214:
210:
206:
202:
192:
190:
186:
182:
178:
174:
170:
161:
153:
149:
145:
141:
138:
134:
128:
124:
118:
114:
110:
96:
92:
88:
84:
81:
78:
74:
70:
65:
53:
44:
40:
36:
32:
29:This article
27:
23:
18:
17:
736:
730:
721:
715:
706:
700:
691:
685:
676:
670:
658:
631:
625:
604:
593:
584:
578:
561:
557:
551:
542:
536:
511:
507:
501:
466:
462:
455:
446:
440:
420:
409:
396:
385:
361:
354:
341:Xavier Leroy
296:
281:
258:
232:
225:
215:(NHTSA) and
203:of tasks in
198:
168:
167:
112:Headquarters
76:Company type
47:
35:terms of use
30:
469:(3): 1–53.
369:Airbus A380
364:stack usage
173:SaarbrĂĽcken
117:SaarbrĂĽcken
766:Categories
433:References
292:multi-core
269:SEI CERT C
131:Key people
50:March 2021
636:CiteSeerX
471:CiteSeerX
335:(32- and
528:28282721
414:and the
302:compiler
298:CompCert
195:Products
143:Products
86:Industry
493:2139310
351:History
314:AArch64
306:PowerPC
265:MISRA C
177:Germany
158:.absint
151:Website
123:Germany
102: (
94:Founded
638:
526:
491:
473:
337:64-bit
333:RISC-V
331:, and
325:32-bit
267:/C++,
234:Astrée
169:AbsInt
524:S2CID
489:S2CID
393:INRIA
329:AMD64
318:IA32
312:and
288:WCET
284:WCET
254:NIST
246:CNRS
217:NASA
160:.com
104:1998
97:1998
646:doi
611:doi
566:doi
516:doi
481:doi
327:),
322:x86
310:ARM
273:CWE
261:C++
250:ENS
244:at
183:at
156:www
45:.
768::
644:.
564:.
522:.
512:17
510:.
487:.
479:.
465:.
429:.
347:.
316:,
308:,
275:,
271:,
175:,
120:,
652:.
648::
619:.
613::
572:.
568::
562:9
530:.
518::
495:.
483::
467:7
320:(
248:/
238:C
106:)
52:)
48:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
