Travelled to:1 × Austria
1 × Japan
1 × Korea
1 × Portugal
1 × Spain
18 × USA
3 × Denmark
3 × France
3 × Italy
4 × Canada
6 × United Kingdom
Collaborated with:S.Gulwani P.Lee ∅ K.Sen W.Weimer S.McPeak M.Harren J.Condit J.Burnim B.E.Chang R.R.Schneck W.Choi T.Elmas S.P.Rahul P.Reames C.Colby A.Chander D.Espinosa N.Islam X.Rival A.Chlipala Z.R.Anderson F.Zhou E.A.Brewer L.Gong S.Chandra M.Pradel P.Schuh D.Gay Ú.Erlingsson M.Abadi M.Vrable M.Budiu J.R.v.Behren T.A.Henzinger R.Jhala R.Majumdar G.Sutre F.Blau M.Plesko K.Cline I.Bagrak R.Ennals
Talks about:code (10) proof (8) use (8) analysi (7) type (6) program (5) certifi (5) specif (5) random (5) carri (5)
Person: George C. Necula
DBLP: Necula:George_C=
Facilitated 2 volumes:
Ed
EdContributed to:
2015
2015
2014
20132013
2013
2012
20112011
20072007
2006
20062006
2006
20052005200520052005
20052004200420042004
2003
200320032003
20032002200220022002
20012001200020002000
20001998199819981997Wrote 49 papers:
- ESEC-FSE-2015-SenNGC #execution #multi #named #summary #symbolic computation #using
- MultiSE: multi-path symbolic execution using value summaries (KS, GCN, LG, WC), pp. 842–853.
- SAS-2015-ChoiCNS #javascript #layout #named #type system
- SJS: A Type System for JavaScript with Fixed Object Layout (WC, SC, GCN, KS), pp. 181–198.
- OOPSLA-2014-PradelSNS #generative #latency #named #testing #user interface
- EventBreak: analyzing the responsiveness of user interfaces through performance-guided test generation (MP, PS, GCN, KS), pp. 33–47.
- ISMM-2013-ReamesN #garbage collection #towards
- Towards hinted collection: annotations for decreasing garbage collector pause times (PR, GCN), pp. 3–14.
- OOPSLA-2013-ChoiNS #android #approximate #learning #testing #user interface
- Guided GUI testing of android apps with minimal restart and approximate learning (WC, GCN, KS), pp. 623–640.
- PLDI-2013-ElmasBNS #concurrent #debugging #domain-specific language #named
- CONCURRIT: a domain specific language for reproducing concurrency bugs (TE, JB, GCN, KS), pp. 153–164.
- PPoPP-2012-BurnimENS #correctness #named #nondeterminism #parallel #specification
- NDetermin: inferring nondeterministic sequential specifications for parallelism correctness (JB, TE, GCN, KS), pp. 329–330.
- ASPLOS-2011-BurnimNS #parallel #semantics #source code #specification #thread
- Specifying and checking semantic atomicity for multithreaded programs (JB, GCN, KS), pp. 79–90.
- PLDI-2011-BurnimENS #correctness #named #nondeterminism #parallel #runtime #specification
- NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness (JB, TE, GCN, KS), pp. 401–414.
- ESOP-2007-ConditHAGN #dependent type #low level #programming
- Dependent Types for Low-Level Programming (JC, MH, ZRA, DG, GCN), pp. 520–535.
- SAS-2007-ChangRN #analysis #invariant
- Shape Analysis with Structural Invariant Checkers (BYEC, XR, GCN), pp. 384–401.
- CC-2006-Necula #dependent type #low level #type system #using
- Using Dependent Types to Port Type Systems to Low-Level Languages (GCN), p. 1.
- OSDI-2006-ErlingssonAVBN #named
- XFI: Software Guards for System Address Spaces (ÚE, MA, MV, MB, GCN), pp. 75–88.
- OSDI-2006-ZhouCABEHNB #named #using
- SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques (FZ, JC, ZRA, IB, RE, MH, GCN, EAB), pp. 45–60.
- SAS-2006-ChangHN #analysis #low level #using
- Analysis of Low-Level Code Using Cooperating Decompilers (BYEC, MH, GCN), pp. 318–335.
- VMCAI-2006-ChangCN #framework #program analysis #safety
- A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety (BYEC, AC, GCN), pp. 174–189.
- CAV-2005-ChanderEILN #java #named #verification
- JVer: A Java Verifier (AC, DE, NI, PL, GCN), pp. 144–147.
- CAV-2005-McPeakN #axiom #data type #similarity #specification
- Data Structure Specifications via Local Equality Axioms (SM, GCN), pp. 476–490.
- CAV-2005-NeculaG #algorithm #program analysis #random #verification
- Randomized Algorithms for Program Analysis and Verification (GCN, SG), p. 1.
- CC-2005-ConditN #independence #slicing
- Data Slicing: Separating the Heap into Independent Regions (JC, GCN), pp. 172–187.
- ESOP-2005-ChanderEILN #bound #dynamic analysis #verification
- Enforcing Resource Bounds via Static Verification of Dynamic Checks (AC, DE, NI, PL, GCN), pp. 311–325.
- POPL-2005-GulwaniN #analysis #interprocedural #precise #random #using
- Precise interprocedural analysis using random interpretation (SG, GCN), pp. 324–337.
- SAS-2005-HarrenN #assembly #dependent type #safety #using
- Using Dependent Types to Certify the Safety of Assembly Code (MH, GCN), pp. 155–170.
- TACAS-2005-WeimerN #detection #fault #mining #specification
- Mining Temporal Specifications for Error Detection (WW, GCN), pp. 461–476.
- CC-2004-McPeakN #generative #glr #named #parsing #performance
- Elkhound: A Fast, Practical GLR Parser Generator (SM, GCN), pp. 73–88.
- OOPSLA-2004-WeimerN #fault #runtime
- Finding and preventing run-time error handling mistakes (WW, GCN), pp. 419–431.
- POPL-2004-GulwaniN #random #using
- Global value numbering using random interpretation (SG, GCN), pp. 342–352.
- SAS-2004-GulwaniN #algorithm #polynomial
- A Polynomial-Time Algorithm for Global Value Numbering (SG, GCN), pp. 212–227.
- SAS-2004-GulwaniN04a #analysis #linear
- Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions (SG, GCN), pp. 328–343.
- CADE-2003-GulwaniN #random
- A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols (SG, GCN), pp. 167–181.
- LICS-2003-NeculaS #framework #generative
- A Sound Framework for Untrusted Verification-Condition Generators (GCN, RRS), pp. 248–260.
- PLDI-2003-ConditHMNW
- CCured in the real world (JC, MH, SM, GCN, WW), pp. 232–244.
- POPL-2003-GulwaniN #random #using
- Discovering affine equalities using random interpretation (SG, GCN), pp. 74–84.
- SOSP-2003-BehrenCZNB #internet #named #scalability #thread
- Capriccio: scalable threads for internet services (JRvB, JC, FZ, GCN, EAB), pp. 268–281.
- CADE-2002-SchneckN #approach #scalability
- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code (RRS, GCN), pp. 47–62.
- CAV-2002-HenzingerJMNSW #proving
- Temporal-Safety Proofs for Systems Code (TAH, RJ, RM, GCN, GS, WW), pp. 526–538.
- CC-2002-NeculaMRW #analysis #c #named #source code #tool support
- CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs (GCN, SM, SPR, WW), pp. 213–228.
- POPL-2002-NeculaMW #legacy #named #type safety
- CCured: type-safe retrofitting of legacy code (GCN, SM, WW), pp. 128–139.
- FLOPS-2001-Necula #architecture #scalability
- A Scalable Architecture for Proof-Carrying Code (GCN), pp. 21–39.
- POPL-2001-NeculaR
- Oracle-based checking of untrusted software (GCN, SPR), pp. 142–154.
- CADE-2000-NeculaL #generative #proving #theorem proving
- Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
- CAV-2000-ColbyLN #architecture #java
- A Proof-Carrying Code Architecture for Java (CC, PL, GCN), pp. 557–560.
- PLDI-2000-ColbyLNBPC #compilation #java
- A certifying compiler for Java (CC, PL, GCN, FB, MP, KC), pp. 95–107.
- PLDI-2000-Necula #compilation #optimisation #validation
- Translation validation for an optimizing compiler (GCN), pp. 83–94.
- PPDP-2000-Necula #design #implementation
- Proof-carrying code: design, implementation and applications (GCN), pp. 175–177.
- Best-of-PLDI-1998-NeculaL98a #compilation #design #implementation
- The design and implementation of a certifying compiler (with retrospective) (GCN, PL), pp. 612–625.
- LICS-1998-NeculaL #performance #proving #representation #validation
- Efficient Representation and Validation of Proofs (GCN, PL), pp. 93–104.
- PLDI-1998-NeculaL #compilation #design #implementation
- The Design and Implementation of a Certifying Compiler (GCN, PL), pp. 333–344.
- POPL-1997-Necula
- Proof-Carrying Code (GCN), pp. 106–119.