Videos

ACM Software System Award 2021

Xavier Leroy, Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan are the recipients of the ACM Software System Award for the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness.

Can you trust your compiler? — With CompCert, you can!

Recording of a free VectorCAST webinar, held on 8 June 2021 in co-operation with Vector.

  • Terminology: Compiler validation vs. compiler verification
  • Introduction to formal compiler verification
  • Benefits of formally verified compilation
  • Experimental evaluation of CompCert performance
  • Tool qualification strategy for industry norms such as ISO 26262

EnergyAnalyzer — static energy analysis for embedded applications

A brief introduction to EnergyAnalyzer, our newest static analyzer for development of embedded systems with energy constraints. Currently available for ARM Cortex-M0 and LEON3.

CompCert presentation for the MORAL project

A brief introduction to the formally-verified CompCert compiler, recorded for the MORAL project in August 2021.



Subscribe to our YouTube channel to be notified of future videos.

a³ 23.10

  • TLS-encrypted network connections between the tools and the License Manager 0:20
  • GUI improvements 5:14
  • Improved interactive value analysis 9:35
  • TimeWeaver improvements 12:12
  • New AIS2 annotations 14:23

Astrée and RuleChecker 23.10

  • Improved call graph view 1:22
  • New project wizard with JSON compilation database importer 2:40
  • New data race report 3:54
  • TLS encryption between analysis servers, Astrée clients, and the License Manager 5:03
  • External user authentication via OpenID Connect (OIDC) 6:02
  • Additional tooltips for value ranges of all subexpressions 6:49
  • Dynamic memory blocks now shown in the Data Flow view 7:27
  • Rule checks for compliance with MISRA C:2023 8:32
  • Diff-based comments 9:05
  • C++ improvements for std::vector and std::string 11:06


a³ 23.04

  • StackAnalyzer/ValueAnalyzer/TimingProfiler for MIPS RL78
  • Analysis of dynamically linked ELF executables for ARM, PowerPC, RISC-V and x86
  • Improved and additional statistics
  • Improved TraceVisualizer
  • Support for TargetLink 2022-B


a³ 22.10

  • Support for AURIX 2nd Gen TC33x, TC35x, TC36x
  • Support for microMIPS32 ISA v3 and v5 and MIPS DSP Module for MIPS32
  • Support for Lauterbach Trace32 BRANCHFLOW export trace format
  • Improved analysis performance and precision


a³ 22.04

  • GUI improvements 0:01
  • Value analysis 3:27
  • TraceVisualizer and TimeWeaver 6:11
  • New annotations 15:17


a³ 21.04

Astrée and RuleChecker 21.04

  • Automatic import of preprocessor configuration from JSON
  • Support of AUTOSAR projects with multiple ARXML files
  • Bounded analysis to obtain incomplete results in shorter time
  • Improved precision
  • State machine domain for C++ analyses
  • Stub implementations for standard library containers
  • Enhanced coverage of MISRA C:2012 and AUTOSAR C++14
  • New options to warn about memory leaks


a³ 20.10

  • Improved workspaces 0:38
  • Unified Symbols and DWARF view 11:01
  • Revamped Disassembly view 13:47
  • Variable-usage statistics 15:12
  • Analysis concurrency level 16:14
  • TriCore-specific changes 18:00
  • Value analysis improvements 21:21
  • Analyzing C++ code 32:28
  • New AIS2 annotations 37:22


a³ 20.04

  • Support for the DDC-I SCORE compiler (PowerPC) and the Renesas CS+ compiler (RH850/V850)
  • Support for Windows color schemes (dark mode)
  • Relaxed license handling and general improve­ments for ValueAnalyzer
  • New consistency check for stack analyses
  • New running task-mode analysis in TimeWeaver
  • Several improvements to the AIS2 annotation language

Astrée and RuleChecker 20.04

  • Improved reporting of annotation insertion errors
  • Automatic filtering of the assembler statement asm {…}
  • One alarm replaced by a diagnostic rule
  • Improved alarm reporting for RuleChecker C++
  • Rule set T now available for C++


