Viktor Vafeiadis

Getting more out of a stateless model checker

Stateless model checking is a widely-applicable automated approach for verifying the assertion safety of bounded concurrent programs. The talk will show how can we use a model checker to prove linearizability, and how careful model of common library operations can boost the model checker’s performance.
 

back to overview
 

Biography

Viktor Vafeiadis is conducting research on the semantics and verification of concurrent and persistent programs. He got his PhD from the University of Cambridge (2008), worked as a postdoc at Microsoft Research and at the University of Cambridge, and is currently a tenured researcher at the Max Planck Institute for Software Systems (MPI-SWS). He has co-authored over 90 peer-reviewed research papers and has been awarded the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award (2008), the ACM SIGPLAN Robin Milner Young Researcher Award (2022), an ERC Consolidator Grant (2020), and multiple distinguished paper awards.
Footer

Imprint / Privacy