List of papers
Path-sensitive analysis
[1] Sound, Complete and Scalable Path-Sensitive Analysis
Isil Dillig, Thomas Dillig, Alex Aiken
https://www.cs.utexas.edu/~isil/pldi006-dillig.pdf
[2] SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
Gogul Balakrishnan, Sriram Sankaranarayanan1, Franjo Ivancic, Ou Wei, and Aarti Gupta
http://www-cs-students.stanford.edu/~srirams/papers/sas2008.pdf
Dataflow analysis
[3] Precise Interprocedural Dataflow Analysis via Graph Reachability
Thomas Reps, Susan Horwitz, Mooly Sagiv
https://dl.acm.org/doi/pdf/10.1145/199448.199462
[4] Finding Optimum Abstractions in Parametric Dataflow Analysis
Xin Zhang, Mayur Naik, Hongseok Yang
https://www.cis.upenn.edu/~mhnaik/papers/pldi13.pdf
Program slicing
[5] Dynamic Program Slicing
Hiralal Agrawal, Joseph R. Horgan
https://dl.acm.org/doi/pdf/10.1145/93548.93576
Pointer analysis
[6] Pointer Analysis for Structured Parallel Programs
Radu Rugina, Martin C. Rinard
https://dl.acm.org/doi/pdf/10.1145/596980.596982
[7] Flow-Sensitive Pointer Analysis for Millions of Lines of Code
Ben Hardekopf, Calvin Lin
https://www.cs.utexas.edu/~lin/papers/cgo11.pdf
Analysis of concurrent programs
[8] Inductive Sequentialization of Asynchronous Programs
Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer
https://dl.acm.org/doi/pdf/10.1145/3385412.3385980
[9] Race Detection for Android Applications
Pallavi Maiya, Aditya Kanade, Rupak Majumdar
http://clweb.csa.iisc.ac.in/pallavi.maiya/droidRacer.pdf
[10] BIGFOOT: Static Check Placement for Dynamic Race Detection
Dustin Rhodes, Cormac Flanagan, Stephen N. Freund
https://dl.acm.org/doi/pdf/10.1145/3062341.3062350
[11] Dataflow Analysis for Concurrent Programs using Datarace Detection
Ravi Chugh, Jan W. Voung, Ranjit Jhala, Sorin Lerner
https://cseweb.ucsd.edu/~lerner/papers/radar.pdf
[12] Dynamic Partial-Order Reduction for Model Checking Software
Cormac Flanagan, Patrice Godefroid
https://users.soe.ucsc.edu/~cormac/papers/popl05.pdf
[13] A Compositional Deadlock Detector for Android Java
James Brotherston, Paul Brunet, Nikos Gorogiannis, Max Kanovich
http://www0.cs.ucl.ac.uk/staff/J.Brotherston/ASE21/deadlocks_final.pdf
Predicate abstraction
[14] Automatic Predicate Abstraction of C Programs
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani
http://web.cs.ucla.edu/~todd/research/pldi01.pdf
Constraint-based approaches, invariant inference
[15] Horn Clause Solvers for Program Verification
Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan and Andrey Rybalchenko
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf
[16] A Data-Driven CHC Solver
He Zhu, Stephen Magill, Suresh Jagannathan
https://www.cs.purdue.edu/homes/suresh/papers/pldi18.pdf
[17] Inductive Invariant Generation via Abductive Inference
Isil Dillig, Thomas Dillig, Boyang Li, Ken McMillan
https://www.cs.utexas.edu/~isil/oopsla13.pdf
[18] Danger Invariants
Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis
https://www.cs.ox.ac.uk/files/8323/danger-paper-extended.pdf
Program synthesis
[19] FlashMeta: A Framework for Inductive Program Synthesis
Oleksandr Polozov, Sumit Gulwani
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/oopsla15-pbe.pdf
[20] Program Synthesis using Conflict-Driven Learning
Yu Feng, Ruben Martins, Osbert Bastani, Isil Dillig
https://trustml.github.io/docs/pldi18b.pdf
[21] Scaling up Superoptimization
Phitchaya Mangpo Phothilimthana, Aditya Thakur, Rastislav Bodik, Dinakar Dhurjati
https://mangpo.net/papers/lens-asplos16.pdf
[22] Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis
Sergey Mechtaev, Jooyong Yi, Abhik Roychoudhury
https://www.comp.nus.edu.sg/~abhik/pdf/ICSE16-angelix.pdf
Verification of smart contracts
[23] Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong
https://link.springer.com/content/pdf/10.1007/978-3-030-99524-9_10.pdf