George C. Necula - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

Specifying and checking semantic atomicity for multithreaded programsJacob Burnim, George C. Necula, Koushik Sen. asplos 2011: 79-90 [doi]

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

2008

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008George C. Necula, Philip Wadler, editors, ACM, 2008.

Exceptional situations and program reliabilityWestley Weimer, George C. Necula. TOPLAS, 30(2), 2008. [doi]

2007

Beyond Bug-Finding: Sound Program Analysis for LinuxZachary R. Anderson, Eric A. Brewer, Jeremy Condit, Robert Ennals, David Gay, Matthew Harren, George C. Necula, Feng Zhou. hotos 2007: [doi]

Enforcing resource bounds via static verification of dynamic checksAjay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula. TOPLAS, 29(5), 2007. [doi]

Shape Analysis with Structural Invariant CheckersBor-Yuh Evan Chang, Xavier Rival, George C. Necula. SAS 2007: 384-401 [doi]

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

A polynomial-time algorithm for global value numberingSumit Gulwani, George C. Necula. SCP, 64(1):97-114, 2007. [doi]

PrefaceJens Knoop, George C. Necula, Wolf Zimmermann. ENTCS, 176(3):1-2, 2007. [doi]

Proceedings of TLDI 07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007François Pottier, George C. Necula, editors, ACM, 2007.

2006

2005

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

JVer: A Java VerifierAjay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula. cav 2005: 144-147 [doi]

Type-based verification of assembly language for compiler debuggingBor-Yuh Evan Chang, Adam J. Chlipala, George C. Necula, Robert R. Schneck. tldi 2005: 91-102 [doi]

The open verifier framework for foundational verifiersBor-Yuh Evan Chang, Adam J. Chlipala, George C. Necula, Robert R. Schneck. tldi 2005: 1-12 [doi]

Data Slicing: Separating the Heap into Independent RegionsJeremy Condit, George C. Necula. CC 2005: 172-187 [doi]

Precise interprocedural analysis using random interpretationSumit Gulwani, George C. Necula. POPL 2005: 324-337 [doi]

A randomized satisfiability procedure for arithmetic and uninterpreted function symbolsSumit Gulwani, George C. Necula. iandc, 199(1-2):107-131, 2005. [doi]

Using Dependent Types to Certify the Safety of Assembly CodeMatthew Harren, George C. Necula. SAS 2005: 155-170 [doi]

PrefaceJens Knoop, George C. Necula, Wolf Zimmermann. ENTCS, 132(1):1-3, 2005. [doi]

PrefaceJens Knoop, George C. Necula, Wolf Zimmermann. ENTCS, 141(2):1-3, 2005. [doi]

Data Structure Specifications via Local Equality AxiomsScott McPeak, George C. Necula. cav 2005: 476-490 [doi]

Randomized Algorithms for Program Analysis and VerificationGeorge C. Necula, Sumit Gulwani. cav 2005: 1 [doi]

CCured: type-safe retrofitting of legacy softwareGeorge C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, Westley Weimer. TOPLAS, 27(3):477-526, 2005. [doi]

Mining Temporal Specifications for Error DetectionWestley Weimer, George C. Necula. TACAS 2005: 461-476 [doi]

2004

A Polynomial-Time Algorithm for Global Value NumberingSumit Gulwani, George C. Necula. SAS 2004: 212-227 [doi]

Global value numbering using random interpretationSumit Gulwani, George C. Necula. POPL 2004: 342-352 [doi]

Join Algorithms for the Theory of Uninterpreted FunctionsSumit Gulwani, Ashish Tiwari, George C. Necula. fsttcs 2004: 311-323 [doi]

Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted FunctionsSumit Gulwani, George C. Necula. SAS 2004: 328-343 [doi]

Elkhound: A Fast, Practical GLR Parser GeneratorScott McPeak, George C. Necula. CC 2004: 73-88 [doi]

Finding and preventing run-time error handling mistakesWestley Weimer, George C. Necula. OOPSLA 2004: 419-431 [doi]

By Reason and Authority: A System for Authorization of Proof-Carrying CodeNathan Whitehead, Martín Abadi, George C. Necula. csfw 2004: 236-250 [doi]

2003

2002

2001

Oracle-based checking of untrusted softwareGeorge C. Necula, Shree Prakash Rahul. POPL 2001: 142-154 [doi]

A Scalable Architecture for Proof-Carrying CodeGeorge C. Necula. FLOPS 2001: 21-39 [doi]

2000

1999

Enforcing Security and Safety with Proof-Carrying CodeGeorge C. Necula. ENTCS, 20, 1999. [doi]

1998

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

Efficient Representation and Validation of ProofsGeorge C. Necula, Peter Lee. lics 1998: 93-104

Safe, Untrusted Agents Using Proof-Carrying CodeGeorge C. Necula, Peter Lee. mas 1998: 61-91 [doi]

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

1997

Proof-Carrying CodeGeorge C. Necula. POPL 1997: 106-119 [doi]

Research on Proof-Carrying Code for Untrusted-Code SecurityGeorge C. Necula, Peter Lee. sp 1997: 204 [doi]

1996

Safe Kernel Extensions Without Run-Time CheckingGeorge C. Necula, Peter Lee. osdi 1996: 229-243