Symbolic Computation and Deduction
in System Design and Verification
Motivation
In the last years, interest in applying methods from computer algebra to
various problems in system design, verification and control has increased.
Precise symbolic computation techniques are needed e.g. in order to
properly handle parameters in parametric descriptions of systems.
In particular, parametric/non-convex constraint solving and
optimization methods are used in plant design.
In fact, numerous problems in science and engineering, in particular
problems which occur in the verification of parametric reactive and
hybrid systems, can be reduced to reasoning in complex theories –
typically combinations of concrete theories (e.g. theories of
integers or reals) and abstract theories (e.g. theories of data
structures). Therefore, finding methods for efficiently combining
deductive techniques with symbolic computation techniques and devising
parametric variants of computer algebra and deduction algorithms will
have a significant impact in these areas.
Aims
The goal of this session is to enhance the interaction between the
symbolic computation, automated reasoning and verification communities.
The session is devoted to research on:
- mathematical theories, which have a direct practical application,
- algorithms (symbolic, symbolic-numeric),
- software libraries/packages,
- applications in science and engineering
The main aim of this session is to stimulate collaborations among researchers working in:
- symbolic computation (e.g. comprehensive Gröbner bases, quantifier
elimination);
- deduction and automated reasoning, in particular in theorem proving
over complex domains, which explicitly make use of computer algebra methods;
- SAT-checking – including methods that go beyond traditional SAT-checking
(e.g. QSAT, parametric SAT, SAT modulo theories);
- the design, verification, and control of real time and hybrid systems.
as well as among researchers interested in using symbolic computation
systems and systems for automated deduction for solving concrete problems
in verification and control.
This will help in
- investigating computational issues in the control design methodology
yielding parametric optimization,
- identifying interesting problems in deduction and symbolic
computation stemming from the verification of reactive and hybrid
systems, and
- clarifying the expectations and wishes the users from verification
and control have from symbolic computation systems or from systems
which combine deduction and computation.
The ultimate aim is to expand the horizons of this area of
research, deepen the interactions, sensibilize researchers from
the symbolic computation and deduction community to the problems
occurring in verification, and, conversely, the researchers in
verification to the newest symbolic computation systems and methods
and — last but not least — offer persons working in research and
development centers of software companies the possibility to get an
overview of the problems and their solutions.