Martin Blicha is a Ph.D. student at the University of Lugano, Switzerland, and at the Charles University, Prague, Czech Republic, under the supervision of Professor Natasha Sharygina and Dr. Jan Kofroň. Martin received his B.Sc. and M.Sc. degrees from Charles University, Prague. His main research interest lies in the area of Craig interpolation, SMT and CHC solving with application to software verification, but he is also interested in broad application of logic in various other domains. He has been a co-developer of the SMT solver OpenSMT for almost 4 years and he also did an internship at the Ethereum Foundation, where he was working on SMTChecker, the formal verification module for the compiler of Solidity, the programming language for Ethereum smart contracts. Martin acted as a member of the artifact evaluation committee at CAV 2020 and as a subreviewer for conferences such as FMCAD, TACAS, LPAR, VMCAI and CAV.
Research Manuscript
Design Verification and Validation
In-Person Only