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 symbolic-numeric 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. Katsuhisa Horimoto 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 symbolic-computation 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. Chaochen Zhou 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 semi-algebraic invariants for polynomial dynamical systems, and also a language and a calculus to model and verify hybrid systems based on the invariants.
 Invited Speakers Martin Fränzle Engineering arithmetic constraint solvers for the analysis of hybrid discrete-continuous systems Hybrid discrete-continuous 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 safety-critical 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 so-called moving-block principle allowing increased traffic density on high-speed tracks while ensuring collision avoidance. Within this talk, we concentrate on automatic verification and analysis of such hybrid systems, with a focus on mixed numeric-symbolic 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 discrete-continuous systems, demonstrate the use of predicative encodings for concisely encoding operational high-level models, and continue to a set of constraint-based methods for automatically analyzing different classes of hybrid discrete-continuous dynamics. Covering the range from non-linear discrete-time hybrid systems to probabilistic hybrid systems, advanced arithmetic constraint solvers will be used as a workhorse for manipulating large and complex-structured Boolean combinations of arithmetic constraints arising in their analysis tasks. Mark Giesbrecht 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:45-9:00 Opening Session chair: Dongming Wang 09:00-10:00 Verifying programs with support from computer algebra Chaochen Zhou 10:00-10:30 Coffee Break Session chair: Naijun Zhan 10:30-11:00 Proving total correctness of loop programs via symbolic-numeric computation method Wang Lin, Min Wu, Zhengfeng Yang and Zhenbing Zeng 11:00-11:30 Superposition as a decision procedure for timed automata Arnaud Fietzke and Christoph Weidenbach 11:30-12:00 An approach of modeling and analyzing data gathering protocol Kang He, Hongli Yang, Zongyan Qiu and Meng Sun 12:00-12:30 The non-Archimedean theory of discrete systems Vladimir Anashin 12:30-14:00 Lunch Session chair: Marc Moreno Maza 14:00-14:30 Rational general solutions of trivariate rational systems of autonomous ODEs Yanli Huang, L.X.Chau Ngo and Franz Winkler 14:30-15:00 Discovering polynomial Lyapunov functions for continuous dynamical systems Zhikun She, Haoyang Li and Bai Xue 15:00-15:30 Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems Jiang Liu, Naijun Zhan and Hengjun Zhao 15:30-16:00 Coffee Break Session chair: Katsuhisa Horimoto 16:00-16:30 Nonlinear analysis of a class of double saturated polymolecular reversible biochemical reactions Jinliang Wang, Jing He and Wei Feng 16:30-17:00 An efficient model predictive control with constraints using a simple explicit control law Yuhei Umeda and Hirokazu Anai 17:00-17:30 Diagonal interacting multiple model algorithm based on $H_\infty$ filtering Xiaoyan Fu, Yingmin Jia and Cuiping Li 18:00-20:00 Dinner
 Session chair: Bican Xia 09:00-10:00 A constraint for optimal parameter estimation to solve an issue of molecular network models in systems Katsuhisa Horimoto 10:00-10:30 Coffee Break Session chair: Martin Fränzle 10:30-11:00 A coinductive calculus for QoS-aware generic components composition Luis S. Barbosa and Sun Meng 11:00-11: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:30-12:00 A New Family of p-ary Sequences with Low Correlation Constructed from Decimated Sequences Yongbo Xia 12:00-12:30 Pre-Galois connection for generic state-based components refinement Sun Meng 12:30-14:00 Lunch Session chair: Stefan Ratschan 14:00-15:00 Engineering arithmetic constraint solvers for the analysis of hybrid discrete-continuous systems Martin Fränzle 15:00-15:30 C-XSC, a sophisticated environment for reliable computing Walter Krämer 15:30-18:30 Excursion to Prince Gong's Mansion and Shicha Lake 19:00-21:30 Banquet
 Session chair: Lihong Zhi 09:00-10:00 Sparsity and complexity in algebraic computation Mark Giesbrecht 10:00-10:30 Coffee Break Session chair: Marc Giusti 10:30-11:00 Solving semi-algebraic 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:00-11:30 Improved bounds for continued fractions variants for real root isolation Elias Tsigaridas 11:30-12:00 The irreducibility of polynomials with coefficients in a unique factorization domain He Miao, Li Yongbin and He Cong 12:00-12:30 SUP(T) decides first-order logic fragment over ground theories Evgeny Kruglov and Christoph Weidenbach 12:30-14:00 Lunch Session chair: Mark Giesbrecht 14:00-14:30 Solving curve completion problems with discrete invariants Jun Zhao and Elizabeth Mansfield 14:30-15:00 Point searching in real singular complete intersection varieties – algorithms of intrinsic complexity Bernd Bank, Marc Giusti and Joos Heintz 15:00-15:30 On solving parametric polynomial systems Marc Moreno Maza, Bican Xia and Rong Xiao 15:30-16:00 Closing 18:00-20:00 Dinner