Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?

Marc Schoolderman, Sjaak Smetsers, M.C.J.D. van Eekelen

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

Software engineers working in industry seldom try to apply formal methods to solve problems. There are various reasons for this. Sometimes these reasons are understandable---the cost of using formal methods does not make economic sense in many contexts. However, formal methods are also often greeted with scepticism. Formal methods are assumed to take too much time, require tools that are too academic, or to be too mathematical to be understood by practice-oriented software engineers. We tested these assumptions by designing a small course around a framework for program verification, aimed at regular computer science students enrolled in a Master's programme. After four lectures and associated exercises, students were given a small verification task where they had to model and verify a real, non-trivial, C function in Why3. A significant majority of students managed to prove a non-trivial functional specification of this C function in the time allotted, and many also pointed out inherent flaws of this function discovered during formalization. Participants reported no major difficulties or mental hurdles in learning Why3, and considered its approach to be appropriate for selected components of safety-critical software. While formal verification tools such as Why3 still have lots of room for improvement, this experience shows that in a short amount of time, software engineers can be taught to use a program verification tool, and obtain usable results without being fully proficient in it. We further recommend that courses on formal methods should also let students explore these as techniques to be applied, instead of only focusing on the theory behind them, as we expect this to gradually lower the barrier to wider acceptance.
Original languageEnglish
Title of host publicationCSERC '19
Subtitle of host publicationThe 8th Computer Science Education Research Conference
EditorsEbrahim Rahimi, Dave Stikkolorum
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery (ACM)
Pages50-57
Number of pages8
Edition1
ISBN (Electronic)9781450377171
DOIs
Publication statusPublished - Nov 2019
Event8th Computer Science Education Research Conference (CSERC'19) - University of Cyprus, Larnaca, Cyprus
Duration: 18 Nov 201920 Nov 2019
Conference number: 8

Conference

Conference8th Computer Science Education Research Conference (CSERC'19)
Abbreviated titleCSERC
CountryCyprus
CityLarnaca
Period18/11/1920/11/19

Fingerprint Dive into the research topics of 'Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?'. Together they form a unique fingerprint.

Cite this