Informace o projektu

Anotace je dostupná pouze v anglickém jazyce.

Embedded software is becoming ubiquitous and is affecting our lives in ever
more situations. It controls cyber-physical systems, computational devices interacting
with physical reality, in particular often also with human beings. These
devices—be it automatic cruise control or pacemaker—must perform their task
safely in their environment in all possible situations. This critical requirement
induces the need to identify important operational system properties that are
to be verified on the systems. The verification process then guarantees, with
arguable certainty, that the resulting behaviour is correct with respect to these
properties. The increasing software complexity gradually prohibits manual efforts
when striving for these guarantees, whereas automatic verification and
controller synthesis become a key opportunity to change the way software is
produced, making it safe and reliable as well as cheaper and more efficient. However,
while hardware verification was industrialized already in 90s and software
verification becomes an industrial standard in many safety- or dependabilitycritical
domains, automatic verification and synthesis of controllers have not
reached the industrial scale yet, despite considerable advances over the past
decades.