Faculty Publications - George Necula

Book chapters or sections

• B. E. Chang, X. Rival, and G. Necula, "Shape analysis with structural invariant checkers," in Static Analysis: Proc. 14th Intl. Symp. (SAS 2007), H. Riis Nielsen and G. File, Eds., Lecture Notes in Computer Science, Vol. 4634, Berlin, Germany: Springer-Verlag, 2007, pp. 384-401.
• J. Condit, M. Harren, Z. Anderson, D. Gay, and G. Necula, "Dependent types for low-level programming," in Programming Languages and Systems: Proc. 16th European Symp. on Programming (ESOP 2007), R. De Nicola, Ed., Lecture Notes in Computer Science, Vol. 4421, Berlin, Germany: Springer-Verlag, 2007, pp. 520-535.
• B. E. Chang, M. Harren, and G. Necula, "Analysis of low-level code using cooperating compilers," in Static Analysis: Proc. 13th Intl. Symp. (SAS 2006), K. Yi, Ed., Lecture Notes in Computer Science, Vol. 4134, Berlin, Germany: Springer-Verlag, 2006, pp. 318-335.
• B. E. Chang, A. Chlipala, and G. Necula, "A framework for certified program analysis and its applications to mobile-code safety," in Verification, Model Checking, and Abstract Interpretation: Proc. 7th Intl. Conf. (VMCAI 2006), E. A. Emerson and K. S. Namjoshi, Eds., Lecture Notes in Computer Science, Vol. 3855, Berlin, Germany: Springer-Verlag, 2006, pp. 174-189.
• W. Weimer and G. Necula, "Mining temporal specifications for error detection," in Tools and Algorithms for the Construction and Analysis of Systems: Proc. 11th Intl. Conf. (TACAS 2005), N. Halbwachs and L. D. Zuck, Eds., Lecture Notes in Computer Science, Vol. 3440, Berlin, Germany: Springer-Verlag, 2005, pp. 461-476.
• A. Chander, D. Espinosa, N. Islam, P. Lee, and G. Necula, "Enforcing resource bounds via static verification of dynamic checks," in Programming Languages and Systems: Proc. 14th European Symp. on Programming (ESOP 2005), M. Sagiv, Ed., Lecture Notes in Computer Science, Vol. 3444, Berlin, Germany: Springer-Verlag, 2005, pp. 311-325.
• J. Condit and G. Necula, "Data slicing: Separating the heap into independent regions," in Compiler Construction: Proc. 14th Intl. Conf. (CC 2005), R. Bodik, Ed., Lecture Notes in Computer Science, Vol. 3443, Berlin, Germany: Springer-Verlag, 2005, pp. 172-187.
• M. Harren and G. Necula, "Using dependent types to certify the safety of assembly code," in Static Analysis: Proc. 12th Intl. Symp. (SAS 2005), C. Hankin and I. Siveroni, Eds., Lecture Notes in Computer Science, Vol. 3672, Berlin, Germany: Springer-Verlag, 2005, pp. 155-170.
• S. McPeak and G. Necula, "Data structure specifications via local equality axioms," in Computer Aided Verification: Proc. 17th Intl. Conf. (CAV 2005), K. Etessami and S. K. Rajamani, Eds., Lecture Notes in Computer Science, Vol. 3576, Berlin, Germany: Springer-Verlag, 2005, pp. 476-490.
• A. Chander, D. Espinosa, N. Islam, P. Lee, and G. Necula, "JVer: A Java verifier," in Computer Aided Verification: Proc. 17th Intl. Conf. (CAV 2005), K. Etessami and S. K. Rajamani, Eds., Lecture Notes in Computer Science, Vol. 3576, Berlin, Germany: Springer-Verlag, 2005, pp. 144-147.
• S. Gulwani, A. Tiwari, and G. Necula, "Join algorithms for the theory of uninterpreted functions," in FSTTCS 2004: Proc. 24th Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science, K. Lodaya and M. Mahajan, Eds., Lecture Notes in Computer Science, Vol. 3328, Berlin, Germany: Springer-Verlag, 2005, pp. 311-323.
• G. Necula, "Proof-carrying code," in Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed., Cambridge, MA: MIT Press, 2004, pp. 177-220.
• M. Harren and G. Necula, "Lightweight wrappers for interfacing with binary code in CCured," in Software Security -- Theories and Systems: Proc. 2nd Mext-NSF-JSPS Intl. Symp. (ISSS 2003). Revised Papers, K. Futatsugi, F. Mizoguchi, and N. Yonezaki, Eds., Lecture Notes in Computer Science, Vol. 3233, Berlin, Germany: Springer-Verlag, 2004, pp. 209-225.
• S. Gulwani and G. Necula, "A polynomial-time algorithm for global value numbering," in Static Analysis: Proc. 11th Intl. Symp. (SAS 2004), R. Giacobazzi, Ed., Lecture Notes in Computer Science, Vol. 3148, Berlin, Germany: Springer-Verlag, 2004, pp. 212-227.
• S. Gulwani and G. Necula, "Path-sensitive analysis for linear arithmetic and uninterpreted functions," in Static Analysis: Proc. 11th Intl. Symp. (SAS 2004), R. Giacobazzi, Ed., Lecture Notes in Computer Science, Vol. 3148, Berlin, Germany: Springer-Verlag, 2004, pp. 328-343.
• S. McPeak and G. Necula, "Elkhound: A fast, practical GLR parser generator," in Compiler Construction: Proc. 13th Intl. Conf. (CC 2004), E. Duesterwald, Ed., Lecture Notes in Computer Science, Vol. 2985, Berlin, Germany: Springer-Verlag, 2004, pp. 73-78.
• S. Gulwani and G. Necula, "A randomized satisfiability procedure for arithmetic and unterpreted function symbols," in Automated Deduction: Proc. 19th Intl. Conf. (CADE-19), F. Baader, Ed., Lecture Notes in Artificial Intelligence, Vol. 2741, Berlin, Germany: Springer-Verlag, 2003, pp. 167-181.
• G. Necula and R. R. Schneck, "Proof-carrying code with untrusted proof rules," in Software Security -- Theories and Systems: Proc. Mext-NSF-JSPS Intl. Symp. (ISSS 2002). Revised Papers, M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, Eds., Lecture Notes in Computer Science, Vol. 2609, Berlin, Germany: Springer-Verlag, 2003, pp. 247-252.
• T. A. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer, "Temporal-safety proofs for systems code," in Computer Aided Verification: Proc. 14th Intl. Conf. (CAV 2002), E. Brinksma and K. G. Larsen, Eds., Lecture Notes in Computer Science, Vol. 2404, Berlin, Germany: Springer-Verlag, 2002, pp. 526-538.
• R. R. Schneck and G. Necula, "A gradual approach to a more trustworthy, yet scalable, proof-carrying code," in Automated Deduction: Proc. 18th Intl. Conf. (CADE-18), A. Voronkov, Ed., Lecture Notes in Computer Science, Vol. 2392, Berlin, Germany: Springer-Verlag, 2002, pp. 47-62.
• G. Necula, "Proof-carrying code. Design and implementation," in Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen, Eds., NATO Science Series II: Mathematics, Physics and Chemistry, Vol. 62, Dordrecht, The Netherlands: Kluwer Academic Publishers, 2002, pp. 261-288.
• G. Necula, S. McPeak, S. P. Rahul, and W. Weimer, "CIL: Intermediate language and tools for analysis and transformation of C programs," in Compiler Construction: Proc. 11th Intl. Conf. (CC 2002), R. N. Horspool, Ed., Lecture Notes in Computer Science, Vol. 2304, Berlin, Germany: Springer-Verlag, 2002, pp. 213-228.
• G. Necula, "A scalable architecture for Proof-Carrying Code," in Functional and Logic Progamming: Proc. 5th Intl. Symp. (FLOPS 2001), H. Kuchen and K. Ueda, Eds., Lecture Notes in Computer Science, Vol. 2024, Berlin, Germany: Springer-Verlag, 2001, pp. 21-39.
• C. Colby, P. Lee, and G. Necula, "A proof-carrying code architecture for Java," in Computer Aided Verification: Proc. 12th Intl. Conf. (CAV 2000), E. A. Emerson and A. P. Sistla, Eds., Lecture Notes in Computer Science, Vol. 1855, Berlin, Germany: Springer-Verlag, 2000, pp. 557-560.
• G. Necula and P. Lee, "Proof generation in the Touchstone Theorem Prover," in Automated Deduction: Proc. 17th Intl. Conf. (CADE-17), D. McAllester, Ed., Lecture Notes in Artificial Intelligence, Vol. 1831, Berlin, Germany: Springer-Verlag, 2000, pp. 25-44.
• G. Necula and P. Lee, "Safe, untrusted agents using proof-carrying code," in Mobile Agents and Security, G. Vigna, Ed., Lecture Notes in Computer Science State-of-the-Art Survey, Vol. 1419, Berlin, Germany: Springer-Verlag, 1998, pp. 61-91.

