Keynote speech and Tutorials
- Keynote speech:
- Andrei Voronkov (University of Manchester)
- Nikolai Tillmann (Microsoft Research)
Pex4Fun: Serious Gaming powered by Symbolic Execution
Pex4Fun (http://www.pex4fun.com/) is a web-based serious gaming environment for learning and teaching programming. With Pex4Fun, a student edits code in any browser, supported by auto-completion. Pex4Fun then executes the code and analyzes it in the cloud. The analysis is based on the automated test generator Pex which uses symbolic execution and the SMT solver Z3 to generate high coverage test suites and find counterexamples to assertions. In particular, Pex4Fun finds interesting and unexpected input values that help students understand what their code is actually doing. The real fun starts with Coding Duels where students write code to implement a teacher's specification. Pex4Fun finds discrepancies in behavior between the student's code and the specification. The student wins when Pex4Fun cannot find any behavioral differences. This tutorial will discuss the technologies that lie behind the Pex4Fun platform, walk through available REST services, show how to use Pex4Fun in teaching and learning, explore existing course materials and illustrate how to create new puzzles.
Nikolai Kosmatov, Virgile Prevosto, Julien Signoles (CEA, LIST, Software Safety Laboratory)
Specification and Proof of Programs with Frama-C
Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in FRAMA-C (Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. In: SEFM 2012. URL: http://frama-c.com/), a freely available software verification toolset. Those who will have FRAMA-C and JESSIE installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of programs on their computer. Program specifications will be written in the specification language ACSL (http://frama-c.com/acsl.html) similar to other specification languages like JML that some participants may know. ACSL syntax is intentionally close to C and can be easily learned on-the-fly. We will also illustrate on several examples how software testing can help in proof failure analysis.
The tutorial is aimed mainly at software engineering students and professionals who will learn more about the state of the art in automated software verification and how it could help them in their career in software development or validation. Using freely available tools FRAMA-C and JESSIE will allow them to quickly install and try the tools. Software engineering lecturers will also be interested in how a tool such as FRAMA-C can help in teaching software verification.
The only necessary background is some familiarity with the C language.
The presenters are researchers at CEA LIST. Nikolai Kosmatov gave several theoretical courses and exercise sessions on proof of programs in 2009-2012. Nikolai co-organized (with Nicky Williams) several successful tutorials on software testing with PATHCRAWLER, another plugin of the FRAMA-C platform, at several international events: TAP 2012, TAROT 2012, ASE 2012 and QSIC 2012 (tutorial materials at http://kosmatov.perso.sfr.fr/nikolai/).
Julien Signoles is one of the main developers of FRAMA-C, he gave several university and training courses on FRAMA-C. His research focused on extensions of the ML language, software security, runtime assertion checking and various applications of static analysis. In particular, he taught proof of programs in 2010-2012.
Virgile Prevosto is one of the developers of FRAMA-C, and was among the organizers of FRAMA-C training sessions in 2009 (Saclay, France) and 2010 (Berlin). He also presented FRAMA-C at the Coq Summer School in Beijing in 2009 and several university courses. His research interests include mainly formal methods and static analysis of programs.