大会特邀报告:
- 李邦河(中国科学院数学与系统科学研究院)
中国科学院数学与系统科学研究院研究员、博士生导师,毕业于中国科学技术大学数学系。中国科学院数学与系统科学研究院研究员。并任研究院学位委员会委员、系统科学研究所学术委员会委员。1987-1988年度获第二届陈省身数学奖,1991年度被评为“国家级有突出贡献专家”,2001年当选为中国科学院院士。研究领域广泛,主要从事微分拓扑、低维拓扑的量子不变量、非标准分析和广义函数等领域的研究,在微分拓扑、低维拓扑、偏微分方程、广义函数、非标准分析以及代数几何和代数机械化等方面均取得了重要成果或重大突破。先后发表研究论文90余篇。他关于微分拓扑的工作曾获第二届陈省身数学奖(1989),他的许多研究结果被国内外学者所引用,在国际上产生了较大影响。
报告题目:希尔伯特第15问题和Ritt--吴方法 摘要:希尔伯特第15问题要求我们理解Schubert的书。在该书的第23节中,Schubert研究了带尖点的三次平面曲线的相关计数问题。他给出了一个描述从一个点引出的切线与这条曲线奇点之间关系的定理。这一定理由所谓的主干数得到,而关于主干数,Schubert说他是由经验所得。因此,本质上说,Schubert甚至都没有给出该定理证明的任何提示。我们利用Van der Waerden以及Weil代数几何框架中的generic point这个概念,并在计算机上实现Ritt--吴方法,证明了Schubert 的定理是完全正确的。
- 詹乃军(中国科学院软件研究所)
中科院软件所研究员,中国科学院大学教授,中国科学院特聘研究员,博士生导师。现任中国科学院软件研究所计算机科学国家重点实验室副主任,中国计算机学会形式化方法专业组秘书长,《Formal Aspects of Computing》、《Journal of Logical and Algebraic Methods in Programming》、《软件学报》、《计算机研究与发展》等编委,及多个国际学术组织任职。主要研究兴趣包括:实时、混成和嵌入式系统,程序验证,模态和时序逻辑,并发计算模型,程序形式语义等。
报告题目:Formal Analysis and Synthesis of Delay Dynamical and Hybrid Systems
摘要: Delay is everywhere in real-world embedded systems, but it lacks effective methods to formal analysis and design of embedded systems in the literature. In this talk, I will report our recent addresses on this issue, including an approach based on interval Taylor model plus interval arithmetic and stability analysis of discrete dynamical systems, an approach based on simulation, and an approach based on game theory.
- 唐小虎(西南交通大学)
西南交通大学特聘教授、博士生导师,国际电气与电子工程师协会(IEEE)信息论成都分会主席。2003年获全国百篇优秀博士学位论文奖,2004年入选教育部新世纪优秀人才支持计划,2006年获四川省有突出贡献专家称号,2007年获得德国洪堡基金,2011年当选四川省第九批学术与技术带头人,2013年获得国家杰出青年科学基金,2014年当选教育部“长江学者奖励计划”特聘教授。发表学术论文80余篇,其中信息与通信领域最顶级旗舰期刊IEEE Transactions on Information Theory (该杂志在电子工程领域947种国际学术期刊中排名:特征影响因子第1,论文影响子第6,影响因子第13)32 篇,被SCI收录论文60余篇,论文被SCI他引300余次,单篇最高被引用50余次。
报告题目:Placement-Delivery Array刻画及其应用
摘要:最近,Placement-Delivery Array(PDA)被提出用于描述编码缓存方案的放置和发送阶段。本报告中,我们首先介绍面向视频传输的编码缓存方案背景,然后给出PDA的概念及其组合特征, 接下来,我们发展并演示其在D2D通信、分布式计算系统等方面的应用。
青年学者邀请报告:
- 甘庭(武汉大学)
题目:Nonlinear Craig Interpolant Generation
摘要:Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, modelchecking,abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions(EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done. We proven that a polynomial interpolant of the form $h(x)>0$ exists for two mutually contradictory polynomial formulas $\varphi(x, y)$ and $\psi(x, z)$, with the form $\wedge_i f_i \ge 0$ , where $f_i$ are polynomials in $x, y$ or $x, z$, and the quadratic module generated by $f_i$ is Archimedean. Then it is shown that such interpolant can be computed efficiently through solving a semi-definite programming problem (SDP).- 贾晓红(中国科学院数学与系统科学研究院)
题目:How Algebra Is Used in Collision Detections
摘要:Collision detection is a key step of many advanced industry environments such as Virtual Reality, Robotics and CNC machining, where exact and efficient collision detection algorithms are highly appreciated. Collision Detection contains two main parts: the algorithm design for the dynamic layer and relative position decision for in the static stage. Traditional research is mainly based on the determination of the relative position or more precisely, morphology of the intersection curve, of two geometry objects, which only indicate the relationship, but neglect the asymmetry between two different objects. Configuration analysis reveals this asymmetry. In many practical environments, interchanging the two objects can lead to qualitative change of the environment, hence providing the concrete geometric or topological behavior of each object is more important. We shall re-explore the collision detection problem through configuration analysis by establishing classifications, enumeration and algebraic determination law of two static bounding volumes;. We also construct connection graph for all possible configurations and provide a symbolic algorithm of computing the configuration variations of two moving objects.- 李念(湖北大学)
题目:Recent Results on the Cross Correlation of $m$-Sequences
摘要:Pseudorandom sequences have significant applications in communication systems, coding theory and cryptography. Maximum length linear feedback shift register sequences (also called $m$-sequences) are popular in sequence design due to their excellent properties. In this talk, we will focus on the cross correlation between an $m$-sequence and its decimation sequence. We will introduce our newly found technique in solving equations over finite fields and its application in solving two open problems, proposed by Niho in 1972 and by Dobbertin, Helleseth and Martinsen in 1999 respectively by estabishing a surprising connection between a combinatorial counting problem and the Zetterberg code.- 牟晨琪(北京航空航天大学)
题目:Chordal Graphs in Triangular Decomposition in Top-Down Style
摘要:In this talk we present some underlying connections between symbolic computation and graph theory. Inspired by the two papers of Cifuentes and Parrilo in 2016 and 2017, we are interested in the chordal graph structures of polynomial sets appearing in triangular decomposition in top-down style. Viewing triangular decomposition in top-down style as multivariate generalization of Gaussian elimination, we show that the associated graph of one specific triangular set computed in any algorithm for triangular decomposition in top-down style is a subgraph of the chordal graph of the input polynomial set and that all the polynomial sets, including all the computed triangular sets, appearing in one specific algorithm for triangular decomposition in top-down style (Wang’s method) have associated graphs which are subgraphs of the chordal graph of the input polynomial set. Potential applications of chordal graphs in symbolic computation are also discussed.- 吴文渊(中国科学院重庆绿色智能技术研究院)
题目:Global Error Estimation for Linear ODE and its Optimal Solution
摘要:Solving Linear Ordinary Differential Equations (ODEs) plays an important role in many applications. There are various numerical methods and solvers to obtain approximate solutions typically represented by points. However, few work about estimation of global error can be found in the literatures. In this talk, we first use Hermite cubic spline interpolation at mesh points to represent the solution, then we define the backward error obtained by substituting the interpolation solution back to ODEs. Then the global error between the exact solution and an approximate solution can be bounded by using the backward error. Moreover, solving ODEs can be transformed to an optimization problem of backward error in certain solution space which can be solved by conjugate gradient method with taking advantages of sparsity of the corresponding matrix. The examples in the talk show that our estimation works well for linear ODEs' models and the refinement can find solutions with smaller global errors than traditional methods in Matlab without additional mesh points.- 徐岗(杭州电子科技大学)
题目:Hexahedral Mesh Subdivision and Simplification for Isogeometric Analysis
摘要: With the requirement of high-precision numerical simulation in intelligent manufacturing, the generation and processing of hexahedral mesh has become a hot issue recently in the field of geometric computing and isogeometric analysis. This talk will introduce our research progress on hexahedral mesh subdivision and simplification. In the first part, the limit point formula of Catmull-Clark volume subdivision will be introduced for all the cases of singular vertex. Based on the proposed formula, the applications on the interpolating volume subdivision and parametric volume approximation of subdivision solid are also given. In the second part, an improved simplification algorithm for singularity structure in hex-mesh is introduced. Starting from an initial hexahedral mesh, the proposed approach can obtain a hexahedral mesh with a much simpler singularity structure while maintaining approximation accuracy.- 叶科(中国科学院数学与系统科学研究院)
题目:Tensor Ranks with Applications to Complexity Theory
摘要:This talk consists of two parts. In the first part, I will review various notions of tensor ranks and present some of our new results on these ranks. In the second part, I will first discuss the connection between tensor ranks and the computational complexity theory. In particular, I will concentrate on the complexity of the matrix-vector/matrix-matrix multiplication. If time permits, I will exhibit some numerical algorithms for small size matrix multiplication obtained by this method.