Articles in journals or magazines

• W. Weimer and G. Necula, "Exceptional situations and program reliability," ACM Trans. Programming Languages and Systems, vol. 30, no. 2, pp. Art. 8:1-51, March 2008.
• A. Chander, D. Espinosa, N. Islam, P. Lee, and G. Necula, "Enforcing resource bounds via static verification of dynamic checks," ACM Trans. Programming Languages and Systems: Special Issue on ESOP '05, vol. 29, no. 5, pp. Art. 28, Aug. 2007.
• J. Knoop, G. Necula, and W. Zimmermann, "Preface," Electronic Notes in Theoretical Computer Science: Proc. 5th Intl. COCV Workshop, vol. 176, no. 3, pp. 1-2, July 2007.
• S. Gulwani and G. Necula, "A polynomial-time algorithm for global value numbering," Science of Computer Programming: Special Issue on SAS 2004, vol. 64, no. 1, pp. 97-114, Jan. 2007.
• J. Knoop, G. Necula, and W. Zimmermann, "Preface," Electronic Notes in Theoretical Computer Science: Proc. 4th Intl. COCV Workshop, vol. 141, no. 2, pp. 1-3, Dec. 2005.
• J. Knoop, G. Necula, and W. Zimmermann, "Preface," Electronic Notes in Theoretical Computer Science: Proc. 3rd Intl. COCV Workshop, vol. 132, no. 1, pp. 1-3, May 2005.
• S. Gulwani and G. Necula, "A randomized satisfiability procedure for arithmetic and uninterpreted function symbols," Information and Computation: Special Issue on CADE-19, vol. 199, no. 1-2, pp. 107-131, May 2005.
• G. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer, "CCured: Type-safe retrofitting of legacy software," ACM Trans. Programming Languages and Systems, vol. 27, no. 3, pp. 477-526, May 2005.
• S. Gulwani and G. Necula, "Precise interprocedural analysis using random interpretation," ACM SIGPLAN Notices, vol. 40, no. 1, pp. 324-337, Jan. 2005.
• W. Weimer and G. Necula, "Finding and preventing run-time error handling mistakes," ACM SIGPLAN Notices, vol. 39, no. 10, pp. 419-431, Oct. 2004.
• G. Necula and P. Lee, "Retrospective: The design and implementation of a certifying compiler," ACM SIGPLAN Notices: Best of PLDI 1979-1999, vol. 39, no. 4, pp. 614-625, April 2004.
• S. Gulwani and G. Necula, "Global value numbering using random interpretation," ACM SIGPLAN Notices, vol. 39, no. 1, pp. 342-352, Jan. 2004.
• J. Condit, M. Harren, S. McPeak, G. Necula, and W. Weimer, "CCured in the real world," ACM SIGPLAN Notices, vol. 38, no. 5, pp. 232-244, 2003.
• R. von Behren, J. Condit, F. Zhou, G. Necula, and E. Brewer, "Capriccio: Scalable threads for Internet services," ACM Operating Systems Review, vol. 37, no. 5, pp. 268-281, Dec. 2003.
• S. Gulwani and G. Necula, "Discovering affine equalities using random interpretation," ACM SIGPLAN Notices, vol. 38, no. 1, pp. 74-84, Jan. 2003.
• G. Necula, S. McPeak, and W. Weimer, "CCured: Type-safe retrofitting of legacy code," ACM SIGPLAN Notices, vol. 37, no. 1, pp. 128-139, Jan. 2002.
• G. Necula and S. P. Rahul, "Oracle-based checking of untrusted software," ACM SIGPLAN Notices, vol. 36, no. 3, pp. 142-154, March 2001.
• C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko, and K. Cline, "A certifying compiler for Java," ACM SIGPLAN Notices, vol. 35, no. 5, pp. 95-107, May 2000.
• G. Necula, "Translation validation for an optimizing compiler," ACM SIGPLAN Notices, vol. 35, no. 5, pp. 83-94, May 2000.
• G. Necula and S. Rahul, "A logic-based approach to software system safety and security (Invited Paper)," ACM SIGSOFT Software Engineering Notes, vol. 25, no. 1, pp. 67-68, Jan. 2000.
• G. Necula, "Enforcing security and safety with proof-carrying code," Electronic Notes in Theoretical Computer Science: Proc. MFPS XV, vol. 20, no. 1, pp. 117-131, May 1999.
• G. Necula and P. Lee, "The design and implementation of a certifying compiler," ACM SIGPLAN Notices, vol. 33, no. 5, pp. 333-344, May 1998.
• G. Necula and P. Lee, "Safe kernel extensions without run-time checking," ACM Operating Systems Review, vol. 30, no. SI, pp. 229-243, Oct. 1996.

