Model Checking Procedures for Infinite State Systems. - Nikola Bogunovic; Edgar Pek (ECBS, 2006)

A flexible schema for generating explanations in lazy theory propagation. - Roberto Bruttomesso; Edgar Pek; Natasha Sharygina (MEMOCODE, 2010)

The OpenSMT Solver. - Roberto Bruttomesso; Edgar Pek; Natasha Sharygina; Aliaksei Tsitovich (TACAS, 2010)

Verifying security invariants in ExpressOS. - Haohui Mai; Edgar Pek; Hui Xue 007; Samuel Talmadge King; Parthasarathy Madhusudan (ASPLOS, 2013)

Explicit and symbolic techniques for fast and scalable points-to analysis. - Edgar Pek; P. Madhusudan (SOAP@PLDI, 2014)

Natural proofs for data structure manipulation in C using separation logic. - Edgar Pek; Xiaokang Qiu; P. Madhusudan (PLDI, 2014)

Automated deductive verification of systems software - Edgar Pek (2015)

Runtime Verification at Work: A Tutorial. - Philip Daian; Dwight Guth; Chris Hathhorn; Yilong Li; Edgar Pek; Manasvi Saxena; Traian-Florin Serbanuta; Grigore Rosu (RV, 2016)

Efficient Incrementalized Runtime Checking of Linear Measures on Lists. - Alex Gyori; Pranav Garg 001; Edgar Pek; P. Madhusudan (ICST, 2017)

Inferring Formal Properties of Production Key-Value Stores. - Edgar Pek; Pranav Garg 001; Muntasir Raihan Rahman; Karl Palmskog; Indranil Gupta; P. Madhusudan (CoRR, 2017)