Some Interesting Papers

Notice: just for fun; not a "sound, complete" reading list.

---

Algorithmic Verification

• Construction of abstract state graphs with PVS, CAV'97
  
• Counterexample-guided abstraction refinement, CAV'00
  
• Checking safety properties using induction and a SAT-solver, FMCAD'00
• Houdini, an annotation assistant for ESC/Java, FME'01
  
• Linear invariant generation using non-linear constraint solving, CAV'03
  
• Symbolic implementation of best abstract transformers, VMCAI'04
  
• SMT techniques for fast predicate abstraction, CAV'06
  
• Lazy abstraction with interpolants, CAV'06
  
• Software verification using k-induction, SAS'11
  
• Understanding IC3, SAT'12
  
• Software model checking for people who love automata, CAV'13
  
• Inductive invariant generation via abductive inference, OOPSLA'13
  
• ICE: A robust framework for learning invariants, CAV'14
  

---

Pointer/Alias Analysis

• Efficient context-sensitive pointer analysis for C programs, PLDI'95
  
• Relevant context inference, POPL'99
  
• Modular interprocedural pointer analysis using access paths, PLDI'00
  
• Undecidability of context-sensitive data-dependence analysis, TOPLAS'00
  
• Unification-based pointer analysis with directional assignments, PLDI'00
  
• Efficient field-sensitive pointer analysis for C, PASTE'04
  
• Demand-driven points-to analysis for Java, OOPSLA'05
  
• Refinement-based context-sensitive points-to analysis for Java, PLDI'06
  
• Making context-sensitive points-to analysis with heap cloning practical for the real world, PLDI'07
  
• The Ant and the Grasshopper: fast and accurate pointer analysis for millions of lines of code, PLDI'07
  
• Demand-driven alias analysis for C, POPL'08
  
• Semi-sparse flow-sensitive pointer analysis, POPL'09
  
• Points-to analysis with efficient strong updates, POPL'11
  
• Flow-sensitive pointer analysis for millions of lines of code, CGO'11
  
• Pick your contexts well: understanding object-sensitivity, POPL'11
  
• Hybrid context-sensitivity for points-to analysis, PLDI'13
  

---

Dataflow Analysis

• Efficient chaotic iteration strategies with widenings, FMPA'93
  
• Precise interprocedural dataflow analysis via graph reachability, POPL'95
  
• ESP: path-sensitive program verification in polynomial time, PLDI'02
  
• Weighted pushdown systems and their application to interprocedural dataflow analysis, SCP'05
  
• Practical extensions to the IFDS algorithm, CC'10
  
• Newtonian program analysis via tensor product, POPL'16
  

---

Static Bug Finding

• Tracking pointers with path and context sensitivity for bug detection in C programs, ESEC/FSE'03
  
• A static analyzer for large safety-critical software, PLDI'03
  
• Scalable error detection using Boolean satisfiability, POPL'05
  
• Effective typestate verification in the presence of aliasing, ISSTA'06, TOSEM'08
  
• Effective static race detection for Java, PLDI'06
  
• Practical memory leak detection using guarded value-flow analysis, PLDI'07
  
• Calysto: scalable and precise extended static checking, ICSE'09
  
• TAJ: effective taint analysis of Web applications, PLDI'09
  
• A few billion lines of code later using static analysis to find bugs in the real world, CACM'10
  
• Thresher: precise refutations for heap reachability, PLDI'13
  

---

Automated Reasoning

• Semantic minimization for three-valued logic, LICS'02
  
• A knowledge compilation map, JAIR'02
  
• Variable independence for first-order definable constraints, TOCL'03
  
• DPLL(T): fast decision procedures, CAV'04
  
• Quantifier elimination by lazy model enumeration, CAV'10
  
• Automating string processing in spreadsheets using input-output examples, POPL'11
  
• A method for symbolic computation of abstract operations, CAV'12
  
• Monadic decomposition, CAV'14, JACM'17
  
• Automating grammar comparison, OOPSLA'15
  
• A formalization of programs in first-order logic, KR'14, AI'16