# 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

- W. Choi, G. Necula, and K. Sen, "Guided GUI testing of android apps with minimal restart and approximate learning," in
*OOPSLA*, A. L. Hosking, P. T. Eugster, and C. V. Lopes, Eds., ACM, 2013, pp. 623-640. [abstract] - 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

- P. W. Choi, S. Chandra, G. Necula, and K. Sen, "SJS: a Typed Subset of JavaScript with Fixed Object Layout," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-10, March 2015.
- K. Sen, G. Necula, L. Gong, and P. W. Choi, "MultiSE: Multi-Path Symbolic Execution using Value Summaries," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-173, Oct. 2014.
- 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.