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
- 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
Abstract Interpretation
- Efficient chaotic iteration strategies with widenings, FMPA'93
- A static analyzer for large safety-critical software, PLDI'03
- Symbolic implementation of best abstract transformers, VMCAI'04
- A policy iteration algorithm for computing fixed points in static analysis of programs, CAV'05
- Lookahead widening, CAV'06
- Recency-abstraction for heap-allocated storage, SAS'06
- Static analysis in disjunctive numerical domains, SAS'06
- Compositional shape analysis by means of bi-abduction, POPL'09
- Abstraction from tests, POPL'12
- TSL: A system for generating abstract interpreters and its application to machine-code analysis, TOPLAS'13
- Making numerical program analysis fast, PLDI'15
Dataflow Analysis
- 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
- 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