Please log in to watch this conference skillscast.
This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware. You implement the semantics of a custom industrial instruction-set architecture in Haskell as an EDSL and perform symbolic execution of machine code programs to generate verification conditions which are later discharged with an SMT solver.
Using this methodology, you verify the functional correctness of programs and perform worst-case execution time analysis.
YOU MAY ALSO LIKE:
- Haskell eXchange 2022: Novice Track (Online Conference on 7th December 2022)
- Haskell eXchange 2022: Online Conference (Online Conference on 8th - 9th December 2022)
- Haskell: Why and How the External STG Interpreter is Useful (SkillsCast recorded in December 2021)
- Keynote — Haskell: What To Do When Success Can't Be Avoided (SkillsCast recorded in November 2021)