with traditional methods would incur huge expression swell and high complexity. Indeed, many problems related to this one are provably intractable, or suspected to be so. Nonetheless, recent work has yielded exciting new algorithms for computing with sparse mathematical expressions. In this talk, we will attempt to navigate this hazardous computational terrain of sparse algebraic computation. We will discuss new algorithms for sparse polynomial root finding and functional decomposition. We will also look at the “inverse” problem of interpolating or reconstructing sparse mathematical functions from a small number of sample points. Computations over traditional symbolic domains, such as the integers and finite fields, as well as symbolicnumeric computations for approximate (floating point) data, will be considered. In all cases, algorithms will require time polynomial in the size of the sparse representation of the input and output, and will provably manage coefficient growth, intermediate expression swell, and numerical stability as appropriate to the problem. A constraint for optimal parameter estimation to solve an issue of molecular network models in systems biology One point is definitely different between network modeling in systems biology and that in other scientific fields. The point is that the models including unmeasured variables frequently emerged, so as to measure the variables under the conditions with as less perturbation to the organism as possible. To consider the point specific to systems biology, we have designed a method by symboliccomputation approach, to estimate kinetic parameter values with a high degree of accuracy. First, we utilize differential elimination, which is an algebraic approach for rewriting a system of differential equations into another equivalent system, to derive the constraints between kinetic parameters from differential equations. Second, since its equivalent system is frequently composed of large equations, the system is further simplified by another symbolic computation. Third, we estimate the kinetic parameters introducing these constraints into an objective function, in addition to the error function of the square difference between the measured and estimated data, in the standard parameter optimization method such as the genetic algorithm (GA) and the particle swarm optimization (PSO). Here, the performance of our method for parameter accuracy improvement is illustrated by the simulation of two representative models in biology, a simple cascade model and a negative feedback model, and the actual data analysis for a signal transduction pathway, in comparison with the previous numerical methods. In addition, we will discuss the merits and pitfalls of the present method for further improvements. Verifying programs with support from computer algebra This talk is to report the recent achievements of our joint project in using Computer Algebra to verify software and hybrid systems. In the talk, we will explain the main ideas of a symbolic decision procedure for termination of linear programs, which can avoid rounding error leading to a wrong conclusion, a complete algorithm to generate semialgebraic invariants for polynomial dynamical systems, and also a language and a calculus to model and verify hybrid systems based on the invariants. 
Invited Speakers Engineering arithmetic constraint solvers for the analysis of hybrid discretecontinuous systems Hybrid discretecontinuous dynamic behavior arises when discrete and continuous dynamic processes become connected, as in the case of embedded computers and their physical environment. An increasing number of the technical artifacts shaping our ambience are relying on embedded computer systems which do interact with their environment in a complex and often safetycritical manner, having sensitive variables of the environment in their sphere of control. Everyday examples include process control at all scales, ranging from household appliances to nuclear power plants, or embedded systems in the transportation domain, such as adaptive cruise control in automotive, aircraft collision avoidance protocols in avionics, or automatic train control applications, including the socalled movingblock principle allowing increased traffic density on highspeed tracks while ensuring collision avoidance. Within this talk, we concentrate on automatic verification and analysis of such hybrid systems, with a focus on mixed numericsymbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicative encodings and dedicated constraint solvers. We provide a brief introduction to hybrid discretecontinuous systems, demonstrate the use of predicative encodings for concisely encoding operational highlevel models, and continue to a set of constraintbased methods for automatically analyzing different classes of hybrid discretecontinuous dynamics. Covering the range from nonlinear discretetime hybrid systems to probabilistic hybrid systems, advanced arithmetic constraint solvers will be used as a workhorse for manipulating large and complexstructured Boolean combinations of arithmetic constraints arising in their analysis tasks. Sparsity and complexity in algebraic computation Modern symbolic computation systems provide an expressive language for describing mathematical objects. For example, we can easily enter equations such as 
into a computer algebra system. However, to determine the factorization 
Wednesday, October 19 
Thursday, October 20 
Friday, October 21 
Tentative Program 
08:459:00 
Opening 

Session chair: Dongming Wang 
09:0010:00 
Verifying programs with support from computer algebra 
10:0010:30 
Coffee Break 