a³ 19.10

  • GUI improvements 0:40
  • TimeWeaver improvements 4:56
  • Improved value analysis 10:50
  • New and improved annotations 14:04

Astrée and RuleChecker 19.10

  • Blacklisting/whitelisting files and folders in RuleChecker configu­rations 0:26
  • C++ code metrics 2:16
  • Improved alarm reporting 3:01
  • Notifications removed 4:59


a³ 19.04

  • Improved license management 0:22
  • Cross-referencing analysis results 4:18
  • Full project search 11:06
  • Improved DWARF lookup 13:45
  • TimeWeaver improvements 15:14
  • Value analysis for all entry points 20:49


a³ 18.10

  • AIS annotations 0:19:
    • New default mapping 0:26
    • New AIS functors 1:14
    • New annotation scope 4:10
  • GUI improvements 7:42:
    • Interactive analyses 7:42
    • Workspace export 11:39
  • Improvements to TimeWeaver 13:07:
    • Interactive MCDS tracing 15:13
    • Trace streaming demo 16:28


a³ 18.04

  • AIS annotations 0:18:
    • Value partitioning 0:18
    • Annotating call targets from DWARF view 11:36
  • Trace-iterative decoding 15:28
  • GUI improvements 20:42
  • Improvements to TimeWeaver 26:08

Astrée and RuleChecker 18.04

  • Rule checks for C++ code 0:14
  • CompCert integration 3:04
  • macOS support 4:09


a³ 17.10

  • Floating licenses 0:31
  • Concurrent analyses 3:01
  • C++ Virtual Call Target Analyzer 5:38
  • C++ type inheritance graphs 13:17
  • Excluding subgraphs 14:38
  • Hybrid WCET analysis with TimeWeaver 16:49

Astrée and RuleChecker 17.10

  • New comment mode 1:02
  • Dealing with uninitialized reads 7:12
  • Improved wrapper generator 9:47
  • Support for GCC-extended assembly 13:29
  • Improved handling of invalid function calls 16:21
  • Re-categorization of MISRA rules 22:07
  • Improved support for TargetLink 28:06


a³ 17.04

  • Context-sensitive help 0:30
  • New AIS Files view 3:27
  • New Statistics view for timing contributions of code snippets 6:13
  • AIS2 Standard Mode vs AIS1 Legacy Mode 10:29
  • Improved creation of project archives for support requests 12:27
  • Local call-string increase 14:12
  • Unrolling for recursive functions 16:54
  • Irreducible loops and recursions 17:40
  • Support for C++ namespaces 19:58

a³ 16.10

  • Workspaces 0:03
  • Point-and-click annotations 6:02
  • Project file generator 16:18
  • Stack area specifications 19:30
  • Jenkins plugin 21:28
  • Extended AIS annotations 25:59:
    • Collecting initializations 26:03
    • Annotating tail calls 27:56
    • New functors end and offset 28:38

a³ 16.04

  • Automatic variable initialization analysis
  • Advanced C++ support
  • New AIS2 features
  • Memory Usage view
  • Import of ORTI files (OSEK/AUTOSAR)

Company presentation

A two-minute introductory video.



StackAnalyzer presentation and demo

A 15-minute introduction to finding the worst-case stack usage of tasks in embedded systems.

RuleChecker plugin for KEIL

A short tutorial on installing the RuleChecker plugin in KEIL µVision and running RuleChecker from within your µVision environment.



WCET analysis on modern processors

Part 1: Introduction

An introduction to statically determining the worst-case timing behaviour of tasks in safety-critical embedded systems running on modern high-end processors.

Part 2: aiT WCET Analyzer

Tool presentation and demo of static WCET analysis of an example application for the Infineon AURIX architecture.


Part 3: TimeWeaver

Tool presentation and demo of hybrid WCET analysis of an example application for the Infineon AURIX architecture.



Subscribe to our YouTube channel to be notified of future videos.