I am currently doing my Bachelor’s thesis at the Formal Verification Group under the supervision of Dr. Mingshuai Chen. Together with colleagues from ISCAS, we work on automated inductive and/or deductive approaches to synthesizing (possibly infinite-state) loopy probabilistic programs encoding randomized algorithms.