School Colloquium——On the Very Nature of Symbolic Execution
报告人：Prof. Marcello Bonsangue (Leiden University, Holland)
地点：Room 1114, Sciences Building No. 1
Abstract: In this talk I will present a formal definition of symbolic execution in terms of a symbolic transition system show that it is correctness with respect to an operational semantics which models the execution
on concrete values. The approach is modular, starting from a basic programming language with a statically fixed number of programming variable and extending it to a programming language with recursive
procedures, arrays, and dynamically allocated variables. (joint work with Frank de Boer, CWI, Amsterdam)
Short Bio: Marcello Bonsangue is an associate professor in computer science at Leiden university. He received his master degree in Computer Science cum laude from from Milano University in Italy, and his Phd degree from the Free University of Amsterdam, in the Netherlands. Before becoming associate professor in Leiden, he was a research fellow of the Royal Netherlands Academy of Arts and Sciences. He is currently the director of education of LIACS, the institute of computer science of Leiden University. His research interests lie in the theoretical foundations of computer science, especially on the use of formal methods to better understand, model, and trust today's complex software systems.