Skip to content

Research

Jump to bottom
Dominik Honnef edited this page May 16, 2022 · 44 revisions

This is a list of papers, talks and similar research on static analysis.

Collections

Topics

  • Variable type analysis

Papers

Intermediate languages

  • CIL: Intermediate Language and Tools for Analysis and Transformation of C programs by George C. Necula et al
  • SAIL: Static Analysis Intermediate Language with a Two-Level Representation by Isil Dillig et al
  • A CIL Tutorial by Zachary Anderson
  • REIL: A platform-independent intermediate representation of disassembled code for static code analysis by Thomas Dullien and Sebastian Porst

SSA/SSI

  • ABCD: Eliminating Array Bounds Checks on Demand by Rastislav Bodik et al
  • Adding Static Single Information Form to LLVM by Andre Luiz Camargos Tavares
  • An Efficient Method of Computing Static Single Assignment Form by Ron Cytron et al
  • Computing Liveness Sets for SSA-Form Programs by Florian Brandner et al
  • Efficiently Computing Static Single Assignment Form and the Control Dependence Graph by Ron Cytron et al
  • Efficiently Computing the Static Single Information Form by Jeremy Singer
  • Efficient SSI Conversion by André Luiz C. Tavares et al
  • Extended SSA Numbering: Introducing SSA Properties to Languages with Multi-level Pointers by Christopher Lapkowski and Laurie J. Hendren
  • Fast Liveness Checking for SSA-Form Programs by Benoit Boissinot et al
  • Interference Graphs for Procedures in Static Single Information Form are Interval Graphs by Philip Brisk and Majid Sarrafzadeh
  • Memory SSA - A Unified Approach for Sparsely Representing Memory Operations by Diego Novillo
  • Optimization in Static Single Assignment Form
  • Shimple: An Investigation of Static Single Assignment Form by Navindra Umanee
  • Simple and Efficient Construction of Static Single Assignment Form by Matthias Braun et al
  • Single-Pass Generation of Static Single-Assignment Form for Structured Languages by Marc M. Brandis and Hanspeter Mössenböck
  • Static Single Information Form by C. Scott Ananian and Martin Rinard
  • Static Single Information from a Functional Perspective by Jeremy Singer
  • SSI Extends SSA by Jeremy Singer
  • SSI revisited: A Program Representation for Sparse Data-flow Analyses by Andrew Tavares et al
  • SSI Revisited by Benoit Boissinot, Philip Brisk, Alain Darte, Fabrice Rastello
  • Tainted Flow Analysis on e-SSA-Form Programs by Andrei Rimsa et al
  • The Hot Path SSA Form: Extending the Static Single Assignment Form for Speculative Optimizations by Subhajit Roy and Y. N. Srikant
  • The SSA Representation Framework: Semantics, Analyses and GCC Implementation by Sebastian Pop
  • The Static Single Information Form by C. Scott Ananian

