Skip to content
Snippets Groups Projects

Suggested projects


Seer (Nils)

Symbolic execution engine for MIR internal format

  • Study and understand the Z3 API
  • Study and understand the user API (maybe add more functionalty)
  • Study outsets for program verification based on seer

LED Audio (John)

  • Modulate LED colors and intensity according to audio input

Drivers for NXP (Axel)


WCET analysis for RTFM models using KLEE (Henrik)

  • Automated testebed, integrated as cargo sub-command

USB-Hid (Johannes)


ETM Tracing

  • Develop an API for setting up ETM trace ARM

AES Encryption in hardware

  • Develop on API for hardware supported AES encryption

CAN bus API and Wheel Sensor implementation

  • Develop a CAN bus API for cortex-m0
  • Implement a wheel sensor for existing model car

Stack Memory Analysis

  • Seer or KLEE based path/call graph extraction
  • Target code analysis, per function stack usage
  • Static worst case stack analysis for RTFM and/or RTFM-TTA

Ethernet driver for TCP/UDP/IP stack

  • Develop driver and integrate to existing TCP/UDP/IP stack

Nucleo 64 support crate

  • Drivers for the Nucleo 64, stm32f401re/stm32f411re, similar to the f3/bluepill support crates

Time Triggered Architecture (RTFM-TTA)

  • Periodic timers
  • Communication channels/message buffers
  • Static analysis (for safely bound buffers)
  • Static analysis for data aging (opitmal ordering?)

Your ideas...