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

Articles in conference proceedings

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

Software

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

Ph.D. Theses