George C. Necula

Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen: NDetermin: inferring nondeterministic sequential specifications for parallelism correctness. PPOPP 2012: 329-330

Derrick Coetzee, Anand Bhaskar, George C. Necula: A model and framework for reliable build systems. CoRR abs/1203.2704 (2012)

Jacob Burnim, George C. Necula, Koushik Sen: Specifying and checking semantic atomicity for multithreaded programs. ASPLOS 2011: 79-90

Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen: NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness. PLDI 2011: 401-414

George C. Necula: Proof-Carrying Code. Encyclopedia of Cryptography and Security (2nd Ed.) 2011: 984-986

Westley Weimer, George C. Necula: Exceptional situations and program reliability. ACM Trans. Program. Lang. Syst. 30(2) (2008)

George C. Necula, Philip Wadler (Eds.): 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, isbn 978-1-59593-689-9

Jens Knoop, George C. Necula, Wolf Zimmermann: Preface. Electr. Notes Theor. Comput. Sci. 176(3): 1-2 (2007)

Sumit Gulwani, George C. Necula: A polynomial-time algorithm for global value numbering. Sci. Comput. Program. 64(1): 97-114 (2007)

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)

Jeremy Condit, Matthew Harren, Zachary R. Anderson, David Gay, George C. Necula: Dependent Types for Low-Level Programming. ESOP 2007: 520-535

Zachary R. Anderson, Eric A. Brewer, Jeremy Condit, Robert Ennals, David Gay, Matthew Harren, George C. Necula, Feng Zhou: Beyond Bug-Finding: Sound Program Analysis for Linux. HotOS 2007

Bor-Yuh Evan Chang, Xavier Rival, George C. Necula: Shape Analysis with Structural Invariant Checkers. SAS 2007: 384-401

François Pottier, George C. Necula (Eds.): Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007. ACM 2007, isbn 1-59593-393-X

George C. Necula: Using Dependent Types to Port Type Systems to Low-Level Languages. CC 2006: 1

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

Úlfar Erlingsson, Martín Abadi, Michael Vrable, Mihai Budiu, George C. Necula: XFI: Software Guards for System Address Spaces. OSDI 2006: 75-88

Bor-Yuh Evan Chang, Matthew Harren, George C. Necula: Analysis of Low-Level Code Using Cooperating Decompilers. SAS 2006: 318-335

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula: A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. VMCAI 2006: 174-189

Jens Knoop, George C. Necula, Wolf Zimmermann: Preface. Electr. Notes Theor. Comput. Sci. 132(1): 1-3 (2005)

Jens Knoop, George C. Necula, Wolf Zimmermann: Preface. Electr. Notes Theor. Comput. Sci. 141(2): 1-3 (2005)

Sumit Gulwani, George C. Necula: A randomized satisfiability procedure for arithmetic and uninterpreted function symbols. Inf. Comput. 199(1-2): 107-131 (2005)

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)

George C. Necula, Sumit Gulwani: Randomized Algorithms for Program Analysis and Verification. CAV 2005: 1

Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula: JVer: A Java Verifier. CAV 2005: 144-147

Scott McPeak, George C. Necula: Data Structure Specifications via Local Equality Axioms. CAV 2005: 476-490

Jeremy Condit, George C. Necula: Data Slicing: Separating the Heap into Independent Regions. CC 2005: 172-187

Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula: Enforcing Resource Bounds via Static Verification of Dynamic Checks. ESOP 2005: 311-325

Sumit Gulwani, George C. Necula: Precise interprocedural analysis using random interpretation. POPL 2005: 324-337

Matthew Harren, George C. Necula: Using Dependent Types to Certify the Safety of Assembly Code. SAS 2005: 155-170

Westley Weimer, George C. Necula: Mining Temporal Specifications for Error Detection. TACAS 2005: 461-476

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck: The open verifier framework for foundational verifiers. TLDI 2005: 1-12

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck: Type-based verification of assembly language for compiler debugging. TLDI 2005: 91-102

