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 ﬁrst 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
veriﬁcation, providing a mathematical proof that no behavior can yield
an error. Software veriﬁcation 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
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
Cortier (scientific organizer)
- Christelle Pierron