题目:基于自动机理论的字符串处理程序的路径可行性判定算法 (Automata-Theoretical Decision Procedures For Path Feasibility of String Manipulating Programs)

摘要:The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, with such applications as symbolic execution of programs manipulating strings and automated detection of cross-site scripting (XSS) vulnerabilities in web applications. A (symbolic) path is given as a finite sequence of assignments and assertions (i.e. without loops), and checking its feasibility amounts to determining the existence of inputs that yield a successful execution. Modern programming languages (e.g.JavaScript, PHP, and Python) support many string operations, e.g. concatenation, replaceAll functions, string reverse, regular expressions (in a non-standard sense e.g. greedy/lazy Kleene star), string length, substring, indexof. Moreover, strings are also often implicitly modified during a computation in some intricate fashion, e.g. the user inputs in Web sites are usually preprocessed by HTML sanitizers, which can be naturally modeled as finite-state transducers.

In this talk, I will present our recent work on automata-theoretical decision procedures for path feasibility of string manipulating programs. Our decision procedures deal with all the aforementioned complex and diverse string operations in a conceptually simple way, thus unifying and extending the existing decision procedures for string constraints. Moreover, we provide an efficient implementation of our decision procedures in a new string solver OSTRICH. We demonstrate the efficacy of OSTRICH against the state-of-the-art competitive solvers, e.g. CVC4 and Z3, by extensive experiments.

This talk is based on our POPL 2018, POPL 2019, and ATVA 2020 publications.
个人简介:Zhilin Wu is a research professor in State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. He obtained his Phd. Degree from the same venue in 2007. His main research interests are program verification, automata theory, and computational logic. His research work appeared in international theoretical flagship conferences e.g. LICS, POPL, and CAV. He is the recipient of the 2020 CCF-IEEE CS Young Scientists Award.

题目:零知识证明:从密码学到金融科技 (Zero Knowledge Proofs: From Crypto to Fintech)


个人简介:邓燚,中国科学院信息工程研究所研究员。2008年获中国科学院软件所信息安全国家重点实验室博士学位。曾先后在英国伦敦大学学院和新加坡南洋理工大学从事博士后研究工作。主要从事密码学研究,特别是有关零知识证明和密码协议的通信与计算复杂性的问题。曾在一些密码学和计算机科学领域旗舰会议-- FOCS Eurocrypt, AsiacryptPKC上发表多篇论文。2011年获中国密码学会首届优秀青年奖,2014年获中国密码学会首届创新奖一等奖,2019年获中国电子学会自然科学奖一等奖。

题目:受限聚类问题的算法设计与分析 (New Algorithms for Constrained Clustering Problems)

摘要:Designing approximation algorithms for the clustering problem remains an active area of research. However, these algorithms can significantly deteriorate their performance in real-world applications. The major reason is that real-world applications often involve additional constraints (such as capacities and lower bounds of facilities) on the input data. In this talk, we first introduce several polynomial-time algorithms with improved approximation ratios for constrained clustering problems such as prize-collecting red-blue median, priority k-median, and lower-bounded k-median. Secondly, we introduce a unified framework for designing FPT(k)-time approximation algorithms in the presence of additional constraints. This framework yields algorithms with improved approximation ratios for the problems of capacitated clustering, lower-bounded clustering, fault-tolerant clustering, clustering with service installation costs, and priority clustering.
个人简介:冯启龙,中南大学计算机学院教授,博士生导师。20089月至20104月,公派留学美国Texas A&M University。一直从事于计算机算法优化、机器学习算法优化等方面的研究。近年来,主持国家自然科学基金面上项目2项、国家自然科学基金青年基金项目1项。担任FCS编委、国际会议TAMC 2020大会主席。