Scott McPeak, George C. Necula: Elkhound: A Fast, Practical GLR Parser Generator. CC 2004: 73-88

Nathan Whitehead, Martín Abadi, George C. Necula: By Reason and Authority: A System for Authorization of Proof-Carrying Code. CSFW 2004: 236-250

Sumit Gulwani, Ashish Tiwari, George C. Necula: Join Algorithms for the Theory of Uninterpreted Functions. FSTTCS 2004: 311-323

Westley Weimer, George C. Necula: Finding and preventing run-time error handling mistakes. OOPSLA 2004: 419-431

Sumit Gulwani, George C. Necula: Global value numbering using random interpretation. POPL 2004: 342-352

Sumit Gulwani, George C. Necula: A Polynomial-Time Algorithm for Global Value Numbering. SAS 2004: 212-227

Sumit Gulwani, George C. Necula: Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions. SAS 2004: 328-343

Sumit Gulwani, George C. Necula: A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. CADE 2003: 167-181

Matthew Harren, George C. Necula: Lightweight Wrappers for Interfacing with Binary Code in CCured. ISSS 2003: 209-225

George C. Necula, Robert R. Schneck: A Sound Framework for Untrusted Verification-Condition Generators. LICS 2003: 248-260

Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer: CCured in the real world. PLDI 2003: 232-244

Sumit Gulwani, George C. Necula: Discovering affine equalities using random interpretation. POPL 2003: 74-84

J. Robert von Behren, Jeremy Condit, Feng Zhou, George C. Necula, Eric A. Brewer: Capriccio: scalable threads for internet services. SOSP 2003: 268-281

Robert R. Schneck, George C. Necula: A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. CADE 2002: 47-62

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

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

George C. Necula, Robert R. Schneck: Proof-Carrying Code with Untrusted Proof Rules. ISSS 2002: 283-298

George C. Necula, Scott McPeak, Westley Weimer: CCured: type-safe retrofitting of legacy code. POPL 2002: 128-139

George C. Necula: A Scalable Architecture for Proof-Carrying Code. FLOPS 2001: 21-39

George C. Necula, Shree Prakash Rahul: Oracle-based checking of untrusted software. POPL 2001: 142-154

George C. Necula, Shree Prakash Rahul: A logic-based approach to software system safety and security. ACM SIGSOFT Software Engineering Notes 25(1): 67-68 (2000)

George C. Necula, Peter Lee: Proof Generation in the Touchstone Theorem Prover. CADE 2000: 25-44

Christopher Colby, Peter Lee, George C. Necula: A Proof-Carrying Code Architecture for Java. CAV 2000: 557-560

George C. Necula: Translation validation for an optimizing compiler. PLDI 2000: 83-94

Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, Kenneth Cline: A certifying compiler for Java. PLDI 2000: 95-107

George C. Necula: Proof-carrying code: design, implementation and applications (abstract). PPDP 2000: 175-177

George C. Necula: Enforcing Security and Safety with Proof-Carrying Code. Electr. Notes Theor. Comput. Sci. 20: 117-131 (1999)

George C. Necula, Peter Lee: Efficient Representation and Validation of Proofs. LICS 1998: 93-104

George C. Necula, Peter Lee: Safe, Untrusted Agents Using Proof-Carrying Code. Mobile Agents and Security 1998: 61-91

George C. Necula, Peter Lee: The Design and Implementation of a Certifying Compiler. PLDI 1998: 333-344

George C. Necula, Peter Lee: The design and implementation of a certifying compiler (with retrospective). Best of PLDI 1998: 612-625

George C. Necula: Proof-Carrying Code. POPL 1997: 106-119

George C. Necula, Peter Lee: Research on Proof-Carrying Code for Untrusted-Code Security. IEEE Symposium on Security and Privacy 1997: 204

George C. Necula, Peter Lee: Safe Kernel Extensions Without Run-Time Checking. OSDI 1996: 229-243