Analysing programs: logic to the rescue
INRIA logo                                                                LORIA logo
Symposium affiliated to CLMPS  

July 22nd, 2011

Scope | Invited speakers | Program (with slides) | Registration | Organizers | Venue

Location: Room K12, faculty of Law of Nancy

It is well known that software contains bugs. While this might be acceptable on its personal computer, this is no longer the case with critical systems such as embedded systems used on planes, cars or pacemakers. The first approach to detect and correct bugs is of course to perform tests, possibly in an automated way. However, this allows to explore only a limited number of potential behaviors. For critical systems, a much higher level of guarantees is obtained through formal verification, providing a mathematical proof that no behavior can yield an error. Software verification makes use of formal models, intrinsically based on logic. The goal of this workshop is to explore how logic is a major ingredient for analysing computer systems.

The symposium will be hosted by the faculty of Law of Nancy. More information on the congress web site.

Invited speakers
The affiliated symposium will consist of six invited talks.

The program with titles and abstracts of the talks can be found here.

All participants must be registered to the CLMPS congress, see the registration webpage.