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 Fundamentals (2-Day Course) with Alejandro Serrano (Online Course on 5th - 6th July 2021)
- Haskell eXchange 2021 (Online Conference on 16th - 17th November 2021)
- LDN *Virtual* Talks Jun 2021 — Concordium Takeover (Online Meetup on 28th June 2021)
- Abstract Fun-sense: a functional perspective on life (SkillsCast recorded in May 2021)
- Resource Analysis with Refinement Types (SkillsCast recorded in May 2021)