Abstract
Our work on narrowing the gap between verification and systematic testing has two directions: (1) complementing verification with systematic testing, and (2) pushing systematic testing toward reaching verification. In the first direction, we explore how to effectively combine static analysis with systematic testing, so as to guide test generation toward properties that have not been previously checked by a static analyzer in a sound way. This combination significantly reduces the test effort while checking more unverified properties. In the second direction, we push systematic testing toward checking as many executions as possible of a real and complex image parser, so as to prove the absence of a certain class of errors. This verification attempt required no static analysis or source code annotations; our purely dynamic techniques targeted the verification of the parser implementation, including complicated assembly patterns that most static analyses cannot handle.
About the author
Maria Christakis is currently a lecturer (assistant professor) in the School of Computing at the University of Kent, England. She was previously a post-doctoral researcher at Microsoft Research Redmond, USA. She received her Ph.D. from the Department of Computer Science of ETH Zurich, Switzerland in the summer of 2015, and feels very fortunate to have been advised by Peter Müller. Maria was awarded with the ETH medal for an outstanding doctoral thesis. She completed her Bachelor's and Master's degrees at the Department of Electrical and Computer Engineering of the National Technical University of Athens, Greece. Maria's goal is to develop theoretical foundations and practical tools for building more reliable and usable software and increasing developer productivity. She is mostly interested in software engineering, programming languages, and formal methods. Maria particularly likes investigating topics in automatic test generation, software verification, program analysis, and empirical software engineering. Her tools and techniques explore novel ways in writing, specifying, verifying, testing, and debugging programs in order to make them more robust while at the same time improving the user experience.
School of Computing, University of Kent, Canterbury, United Kingdom of Great Britain and Northern Ireland
Acknowledgement
I am grateful to Peter Müller, Valentin Wüstholz, and Patrice Godefroid; this work would not have been possible without them. I would also like to thank my other collaborators, Patrick Emmisberger and Rustan Leino.
©2017 Walter de Gruyter Berlin/Boston
