AbsInt Astrée
Online Course

Learn how to use Static Analysis tool based on the Abstract Interpretation so you can prove the absence of runtime errors and data races.



Write your awesome label here.

AbsInt Astrée Course,

This course is a deep dive into static analysis of safety-critical applications.

This course provides comprehensive coverage of Static Analysis and Abstract Interpretation, the design and usage of the static analyzer Astrée which aims to formally prove the absence of runtime errors and data races. It also covers the RuleChecker module to check coding guidelines and compute code metrics. The course features practical exercises with the tool for each topic.

This course is aimed at software validation and verification engineers, QA engineers and developers of safety-critical code. After completing this comprehensive training, you will have the necessary skills to:

  •     Set up your own Astrée analyses
  •     Investigate and review findings
  •     Automate analyses and integrate them into the development process
  •     Deeper understand state-of-the-art static program analysis
  •     Write safer, more robust C code
 

Structure:

Online Zoom Training
10 students max

Scope:

4 Hours per module.
6 Sessions
24 hours total training

Detailed Agenda:

  1.     General Introduction
  2.     Foundations of Static Analysis and Abstract Interpretation
  3.     Checking Coding Guidelines
  4.     Astrée Key Concepts: The Sound Analyzer
  5.     The Static Analysis Ecosystem
  6.     Efficiently Working with Astrée and RuleChecker
  7.     Modeling the Environment
  8.     Data Races and Deadlocks
  9.     Minimizing False Alarm Rate
  10.     Model-based Code Analysis
  11.     Automating Astrée Analyses
Write your awesome label here.

Created by

Dr. Jörg Herter

Jörg Herter studied Computer Science and received his Ph.D. on predictable dynamic memory allocation for hard real-time systems in 2014. He has been a research fellow at Saarland University and the University of Applied Sciences in Saarbrücken. His current work is focused on functional safety and the formal validation and verification of safety-critical software. Jörg Herter works as a Senior Technical Consultant for AbsInt. He teaches static program analysis, embedded systems technology, compiler construction, and mathematics at the Saarland University of Applied Sciences and Cooperative Education. Jörg is also a lecturer at the University of Luxembourg.