title: compiler validation via equivalence modulo inputs
lecture time: june 28, 2024, 10:00-11:30
venue: lecture hall, 4th floor, information building
tencent meeting id: 449-359-363
abstract
as an integral component of the foundation of our digital world, compilers are among the most important system software. thus their correctness is crucial to everyone’s daily life, directly or indirectly. in this talk, i present our continuous efforts on validating optimizing compilers with equivalence modulo inputs (emi), a general and effective methodology to generate equivalent programs from existing valid programs. specifically, i will present two different state-of-the-art techniques to realize emi, i.e., athena and hermes. these techniques have helped us find ~1600 new, real bugs in gcc and llvm, of which ~90% are already fixed by the compiler developers. my current group has also designed a syntax-guided language-agnostic compiler validation technique, which has uncovered over 300 new, real bugs in gcc, llvm, rust, solidity, scalar and other compilers.
lecturer
dr. chengnian sun is an associate professor in the cheriton school of computer science at the university of waterloo. his primary research interests encompass the domains of software engineering and programming languages. his focused efforts involve the conceptualization and implementation of techniques, tools, and methodologies that contribute to the enhancement of software reliability and developers’ productivity. he has published more than 50 peer-reviewed papers at top-tier conferences and journals, such as icse, asplos, pldi, fse and tosem. these works have generated over 3800 citations; one paper was awarded the acm distinguished paper award at ase 2012, one was nominated for best paper award at icsm 2013, and one was awarded the 10-year most influential paper award at saner 2022. before joining uwaterloo, he was a full-time software engineer at google, mountain view, working on java/android compiler tool-chains and machine learning libraries for google search. prior to google, he spent three wonderful years as a postdoctoral fellow at the university of california, davis, working on compiler validation techniques, which have detected 1600 bugs in gcc and llvm. he holds a ph.d. in computer science from the national university of singapore, and a bachelor degree from northeastern university, china.
