Videos

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.

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

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.

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

• 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

• 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

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

• GUI improvements 0:53
• Value analysis 10:08
• Path analysis 14:22
• New annotations 16:58

• 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

• 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

• 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

• 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++

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

• 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

• 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

• 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

• 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

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

• 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

• 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 two-minute introductory video.

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

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

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

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

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