Scheduling
11. März 2021
with Michael Roitzsch
State of Hardware 2020
24. Dezember 2020
with Werner Haas
HelenOS
15. September 2020
with Martin Decky
Formal Methods
10. August 2020
with Marius Melzer
Intel SGX
23. Juni 2020
with Jo Van Bulck
L4 and L4Re
09. Mai 2020
with Michael Hohmuth
Contact Tracing Apps
23. April 2020
with Michael Roitzsch
Sustainability
01. März 2020
with Michael Engel
Genode Labs
06. Februar 2020
with Norman Feske
Ada and SPARK
20. Dezember 2019
with Alexander Senier
Show Notes and Links
Flo and Julian talk to Alexander Senier about Ada, SPARK and how to build reliable and trustworthy software. We also talk about Alexander’s company, Componolit.
- Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly.
- Send feedback to podcast@ukvly.org or via Twitter.
Resources to get started
- awesome Ada: A curated list of awesome resources related to the Ada and SPARK programming language.
- learn.adacore.com
- Free book: Safe and Secure Software - An invitation to Ada 2012
- Implementation Guidance for the Adoption of SPARK
- John W. McCormick, Peter C. Chapin: Building High Integrity Applications with SPARK
- Ada for the C++ or Java Developer
- Rust and SPARK: Reliability for Everyone (the statements on SPARK pointers are outdated!)
- Alire: the Ada package manager
- Ada Devevelopers room at FOSDEM
Low-level and systems programming resources
- Ada Bare Bones
- Spunky: A kernel using Ada
- Ada drivers library
- Ada Operating System development example
Resources specific to component-based systems
- Genode has built-in support for SPARK/Ada
- Muen, a separation kernel fully implemented in SPARK
- Ewok, a microkernel for embedded systems implemented in SPARK
- Gneiss - framework for platform-independent SPARK components running on Genode, Muen and Linux
- RecordFlux - Verifiable message parser/generators in SPARK
- Article: SPARK as an extremum: Components in pure SPARK