Articles in conference proceedings

• Z. Anderson, E. Brewer, J. Condit, R. Ennals, D. Gay, M. Harren, G. Necula, and F. Zhou, "Beyond bug-finding: Sound program analysis for Linux," in Proc. 11th USENIX Workshop on Hot Topics in Operating Systems (HotOS XI), Berkeley, CA: USENIX Association, 2007, pp. 6 pg.
• U. Erlingsson, M. Abadi, M. Vrable, M. Budiu, and G. Necula, "XFI: Software guards for system address spaces," in Proc. 7th USENIX Symp. on Operating Systems Design and Implementation (OSDI '06), Berkeley, CA: USENIX Association, 2006, pp. 75-88.
• F. Zhou, J. P. Condit, Z. R. Anderson, I. Bagrak, R. Ennals, M. T. Harren, G. Necula, and E. Brewer, "SafeDrive: Safe and recoverable extensions using language-based techniques," in Proc. 7th USENIX Symp. on Operating Systems Design and Implementation (OSDI '06), Berkeley, CA: USENIX Association, 2006, pp. 45-60.
• A. Chlipala and G. Necula, "Cooperative integration of an interactive proof assistant and an automated prover," in Proc. 6th Intl. Workshop on Strategies in Automated Deduction (STRATEGIES 2006), M. Archer, T. Boy de la Tour, and C. Munoz, Eds., 2006, pp. 19 pg.
• B. E. Chang, A. Chlipala, G. Necula, and R. R. Schneck, "Type-based verification of assembly language for compiler debugging," in Proc. 2005 ACM SIGPLAN Intl. Workshop on Types in Languages Design and Implementation (TLDI '05), New York, NY: The Association for Computing Machinery, Inc., 2005, pp. 91-102.
• B. E. Chang, A. Chlipala, G. Necula, and R. R. Schneck, "The open verifier framework for foundational verifiers," in Proc. 2005 ACM SIGPLAN Intl. Workshop on Types in Languages Design and Implementation (TLDI '05), New York, NY: The Association for Computing Machinery, Inc., 2005, pp. 1-12.
• S. Gulwani and G. Necula, "Precise interprocedural analysis using random interpretation," in Proc. 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '05), New York, NY: The Association for Computing Machinery, Inc., 2005, pp. 324-337.
• W. Weimer and G. Necula, "Finding and preventing run-time error handling mistakes," in Proc. 19th Annual Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '04), New York, NY: The Association for Computing Machinery, Inc., 2004, pp. 419-431.
• N. Whitehead, M. Abadi, and G. Necula, "By reason and authority: A system for authorization of proof-carrying code," in Proc. 17th IEEE Computer Security Foundations Workshop, Los Alamitos, CA: IEEE Computer Society, 2004, pp. 236-250.
• S. Gulwani and G. Necula, "Global value numbering using random interpretation," in Proc. 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '04), New York, NY: The Association for Computing Machinery, Inc., 2004, pp. 342-352.
• J. R. Von Behren, J. P. Condit, F. Zhou, G. Necula, and E. Brewer, "Capriccio: Scalable threads for internet services," in Proc. 19th ACM Symp. on Operating Systems Principles (SOSP '03), New York, NY: The Association for Computing Machinery, Inc., 2003, pp. 268-281.
• G. Necula and R. R. Schneck, "A sound framework for untrusted verification-condition generators," in Proc. 18th Annual IEEE Symp. on Logic in Computer Science (LICS 2003), Los Alamitos, CA: IEEE Computer Society, 2003, pp. 248-260.
• J. Condit, M. Harrren, S. McPeak, G. Necula, and W. Weimer, "CCured in the real world," in Proc. 2003 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI '03), New York, NY: The Association for Computing Machinery, Inc., 2003, pp. 232-244.
• S. Gulwani and G. Necula, "Discovering affine equalities using random interpretation," in Proc. 30th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '03), New York, NY: The Association for Computing Machinery, Inc., 2003, pp. 74-84.
• G. Necula, S. McPeak, and W. Weimer, "CCured: Type-safe retrofitting of legacy code," in Proc. 29th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '02), New York, NY: The Association for Computing Machinery, Inc., 2002, pp. 128-139.
• G. Necula and S. P. Rahul, "Oracle-based checking of untrusted software," in Proc. 28th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '01), New York, NY: The Association for Computing Machinery, Inc., 2001, pp. 142-154.
• G. Necula, "Proof-carrying code: Design, implementation and applications (Abstract)," in Proc. 2nd ACM SIGPLAN Intl. Conf. on Principles and Practice of Declarative Programming (PPDP '00), New York, NY: The Association for Computing Machinery, Inc., 2000, pp. 175-177.
• C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko, and K. Cline, "A certifying compiler for Java," in Proc. 2000 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI '00), The Association for Computing Machinery, Inc., 2000, pp. 95-107.
• G. Necula, "Translation validation for an optimizing compiler," in Proc. ACM SIGPLAN 2000 Conf. on Programming Language Design and Implementation (PLDI '00), New York, NY: The Association for Computing Machinery, Inc., 2000, pp. 83-94.
• G. Necula and P. Lee, "Efficient representation and validation of proofs," in Proc. 13th Annual IEEE Symp. on Logic in Computer Science (LICS 1998), Los Alamitos, CA: IEEE Computer Society, 1998, pp. 93-104.
• G. Necula and P. Lee, "The design and implementation of a certifying compiler," in Proc. ACM SIGPLAN 1998 Conf. on Programming Language Design and Implementation (PLDI '98), A. M. Berman, Ed., New York, NY: The Association for Computing Machinery, Inc., 1998, pp. 333-344.
• G. Necula and P. Lee, "Research on proof-carrying code for untrusted-code security," in Proc. 1997 IEEE Symp. on Security and Privacy, Los Alamitos, CA: IEEE Computer Society, 1997, pp. 204-204.
• G. Necula, "Proof-carrying code," in Conference Record of the 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL '97), New York, NY: The Association for Computing Machinery, Inc., 1997, pp. 106-119.
• G. Necula and P. Lee, "Best Paper Award: Safe kernel extensions without run-time checking," in Proc. 2nd USENIX Symp. on Operating Systems Design and Implementation (OSDI '96), Berkeley, CA: USENIX Association, 1996, pp. 229-244.

Conference proceedings (edited)

• G. Necula and P. Wadler, Eds., Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.

Technical Reports

• D. Coetzee, A. Bhaskar, and G. Necula, "A model and framework for reliable build systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2012-27, Feb. 2012. [abstract]
• J. Burnim, T. Elmas, G. Necula, and K. Sen, "NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-143, Dec. 2011. [abstract]
• R. Sauciuc and G. Necula, "Reverse Execution With Constraint Solving," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-67, May 2011. [abstract]
• K. Asanovic, R. Bodik, J. Demmel, T. Keaveny, K. Keutzer, J. D. Kubiatowicz, E. A. Lee, N. Morgan, G. Necula, D. A. Patterson, K. Sen, J. Wawrzynek, D. Wessel, and K. A. Yelick, "The Parallel Computing Laboratory at U.C. Berkeley: A Research Agenda Based on the Berkeley View," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2008-23, March 2008. [abstract]
• B. E. Chang, X. Rival, and G. Necula, "Shape Analysis with Structural Invariant Checkers," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-80, June 2007. [abstract]
• J. P. Condit, M. T. Harren, Z. R. Anderson, D. Gay, and G. Necula, "Dependent Types for Low-Level Programming," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-129, Oct. 2006. [abstract]
• B. E. Chang, M. T. Harren, and G. Necula, "Analysis of Low-Level Code Using Cooperating Decompilers," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-86, June 2006. [abstract]
• S. Gulwani and G. C. Necula, "Precise Interprocedural Analysis using Random Interpretation (Revised version)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1353, Aug. 2005. [abstract]
• S. Gulwani and G. C. Necula, "Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-04-1325, May 2004. [abstract]
• S. Gulwani and G. C. Necula, "Global Value Numbering Using Random Interpretation (Full version)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1296, Nov. 2003. [abstract]
• S. Gulwani and G. C. Necula, "A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols (Full Version)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-03-1241, April 2003. [abstract]
• S. P. Rahul and G. C. Necula, "Proof Optimization Using Lemma Extraction," EECS Department, University of California, Berkeley, Tech. Rep. UCB/CSD-01-1143, May 2001. [abstract]
• P. A. Dinda, G. Necula, and M. Price, "MacFS: A Portable Macintosh File System Library," School of Computer Science, Carnegie Mellon University, Tech. Rep. CMU/CS-98-145, July 1998.
• G. Necula and P. Lee, "Efficient Representation and Validation of Logical Proofs," School of Computer Science, Carnegie Mellon University, Tech. Rep. CMU/CS-97-172, Oct. 1997.
• G. Necula and P. Lee, "Proof-Carrying Code," Deparment of Computer Science, Carnegie Mellon University, Tech. Rep. CMU/CS-96-165, Nov. 1996.
• G. Necula and L. George, "Accounting for the Performance of Standard ML on the DEC Alpha," AT&T Bell Labs, Murray Hill, NJ, Sep. 1994.

Software

• G. Necula, S. McPeak, W. Weimer, B. Liblit, and M. Harren, "CIL: C Intermediate Language (Version 1.3.6)," 2007. [abstract]
• G. Necula, S. McPeak, W. Weimer, M. Harren, and J. Condit, "CCured (Version 1.3.5)," 2007. [abstract]

Patents

• A. Chandler, N. Islam, D. Espinosa, P. Lee, and G. Necula, "Method and apparatus for enforcing safety properties of computer programs by generatiing and solving constraints," U.S. Patent Application. Nov. 2005.
• A. Chandler, N. Islam, D. Espinosa, G. Necula, and P. Lee, "Performing checks on the resource usage of computer programs," U.S. Patent Application. Dec. 2004.
• G. C. Necula and P. Lee, "Safe to execute verification of software," U.S. Patent 6,128,774. Oct. 2000.

Talks or presentations

• G. Necula, "Using Dependent Types to Port Type Systems to Low-Level Languages (Invited Talk)," presented at 15th Intl. Conf. on Compiler Construction (CC 2006), Vienna, Austria, March 2006.
• G. Necula and S. Gulwani, "Randomized Algorithms for Program Analysis and Verification (Invited Talk)," presented at 17th Intl. Conf. on Computer Aided Verification, Edinburgh, Scotland, UK, July 2005.

Ph.D. Theses

• G. Necula, "Compiling with Proofs," School of Computer Science, Carnegie Mellon University, Sep. 1998.