Organizers
Motivation
Topics
Program
Abstracts
Registration
Location
RISC, Castle of Hagenberg,
Austria
at ACA 2008
Important Dates
Early registration deadline:July, 7, 2008
The session will take place
on July 29 and 30, 2008
Contact
For further informations please send an e-mail toViorica Sofronie-Stokkermans
Aims
The main aim of this session is to enhance the interaction, and stimulate collaborations among the
symbolic computation, automated reasoning and verification communities, and especially 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;
Topics
Topics of interest are those at the borderline between theoretical research in symbolic computation and deduction and applications. These include, but are not restricted to:- Deductive verification and symbolic computation
Of particular interest are examples from verification of reactive and hybrid systems which illustrate the type of deductive problems appearing in relationship with verification tasks: symbolic computation, decision procedures for numerical (or possibly mixed) domains, deduction, SAT checking, quantifier elimination, interpolation. - Integration of deduction and computation
Of particular interest are possibilities of combining decision procedures or of combining deductive techniques with symbolic computation techniques. - Parametric verification vs parametric deduction and computation
This includes but is not limited to:- loop parallelization,
- software verification,
- analysis and design of differential equations,
- system design in control, signal processing etc.
- Parametric optimization and optimization over parameters
Current computation in modern control is based almost exclusively on standard numerical linear algebra routines. However, computer algebra is gaining importance as a computational tool due to its capability of dealing with parameters, since many problems in practical applications can be reduced to parameter optimization problems. - Applications to:
- verification of real time and hybrid systems,
- control system design and verification,
- manufacturing design and design automation.