Seminar Formal Methods for C
Despite its age, the C programming language is still popular for embedded systems software in particular for critical tasks. In this seminar, we will investigate methods and tools which promise to support us in proving C programs correct with respect to a given specification or in finding generic errors like segmentation faults. After a short lecture block on the C programming language, each participant group is supposed to implement solutions to some small problems that we provide. Afterwards, each group will set out to prove some other implementations and the own code correct. In a final seminar block, each group is supposed to report on the tool they used, the technique behind the tool and consequently expected strengths and weaknesses, and experience with the implementations.
|Instructors||Bernd Westphal, Daniel Dietsch, Sergio Feo-Arenis, Marius Greitschus|
|Kick-Off||5.5.2014, 14:00 - max. 18:00, c.t.
|Course Catalog||Formal Methods for C|
- 2014-08-05: the schedule:
- 9:30 - 9:45 - Opening
- 9:45 - 10:30 - frama-C Value Analysis
- 10:30 - 11:15 - Astree
- 11:15 - 12:00 - Blast
- 12:00 - 13:00 - Lunch break
- 13:00 - 13:45 - CPAChecker
- 13:45 - 14:30 - CBMC
- 14:30 - 14:45 - Coffee break
- 14:45 - 15:30 - VCC
- 2014-08-01: the block seminar will take place in room 106-0-007, schedule tba.
- 2014-07-18: the block seminar will take place on Thursday, 7th of August, 2014. Place (in university) and schedule tba.
- 2014-06-25: third verification task online, the source code of the Unix utility cat(1)
- 2014-05-20: same room, same time - final introductory lectures on C will take place in 101-00-036 at 16-18
- 2014-05-15: room change - next introductory lectures on C will take place in 101-00-036, time is unchanged, 16-18
- 2014-05-09: battery low controller programming can start - library available for download
- 2014-05-05: time changed - introductory lectures on C will take place Monday, 16-18, room is unchanged, Geb. 082 Pool 00-029.
- 2014-03-31: Homepage - if you have further questions on this seminar, don't hesitate to contact us.
The virtual machine image with all the aforementioned tools (except VCC) installed can be downloaded here, either in tar.gz or in zip format:
Note that these links only work from inside the University's network.
The username for the virtual machine is sfmfc, the password is sfmfc as well.
- 2014-05-05: Kickoff-Meeting (Slides)
- 2014-05-12: Introductory Talk: Formal Methods for C, Part 1 (Slides (with annot.), 2-up, 6-up, Recording)
- 2014-05-19: Introductory Talk: Formal Methods for C, Part 2 (Slides (with annot.), 2-up, 6-up, Recording)
- 2014-05-26: Introductory Talk: Formal Methods for C, Part 3 (Slides (with annot.), 2-up, 6-up, Recording)
This seminar will be structured as follows:
- 1st/2nd week of lecture period (Monday, afternoon, with recording): Lecture Phase
- 2-3 lectures on C concepts and tools in one of the pool rooms (not a programming course!, prior experience with Java or a similar language is a necessary premise for the seminar)
- includes hands-on mini implementation tasks and simple C programming assignment
- 3rd to last week: Individual Work
- C programming task: state-based controller (for a simple system; details tba)
- get acquainted with your chosen tool, research the background of the underlying technique, possibly research whether your chosen tool has been compared to others in the literature
- reproduce examples from the manual/tutorial, prove at least one non-trivial property not in the documentation and find at least one non-trivial bug (after changing the example, if needed)
- apply your chosen tool to three examples including your state-based controller, investigate how well the tool applies to these examples, which code changes are necessary, which bugs are found, which properties can be shown, etc.
- meet with supervisors as needed
- a VirtualBox image with all necessary compilers and verification tools pre-installed will be provided
- after the lecture period: Block Seminar (length depending on no. of groups)
- each group gives a talk on the chosen tool: what the tool aims at, the techniques behind and consequently expected strengths and weaknesses, and the experience during the individual work
- discussion with the audience (which happens to have worked on the same examples and thus should be able to ask profound questions)
Date and time for the Kick-off meeting will be announced to the registered participants by mail and on the homepage; at the moment good candidates are Monday, 28.4.2014 or Monday, 5.5.2014, 14:00, Geb. 082 Pool 00-029.
- June 30, 2014: Finished "Theory behind the Tool" part of the talk
- July 14, 2014: Finished structure of the talk
- To be announced: Presentations
The grade is determined by (content and style of) the (at least 30 min., at most 45 min.) presentation in the block seminar phase, cf. details in kickoff meeting slides.
- Astrée Run-Time Error Analyzer
- BLAST - Berkeley Lazy Abstraction Software verification Tool
- CBMC - Bounded Model-Checking for ANSI-C
- CPAchecker - The Configurable Software-Verification Platform
- ESBMC - Efficient SMT-Based Context-Bounded Model Checker
- Frama-C Software Analysers, plugins 'wp' and 'value analysis'
- LLBMC - the low-level bounded model checker
- Ultimate Automizer
- VCC - A Verifier for Concurrent C
Related Links, Literature
- Competition on Software Verification (SV-COMP)
- Brian W. Kernighan, Dennis Ritchie: The C Programming Language, Prentice Hall.