| 2018 | ICSE | DetReduce: minimizing Android GUI test suites for regression testing. | Wontae Choi, Koushik Sen, George C. Necula, Wenyu Wang |
| 2016 | NSDI | Minimizing Faulty Executions of Distributed Systems. | Colin Scott, Aurojit Panda, Vjekoslav Brajkovic, George C. Necula, Arvind Krishnamurthy, Scott Shenker |
| 2015 | SAS | SJS: A Type System for JavaScript with Fixed Object Layout. | Wontae Choi, Satish Chandra, George C. Necula, Koushik Sen |
| 2014 | OOPSLA | EventBreak: analyzing the responsiveness of user interfaces through performance-guided test generation. | Michael Pradel, Parker Schuh, George C. Necula, Koushik Sen |
| 2013 | OOPSLA | Guided GUI testing of android apps with minimal restart and approximate learning. | Wontae Choi, George C. Necula, Koushik Sen |
| 2013 | PLDI | CONCURRIT: a domain specific language for reproducing concurrency bugs. | Tayfun Elmas, Jacob Burnim, George C. Necula, Koushik Sen |
| 2012 | PPoPP | NDetermin: inferring nondeterministic sequential specifications for parallelism correctness. | Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen |
| 2011 | ASPLOS | Specifying and checking semantic atomicity for multithreaded programs. | Jacob Burnim, George C. Necula, Koushik Sen |
| 2011 | PLDI | NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness. | Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen |
| 2007 | ESOP | Dependent Types for Low-Level Programming. | Jeremy Condit, Matthew Harren, Zachary R. Anderson, David Gay, George C. Necula |
| 2007 | HotOS | Beyond Bug-Finding: Sound Program Analysis for Linux. | Zachary R. Anderson, Eric A. Brewer, Jeremy Condit, Robert Ennals, David Gay, Matthew Harren, George C. Necula, Feng Zhou |
| 2007 | SAS | Shape Analysis with Structural Invariant Checkers. | Bor-Yuh Evan Chang, Xavier Rival, George C. Necula |
| 2006 | CC | Using Dependent Types to Port Type Systems to Low-Level Languages. | George C. Necula |
| 2006 | OSDI | XFI: Software Guards for System Address Spaces. | lfar Erlingsson, Martn Abadi, Michael Vrable, Mihai Budiu, George C. Necula |
| 2006 | OSDI | SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques. | Feng Zhou, Jeremy Condit, Zachary R. Anderson, Ilya Bagrak, Robert Ennals, Matthew Harren, George C. Necula, Eric A. Brewer |
| 2006 | SAS | Analysis of Low-Level Code Using Cooperating Decompilers. | Bor-Yuh Evan Chang, Matthew Harren, George C. Necula |
| 2006 | VMCAI | A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula |
| 2005 | CAV | JVer: A Java Verifier. | Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula |
| 2005 | CAV | Data Structure Specifications via Local Equality Axioms. | Scott McPeak, George C. Necula |
| 2005 | CAV | Randomized Algorithms for Program Analysis and Verification. | George C. Necula, Sumit Gulwani |
| 2005 | CC | Data Slicing: Separating the Heap into Independent Regions. | Jeremy Condit, George C. Necula |
| 2005 | ESOP | Enforcing Resource Bounds via Static Verification of Dynamic Checks. | Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula |
| 2005 | POPL | Precise interprocedural analysis using random interpretation. | Sumit Gulwani, George C. Necula |
| 2005 | SAS | Using Dependent Types to Certify the Safety of Assembly Code. | Matthew Harren, George C. Necula |
| 2005 | TACAS | Mining Temporal Specifications for Error Detection. | Westley Weimer, George C. Necula |
| 2004 | CC | Elkhound: A Fast, Practical GLR Parser Generator. | Scott McPeak, George C. Necula |
| 2004 | OOPSLA | Finding and preventing run-time error handling mistakes. | Westley Weimer, George C. Necula |
| 2004 | POPL | Global value numbering using random interpretation. | Sumit Gulwani, George C. Necula |
| 2004 | SAS | A Polynomial-Time Algorithm for Global Value Numbering. | Sumit Gulwani, George C. Necula |
| 2004 | SAS | Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions. | Sumit Gulwani, George C. Necula |
| 2003 | CADE | A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. | Sumit Gulwani, George C. Necula |
| 2003 | LICS | A Sound Framework for Untrusted Verification-Condition Generators. | George C. Necula, Robert R. Schneck |
| 2003 | PLDI | CCured in the real world. | Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer |
| 2003 | POPL | Discovering affine equalities using random interpretation. | Sumit Gulwani, George C. Necula |
| 2003 | SOSP | Capriccio: scalable threads for internet services. | J. Robert von Behren, Jeremy Condit, Feng Zhou, George C. Necula, Eric A. Brewer |
| 2002 | CADE | A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. | Robert R. Schneck, George C. Necula |
| 2002 | CAV | Temporal-Safety Proofs for Systems Code. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grgoire Sutre, Westley Weimer |
| 2002 | CC | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. | George C. Necula, Scott McPeak, Shree Prakash Rahul, Westley Weimer |
| 2002 | POPL | CCured: type-safe retrofitting of legacy code. | George C. Necula, Scott McPeak, Westley Weimer |
| 2001 | FLOPS | A Scalable Architecture for Proof-Carrying Code. | George C. Necula |
| 2001 | POPL | Oracle-based checking of untrusted software. | George C. Necula, Shree Prakash Rahul |
| 2000 | CADE | Proof Generation in the Touchstone Theorem Prover. | George C. Necula, Peter Lee |
| 2000 | CAV | A Proof-Carrying Code Architecture for Java. | Christopher Colby, Peter Lee, George C. Necula |
| 2000 | PLDI | A certifying compiler for Java. | Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, Kenneth Cline |
| 2000 | PLDI | Translation validation for an optimizing compiler. | George C. Necula |
| 2000 | PPDP | Proof-carrying code: design, implementation and applications (abstract). | George C. Necula |
| 1998 | LICS | Efficient Representation and Validation of Proofs. | George C. Necula, Peter Lee |
| 1998 | PLDI | The Design and Implementation of a Certifying Compiler. | George C. Necula, Peter Lee |
| 1998 | PLDI | The design and implementation of a certifying compiler (with retrospective) | George C. Necula, Peter Lee |
| 1997 | POPL | Proof-Carrying Code. | George C. Necula |
| 1997 | SP | Research on Proof-Carrying Code for Untrusted-Code Security. | George C. Necula, Peter Lee |
| 1996 | OSDI | Safe Kernel Extensions Without Run-Time Checking. | George C. Necula, Peter Lee |