Invited Talks


The invited talks take place at 9am on each of the main conference days:

Titles and Abstracts

Erika Ábrahám,
RWTH Aachen University, Germany

Building Bridges between Symbolic Computation and Satisfiability Checking


Abstract: The satisfiability problem is the problem of deciding whether a logical formula is satisfiable. For first-order arithmetic theories, in the early 20th century some novel solutions in form of decision procedures were developed in the area of mathematical logic. With the advent of powerful computer architectures, a new research line started to develop practically feasible implementations of such decision procedures. Since then, symbolic computation has grown to an extremely successful scientific area, supporting all kinds of scientific computing by efficient computer algebra systems.

Independently, around 1960 a new technology called SAT solving started its career. Restricted to propositional logic, SAT solvers showed to be very efficient when employed by formal methods for verification, especially for checking digital circuits. It did not take long till the power of SAT solving for Boolean problems has been extended to cover also different theories. Nowadays, fast SAT-modulo-theories (SMT) solvers are available also for arithmetic problems.

Due to their different roots, symbolic computation and SMT solving tackle the satisfiability problem differently. We discuss differences and similarities in their approaches, highlight potentials of combining their strengths, and discuss the challenges that come with this task.

Éric Schost,
University of Western Ontario, Canada

Algorithms for finite fields arithmetic


Abstract: Finite fields appear in many branches of pure and applied mathematics, prominently so in areas such as number theory, cryptography and coding theory. As a result, building and computing in arbitrary finite fields is a fundamental task for any computer algebra system; for instance, the implementation available in Magma remains one of the most complete known to us.

Many questions remain open regarding the complexity of this kind of calculation, some of them very challenging. The most famous one is probably whether one can construct an arbitrary finite field in deterministic polynomial time.

In this talk, our objective is more modest. If we consider randomized algorithms, it is known that one can build and compute in arbitrary finite finite fields in polynomial time; using techniques based on FFT multiplication, a natural goal is then to design efficient algorithms, that would work in quasi-linear time. I will describe work in this direction by Shoup, Lenstra, Couveignes and Lercier, how ideas such as Kedlaya and Umans' modular composition algorithm can be brought into play, and recent results obtained with De Feo and Doliskani.

Lihong Zhi,
MMRC, Chinese Academy of Sciences, China

Optimization Problems over Noncompact Semialgebraic Sets


Abstract: In this talk, we will introduce some recent progress in dealing with optimization problems over noncompact semialgebraic sets. When one does not know a priori if the polynomial attains a minimum, one has to take into account asymptotic phenomena. We introduce the conditions of pointedness and closedness at infinity of a noncompact semialgebraic set, and show that under these conditions our modified hierarchies of nested theta bodies and Lasserre”Ēs relaxations converge to the closure of the convex hull of the semialgebraic set. We consider the problem of optimizing a parametric linear function over a noncompact real algebraic variety and show that when the real variety is irreducible, smooth and the recession cone of the closure of its convex hull is pointed, then its dual variety is an irreducible hypersurface and the defining polynomial represents the optimal value function. Finally, we will show how to characterize the lifts of noncompact convex sets by the cone factorizations of properly defined slack operators.