HLL crash course for safety engineers

Beginning May 18th, I led a four-day online crash course on HLL for a dozen safety engineers. Due to the French COVID-19 lockdown, the course was conducted via Microsoft Teams, alternating lectures and exercises. An online course is a very special experience: you can get very close to a student’s activities when sharing terminals and files. At the same time, when someone doesn’t speak or write anything, you can’t even know where they are! I felt that we are not an online course company as is, and this kind of course could be improved by some extra communication tools and personalization. My lectures were live, while recorded ones would allow trainees to set their own pace. I also think that I would make sure the trainees have access to a shared chat, even in a face to face course. This allows rich interactions and stores questions and answers one could revisit anytime.

This course provided a practical introduction to formal verification activities that are encountered in real-world projects. We talked about formalizing requirements, environment modeling through constraints, choosing an appropriate proof strategy and, of course, some debugging. This may sound like it would require a strong background in software engineering to be at ease with the software tools. However, the attendees revealed unexpected skills when digging into PSL – our proof engine – and its associated tools.

As per usual in formal verification, a large amount of time was spent on the corner cases of requirement specification. Indeed, even though safety engineers are used to providing such requirements, they were sometimes surprised when formalization exposed some missing behaviors or lack of precision. Manipulating HLL formulas, especially when quantification enters, is a powerful way to reveal corner cases of even the most simple designs.

Prover would like to congratulate all of the attendees for their patience and enthusiasm during this course, helping to share lessons learned with others. We are happy that more people are now Prover Certified formal verification engineers.