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.
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.
Subscribe to our YouTube channel to be notified of future videos.
asm {…}
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.
Subscribe to our YouTube channel to be notified of future videos.