Session chair: Naijun Zhan 
10:3011:00 
Proving total correctness of loop programs via symbolicnumeric computation method Wang Lin, Min Wu, Zhengfeng Yang and Zhenbing Zeng 
11:0011:30 
Superposition as a decision procedure for timed automata Arnaud Fietzke and Christoph Weidenbach 
11:3012:00 
An approach of modeling and analyzing data gathering protocol Kang He, Hongli Yang, Zongyan Qiu and Meng Sun 
12:0012:30 
The nonArchimedean theory of discrete systems Vladimir Anashin 
12:3014:00 
Lunch 

Session chair: Marc Moreno Maza 
14:0014:30 
Rational general solutions of trivariate rational systems of autonomous ODEs Yanli Huang, L.X.Chau Ngo and Franz Winkler 
14:3015:00 
Discovering polynomial Lyapunov functions for continuous dynamical systems Zhikun She, Haoyang Li and Bai Xue 
15:0015:30 
Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems Jiang Liu, Naijun Zhan and Hengjun Zhao 
15:3016:00 
Coffee Break 

Session chair: Katsuhisa Horimoto 
16:0016:30 
Nonlinear analysis of a class of double saturated polymolecular reversible biochemical reactions Jinliang Wang, Jing He and Wei Feng 
16:3017:00 
An efficient model predictive control with constraints using a simple explicit control law Yuhei Umeda and Hirokazu Anai 
17:0017:30 
Diagonal interacting multiple model algorithm based on $H_\infty$ filtering Xiaoyan Fu, Yingmin Jia and Cuiping Li 
18:0020:00 
Dinner 

Session chair: Bican Xia 
09:0010:00 
A constraint for optimal parameter estimation to solve an issue of molecular network models in systems Katsuhisa Horimoto 
10:0010:30 
Coffee Break 

Session chair: Martin Fränzle 
10:3011:00 
A coinductive calculus for QoSaware generic components composition Luis S. Barbosa and Sun Meng 
11:0011:30 
On the implementation of cubic public keys based on algebraic graphs over the finite commutative ring and their special symmetries Michal Klisowski and Vasyl Ustimenko 
11:3012:00 
A New Family of pary Sequences with Low Correlation Constructed from Decimated Sequences Yongbo Xia 
12:0012:30 
PreGalois connection for generic statebased components refinement Sun Meng 
12:3014:00 
Lunch 

Session chair: Stefan Ratschan 
14:0015:00 
Engineering arithmetic constraint solvers for the analysis of hybrid discretecontinuous systems Martin Fränzle 
15:0015:30 
CXSC, a sophisticated environment for reliable computing Walter Krämer 
15:3018:30 
Excursion to Prince Gong's Mansion and Shicha Lake 
19:0021:30 
Banquet 

Session chair: Lihong Zhi 
09:0010:00 
Sparsity and complexity in algebraic computation Mark Giesbrecht 
10:0010:30 
Coffee Break 

Session chair: Marc Giusti 
10:3011:00 
Solving semialgebraic systems with the RegularChains library in Maple Changbo Chen, James Davenport, François Lemaire, Marc Moreno Maza, Nalina Phisanbut, Bican Xia, Rong Xiao and Yuzhen Xie 
11:0011:30 
Improved bounds for continued fractions variants for real root isolation Elias Tsigaridas 
11:3012:00 
The irreducibility of polynomials with coefficients in a unique factorization domain He Miao, Li Yongbin and He Cong 
12:0012:30 
SUP(T) decides firstorder logic fragment over ground theories Evgeny Kruglov and Christoph Weidenbach 
12:3014:00 
Lunch 

Session chair: Mark Giesbrecht 
14:0014:30 
Solving curve completion problems with discrete invariants Jun Zhao and Elizabeth Mansfield 
14:3015:00 
Point searching in real singular complete intersection varieties – algorithms of intrinsic complexity Bernd Bank, Marc Giusti and Joos Heintz 
15:0015:30 
On solving parametric polynomial systems Marc Moreno Maza, Bican Xia and Rong Xiao 
15:3016:00 
Closing 
18:0020:00 
Dinner 