Other

  • Abstract Interpretation and Abstract Domains by Stefan Bygde
  • Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints by Patrick Cousot and Radhia Cousot
  • Accurate Static Branch Prediction by Value Range Propagation by Jason R. C. Patterson
  • A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings by Zhendong Su and David Wagner
  • A Dataflow Framework for Java by Stefan Heule and Charlie Garrett
  • A Fast and Low-Overhead Technique to Secure Programs Against Integer Overflows by Raphael Ernani Rodrigues et al
  • An Incremental Points-to Analysis with CFL-Reachability by Yi Lu, Lei Shang et al
  • An introduction to abstract interpretation by Samson Abramsky and Chris Hankin
  • A Simple, Fast Dominance Algorithm by Keith D. Cooper et al
  • A staged static program analysis to improve the performance of runtime monitoring by Eric Bodden et al
  • A Survey of Symbolic Execution Techniques by Roberto Baldoni et al
  • At Ease with Your Warnings: The Principles of the Salutogenesis Model Applied to Automatic Static Analysis by Jan-Peter Ostberg and Stefan Wagner
  • A unified approach to global program optimization by Gary A. Kildall
  • A Propagation Engine for GCC by Diego Novillo
  • Automatic Construction of Sparse Data Flow Evaluation Graphs by Ron Cytron et al
  • Bidirectional Data Flow Analysis : Myths and Reality by Uday P. Khedker and Dhananjay M. Dhamdhere
  • Bitwise: Optimizing Bitwidths Using Data-Range Propagation by Mark William Stephenson
  • Combining Model Checking and Data-Flow Analysis by Dirk Beyer, Sumit Gulwani, and David A. Schmidt
  • Compiler Analysis of the Value Ranges for Variables by William H. Harrison
  • Computing Dominators and Dominance Frontiers by Preston Briggs
  • Constant Propagation with Conditional Branches by Mark N. Wegman and F. Kenneth Zadeck
  • Datalog for Static Analysis by Ben Greenman
  • Debugging Static Analysis by Lisa Nguyen Quang Do et al
  • DUCKEE GO: Dynamic and User-friendly ConcoliK Execution Engine in GO by Christopher Shao et al
  • Efficient and Effective Handling of Exceptions in Java Points-To Analysis by George Kastrinis and Yannis Smaragdakis
  • Efficient Graph Reachability Query Answering using Tree Decomposition by Fang Wei
  • Evaluating “find a path” reachability queries by Panagiotis Bouros et al
  • Exploiting Postdominance for Speculative Parallelization by Mayank Agarwhal
  • Finding Dominators in Practice by Loukas Georgiadis et al
  • Flow insensitive relational static analysis by Solène Mirliaz, David Pichardie
  • Function Outlining by Peng Zhao and José Nelson Amaral
  • FUZZIFICATION: Anti-Fuzzing Techniques by Jinho Jung
  • Go-Sanitizer: Bug-Oriented Assertion Generation for Golang by Cong Wang et al
  • GPU-Accelerated Fixpoint Algorithms for Faster Compiler Analyses by Thorsten Blaß and Michael Philippsen
  • Hoopl: A Modular, Reusable Library for Dataflow Analysis and Transformation by Norman Ramsey et al
  • How Developers Engage with Static Analysis Tools in Different Contexts by Carmine Vassallo et al
  • How Many of All Bugs Do We Find? A Study of Static Bug Detectors by Andrew Habib and Michael Pradel
  • Implementation Techniques for Efficient Data-Flow Analysis of Large Programs by Darren C. Atkinson and William G. Griswold
  • Improving Switch Lowering for The LLVM Compiler System by Anton Korobeynikov
  • In Defense of Unsoundness by Ben Livshits et al
  • Infeasible Paths Detection Using Static Analysis by Burhan Barhoush and Izzat Alsmadi
  • Interprocedural Symbolic Range Propagation for Optimizing Compilers by Hansang Bae and Rudolf Eigenmann
  • Introduction to Abstract Interpretation by Bruno Blanchet
  • Introduction to set constraint-based program analysis by Alexander Aiken
  • Lessons from Building Static Analysis Tools at Google by Caitlin Sadowski et al
  • Making Context-sensitive Points-to Analysis with Heap Cloning Practical For The Real World by Chris Lattner et al
  • Modern Code Review: A Case Study at Google by Caitlin Sadowski et al
  • Monotone Data Flow Analysis Frameworks by John B. Kam and Jeffrey D. Ullman
  • Nesting of Reducible and Irreducible Loops by Paul Havlak
  • On Benchmarking the Capability of Symbolic Execution Tools with Logic Bombs by Hui Xu et al
  • Online algorithms for partially ordered sets by Mikko Herranen
  • On Loops, Dominators, and Dominance Frontiers by G. Ramalingam
  • On the Impact of Programming Languages on Code Quality
  • Path-Sensitive Analysis Using Edge Strings by Armand Navabi et al
  • Path-Sensitive Data Flow Analysis Simplified by Kirsten Winter et al
  • Path-Tree: An Efficient Reachability Indexing Scheme for Large Directed Graphs by Ruoming Jin et al
  • Polynomial Precise Interval Analysis Revisited by Thomas Gawlitza et al
  • Program Analysis and Specialization for the C Programming Language by Lars Ole Andersen
  • Program Analysis as Constraint Solving by Sumit Gulwani et al
  • Program Analysis using Symbolic Ranges by Sriram Sankaranarayanan et al
  • Range Analysis with Abstract Interpretation by Yury Markovskiy
  • Reachability Queries in Very Large Graphs: A Fast Refined Online Search Approach by Rene R. Veloso et al
  • Rethinking Soot for Summary-Based Whole-Program Analysis by Dacong Yan et al
  • SafeStrings - Representing Strings as Structured Data by David Kelly et al
  • Scalable and precise range analysis on the interval lattice by Raphael Ernani Rodrigues
  • Scheduling Series-Parallel Task Graphs to Minimize Peak Memory by Enver Kayaaslan et al
  • Sound Control-Flow Graph Extraction for Java Programs with Exceptions by Afshin Amighi et al
  • Sparse Analysis of Variable Path Predicates Based Upon SSA-Form by Thomas S. Heinze and Wolfram Amme
  • Sparse Bidirectional DataFlow Analysis as a Basis for Type Inference by Jeremy Singer
  • Sparse Dataflow Analysis with Pointers and Reachability by Magnus Madsen and Anders Møller
  • Speed and Precision in Range Analysis by Victor Hugo Sperle Campos et al
  • Static Analysis Techniques and Tools: A Systematic Mapping Study
  • Static program analysis based on virtual register renaming by Jeremy Singer
  • SVF: Interprocedural Static Value-Flow Analysis in LLVM by Yulei Sui and Jingling Xue
  • Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions by Radu Rugina and Martin C. Rinard
  • Symbolic Execution with Mixed Concrete-Symbolic Solving by Corina S. Pasareanu et al
  • Taming the Static Analysis Beast by John Toman and Dan Grossman
  • Testing Source Code with the Logic Programming Language Prolog by Thomas Handwerker
  • The Design and Implementation of a Non-Iterative Range Analysis Algorithm on a Production Compiler by Douglas do Couto Teixeira and Fernando Magno Quintao Pereira
  • The LLVM Instruction Set and Compilation Strategy by Chris Lattner and Vikram Adve
  • The new intraprocedural Scalar Replacement of Aggregates by Martin Jambor
  • Translation Validation for the LLVM Compiler by Kevin Jacobus de Vos
  • Tricorder: Building a Program Analysis Ecosystem by Caitlin Sadowski et al
  • Using Static-Single-Information-Form for SCAD code generation by Alexander Schneiders
  • What Developers Want and Need from Program Analysis: An Empirical Study by Maria Christakis and Christian Bird
  • Why Don't Software Developers Use Static Analysis Tools to Find Bugs? by Brittany Johnson et al

SAT, SMT

  • Beaver: An SMT Solver for Quantifier-free Bit-vector Logic by Rhishikesh Shrikant Limaye and Sanjit A. Seshia
  • Bitvectors in SMT-RAT and their application to integer arithmetics by Andreas Krüger
  • Control-Flow Analysis with SAT Solvers by Steven Lyde and Matthew Might
  • DPVIS– A Tool to Visualize the Structure of SAT Instances by Carsten Sinz and Edda-Maria Dieringer
  • Further Steps Down The Wrong Path: Improving the Bit-Blasting of Multiplication by Martin Brain
  • LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR by Florian Merz, Stephan Falke, and Carsten Sinz
  • SMT Solving for Arithmetic Theories: Theory and Tool Support by Erika Abraham and Gereon Kremer

Books

  • Static Program Analysis by Anders Møller and Michael I. Schwartzbach
  • Static Single Assignment Book by lots of authors
  • Value-Range Analysis of C Programs by Axel Simon
  • Data Flow Analysis - Theory and Practice by Uday P. Khedker et al

Talks

Clone this wiki locally