| 2008 |
|---|
| 60 | | George C. Necula,
Philip Wadler:
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008
ACM 2008 |
| 59 | EE | Westley Weimer,
George C. Necula:
Exceptional situations and program reliability.
ACM Trans. Program. Lang. Syst. 30(2): (2008) |
| 2007 |
|---|
| 58 | | François Pottier,
George C. Necula:
Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007
ACM 2007 |
| 57 | EE | Jeremy Condit,
Matthew Harren,
Zachary R. Anderson,
David Gay,
George C. Necula:
Dependent Types for Low-Level Programming.
ESOP 2007: 520-535 |
| 56 | EE | Bor-Yuh Evan Chang,
Xavier Rival,
George C. Necula:
Shape Analysis with Structural Invariant Checkers.
SAS 2007: 384-401 |
| 55 | EE | Ajay Chander,
David Espinosa,
Nayeem Islam,
Peter Lee,
George C. Necula:
Enforcing resource bounds via static verification of dynamic checks.
ACM Trans. Program. Lang. Syst. 29(5): (2007) |
| 54 | EE | Jens Knoop,
George C. Necula,
Wolf Zimmermann:
Preface.
Electr. Notes Theor. Comput. Sci. 176(3): 1-2 (2007) |
| 53 | EE | Sumit Gulwani,
George C. Necula:
A polynomial-time algorithm for global value numbering.
Sci. Comput. Program. 64(1): 97-114 (2007) |
| 2006 |
|---|
| 52 | EE | George C. Necula:
Using Dependent Types to Port Type Systems to Low-Level Languages.
CC 2006: 1 |
| 51 | EE | Feng Zhou,
Jeremy Condit,
Zachary R. Anderson,
Ilya Bagrak,
Robert Ennals,
Matthew Harren,
George C. Necula,
Eric A. Brewer:
SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques.
OSDI 2006: 45-60 |
| 50 | EE | Úlfar Erlingsson,
Martín Abadi,
Michael Vrable,
Mihai Budiu,
George C. Necula:
XFI: Software Guards for System Address Spaces.
OSDI 2006: 75-88 |
| 49 | EE | Bor-Yuh Evan Chang,
Matthew Harren,
George C. Necula:
Analysis of Low-Level Code Using Cooperating Decompilers.
SAS 2006: 318-335 |
| 48 | EE | Bor-Yuh Evan Chang,
Adam J. Chlipala,
George C. Necula:
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.
VMCAI 2006: 174-189 |
| 2005 |
|---|
| 47 | EE | George C. Necula,
Sumit Gulwani:
Randomized Algorithms for Program Analysis and Verification.
CAV 2005: 1 |
| 46 | EE | Ajay Chander,
David Espinosa,
Nayeem Islam,
Peter Lee,
George C. Necula:
JVer: A Java Verifier.
CAV 2005: 144-147 |
| 45 | EE | Scott McPeak,
George C. Necula:
Data Structure Specifications via Local Equality Axioms.
CAV 2005: 476-490 |
| 44 | EE | Jeremy Condit,
George C. Necula:
Data Slicing: Separating the Heap into Independent Regions.
CC 2005: 172-187 |
| 43 | EE | Ajay Chander,
David Espinosa,
Nayeem Islam,
Peter Lee,
George C. Necula:
Enforcing Resource Bounds via Static Verification of Dynamic Checks.
ESOP 2005: 311-325 |
| 42 | EE | Sumit Gulwani,
George C. Necula:
Precise interprocedural analysis using random interpretation.
POPL 2005: 324-337 |
| 41 | EE | Matthew Harren,
George C. Necula:
Using Dependent Types to Certify the Safety of Assembly Code.
SAS 2005: 155-170 |
| 40 | EE | Westley Weimer,
George C. Necula:
Mining Temporal Specifications for Error Detection.
TACAS 2005: 461-476 |
| 39 | EE | Bor-Yuh Evan Chang,
Adam J. Chlipala,
George C. Necula,
Robert R. Schneck:
The open verifier framework for foundational verifiers.
TLDI 2005: 1-12 |
| 38 | EE | Bor-Yuh Evan Chang,
Adam J. Chlipala,
George C. Necula,
Robert R. Schneck:
Type-based verification of assembly language for compiler debugging.
TLDI 2005: 91-102 |
| 37 | EE | George C. Necula,
Jeremy Condit,
Matthew Harren,
Scott McPeak,
Westley Weimer:
CCured: type-safe retrofitting of legacy software.
ACM Trans. Program. Lang. Syst. 27(3): 477-526 (2005) |
| 36 | EE | Jens Knoop,
George C. Necula,
Wolf Zimmermann:
Preface.
Electr. Notes Theor. Comput. Sci. 132(1): 1-3 (2005) |
| 35 | EE | Jens Knoop,
George C. Necula,
Wolf Zimmermann:
Preface.
Electr. Notes Theor. Comput. Sci. 141(2): 1-3 (2005) |
| 34 | EE | Sumit Gulwani,
George C. Necula:
A randomized satisfiability procedure for arithmetic and uninterpreted function symbols.
Inf. Comput. 199(1-2): 107-131 (2005) |
| 2004 |
|---|
| 33 | EE | Scott McPeak,
George C. Necula:
Elkhound: A Fast, Practical GLR Parser Generator.
CC 2004: 73-88 |
| 32 | EE | Nathan Whitehead,
Martín Abadi,
George C. Necula:
By Reason and Authority: A System for Authorization of Proof-Carrying Code.
CSFW 2004: 236-250 |
| 31 | EE | Sumit Gulwani,
Ashish Tiwari,
George C. Necula:
Join Algorithms for the Theory of Uninterpreted Functions.
FSTTCS 2004: 311-323 |
| 30 | EE | Westley Weimer,
George C. Necula:
Finding and preventing run-time error handling mistakes.
OOPSLA 2004: 419-431 |
| 29 | EE | Sumit Gulwani,
George C. Necula:
Global value numbering using random interpretation.
POPL 2004: 342-352 |
| 28 | EE | Sumit Gulwani,
George C. Necula:
A Polynomial-Time Algorithm for Global Value Numbering.
SAS 2004: 212-227 |
| 27 | EE | Sumit Gulwani,
George C. Necula:
Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions.
SAS 2004: 328-343 |
| 2003 |
|---|
| 26 | EE | Sumit Gulwani,
George C. Necula:
A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols.
CADE 2003: 167-181 |
| 25 | EE | Matthew Harren,
George C. Necula:
Lightweight Wrappers for Interfacing with Binary Code in CCured.
ISSS 2003: 209-225 |
| 24 | EE | George C. Necula,
Robert R. Schneck:
A Sound Framework for Untrusted Verification-Condition Generators.
LICS 2003: 248-260 |
| 23 | EE | Jeremy Condit,
Matthew Harren,
Scott McPeak,
George C. Necula,
Westley Weimer:
CCured in the real world.
PLDI 2003: 232-244 |
| 22 | EE | Sumit Gulwani,
George C. Necula:
Discovering affine equalities using random interpretation.
POPL 2003: 74-84 |
| 21 | EE | J. Robert von Behren,
Jeremy Condit,
Feng Zhou,
George C. Necula,
Eric A. Brewer:
Capriccio: scalable threads for internet services.
SOSP 2003: 268-281 |
| 2002 |
|---|
| 20 | EE | Robert R. Schneck,
George C. Necula:
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.
CADE 2002: 47-62 |
| 19 | EE | Thomas A. Henzinger,
Ranjit Jhala,
Rupak Majumdar,
George C. Necula,
Grégoire Sutre,
Westley Weimer:
Temporal-Safety Proofs for Systems Code.
CAV 2002: 526-538 |
| 18 | EE | George C. Necula,
Scott McPeak,
Shree Prakash Rahul,
Westley Weimer:
CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs.
CC 2002: 213-228 |
| 17 | EE | George C. Necula,
Robert R. Schneck:
Proof-Carrying Code with Untrusted Proof Rules.
ISSS 2002: 283-298 |
| 16 | EE | George C. Necula,
Scott McPeak,
Westley Weimer:
CCured: type-safe retrofitting of legacy code.
POPL 2002: 128-139 |
| 2001 |
|---|
| 15 | EE | George C. Necula:
A Scalable Architecture for Proof-Carrying Code.
FLOPS 2001: 21-39 |
| 14 | EE | George C. Necula,
Shree Prakash Rahul:
Oracle-based checking of untrusted software.
POPL 2001: 142-154 |
| 2000 |
|---|
| 13 | | George C. Necula,
Peter Lee:
Proof Generation in the Touchstone Theorem Prover.
CADE 2000: 25-44 |
| 12 | | Christopher Colby,
Peter Lee,
George C. Necula:
A Proof-Carrying Code Architecture for Java.
CAV 2000: 557-560 |
| 11 | EE | George C. Necula:
Translation validation for an optimizing compiler.
PLDI 2000: 83-94 |
| 10 | EE | Christopher Colby,
Peter Lee,
George C. Necula,
Fred Blau,
Mark Plesko,
Kenneth Cline:
A certifying compiler for Java.
PLDI 2000: 95-107 |
| 9 | EE | George C. Necula:
Proof-carrying code: design, implementation and applications (abstract).
PPDP 2000: 175-177 |
| 1999 |
|---|
| 8 | EE | George C. Necula:
Enforcing Security and Safety with Proof-Carrying Code.
Electr. Notes Theor. Comput. Sci. 20: (1999) |
| 1998 |
|---|
| 7 | EE | George C. Necula,
Peter Lee:
The design and implementation of a certifying compiler (with retrospective)
Best of PLDI 1998: 612-625 |
| 6 | | George C. Necula,
Peter Lee:
Efficient Representation and Validation of Proofs.
LICS 1998: 93-104 |
| 5 | EE | George C. Necula,
Peter Lee:
Safe, Untrusted Agents Using Proof-Carrying Code.
Mobile Agents and Security 1998: 61-91 |
| 4 | | George C. Necula,
Peter Lee:
The Design and Implementation of a Certifying Compiler.
PLDI 1998: 333-344 |
| 1997 |
|---|
| 3 | EE | George C. Necula,
Peter Lee:
Research on Proof-Carrying Code for Untrusted-Code Security.
IEEE Symposium on Security and Privacy 1997: 204 |
| 2 | EE | George C. Necula:
Proof-Carrying Code.
POPL 1997: 106-119 |
| 1996 |
|---|
| 1 | | George C. Necula,
Peter Lee:
Safe Kernel Extensions Without Run-Time Checking.
OSDI 1996: 229-243 |
