演讲1：概率程序的形式验证：终止，成本分析和灵敏度

Talk 1: Formal Verification of Probabilistic Programs: Termination, Cost

Analysis and Sensitivity

Speaker: Hongfei Fu (Shanghai Jiao Tong University)

Abstract: Formal verification is the study to ensure correctness of systems through

rigorous mathematical approaches. Probabilistic programs are classical programs

extended with random number generators that capture a large class of application

scenarios with probability, such as artificial intelligence, random walks, randomized

algorithms, stochastic systems, etc. Formal verification of probabilistic programs

aims at developing methodologies that can prove correctness of fundamental

probabilistic properties such as termination with probability one, expected resource

consumption, and expected sensitivity against slight perturbation of inputs, etc. In

the talk, I will introduce our theoretical results on verifying termination, cost and

sensitivity of probabilistic programs.

Bio: Dr. Hongfei Fu obtained his PhD at RWTH Aachen, supervised by Prof. JoostPieter Katoen. He is currently an assistant professor at John Hopcroft Center for

Computer Science, Shanghai Jiao Tong University. His main research interest lies in

developing automated approaches for solving model-checking and programverification problems in the broad sense.

Talk 2: Input Selection In Interactive Program Synthesis

Speaker: Ruyi Ji (Peking University)

Abstract: Interactive program synthesis has been proposed to solve the ambiguity in

specifications. A typical form of interaction is input-output queries, where the

system queries with an input, and the developer provides the corresponding output.

However, existing systems usually randomly select the input, which may lead to

many more questions being asked than necessary. We address the input selection

problem in interactive program synthesis, and Our goal is to minimize the number of

queries to the user.

Bio: Ruyi Ji is a fourth-year undergraduate student in Peking Univerity, and he'll

continue studying at Peking University for a Ph.D. degree next year. He used to be a

contestant in competitive programming and has won one gold medal and one silver

medal in ICPC World Finals.