[09-17] On Solving String Constraints

Title: On Solving String Constraints

Speaker: Yu-Fang Chen (陳郁方), Institute of Information Science, Academia Sinica, Taiwan

Time: 3:00pm, September 17th (Tuesday), 2019

Venue: Lecture room (334), SKLCS, Building 5, Software Park, Chinese Academy of Sciences

Abstract:
String data types are present in all conventional programming and scripting languages. In fact, it is almost impossible to reason about the correctness and security of such programs without having a decision procedure for string constraints.
A typical string constraint consists of word equations over string variables denoting strings of arbitrary lengths, together with constraints on (i) the length of strings, and (ii) the regular languages to which strings belong. Decidability of this general logic is still open. In this talk, we will discuss recent results on the decidability, decision procedures, and tools for the core string constraints solving.
Some features of standard string APIs in conventional programming languages are not covered by the core string constraints, we will also discuss this issue and show the state-of-the art in this aspect.
We will also talk about some on-going research directions on this topic.

Biography:
Yu-Fang Chen is a research fellow at the Institute of Information Science, Academia Sinica, Taiwan. He was an associate research fellow from 2014 to 2018 and assistant research fellow from 2009 to 2014 at the same institute. In 2009, he worked as a postdoc researcher at Uppsala University, Sweden.
He finished his Ph.D. study at the National Taiwan University in 2008 and wrote his doctoral thesis on the topic of the automation of compositional verification using automata learning algorithms. He has served in the program committees of a number of conferences and workshops, including ATVA, CONCUR, TACAS, APLAS, FASE and FM. His paper titled “When simulation meets antichains (for checking language inclusion of NFA’s)” won the best theory paper award at ETAPS 2010.
His research interest is the development of principled methods to ensure the quality of computer programs. He is particularly interested in software model checking and related techniques such as computational learning, automata theory, and satisfiability modulo theories (SMT). He is also interested in the applications of applying these techniques to ensure the correctness of real-world programs (e.g., high-speed crypto code and MapReduce programs).
More information can be found in http://bull.iis.sinica.edu.tw/yfc/