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.

Course type	Seminar
Instructors	Bernd Westphal, Daniel Dietsch, Sergio Feo-Arenis, Marius Greitschus
Kick-Off	5.5.2014, 14:00 - max. 18:00, c.t.
Presentation	tba.
Presentation language	English
Credits	4
Course Catalog	Formal Methods for C

News

2014-08-05: the schedule:
1. 9:30 - 9:45 - Opening
2. 9:45 - 10:30 - frama-C Value Analysis
3. 10:30 - 11:15 - Astree
4. 11:15 - 12:00 - Blast
5. 12:00 - 13:00 - Lunch break
6. 13:00 - 13:45 - CPAChecker
7. 13:45 - 14:30 - CBMC
8. 14:30 - 14:45 - Coffee break
9. 14:45 - 15:30 - VCC
We will be there from 9:15 the latest in order to check whether personal presentation equipment and beamer understand each other.

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.

Resources

Virtual Machine

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.

Examples

scan_ushort.c
Low Battery Controller (Exercise Sheet, Framework)
cat.c

Slides

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)

Description

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.

Important Dates

June 30, 2014: Finished "Theory behind the Tool" part of the talk
July 14, 2014: Finished structure of the talk
To be announced: Presentations

Formalia

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.