Programming Language Research Seminar 2019/20 fall

Static Analysis Topics

Concurrency and Weak Memory Models

• Relational Thread Interference Abstraction
  • Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models
  • Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
  • Relational Thread-Modular Static Value Analysis by Abstract Interpretation
• Model-checking abstractions and partial order reductions.
  • Effective stateless model checking for C/C++ concurrency
  • Verification of Concurrent Programs on Weak Memory Models
  • Partial Orders for Efficient Bounded Model Checking of Concurrent Software
  • Certified normalization of generalized traces
  • Owicki-Gries Reasoning for Weak Memory Models
• Possibly: Concurrency with Algebraic Effect Handlers

SMT-Based Static Analysis

• Model-Checking Approaches: Classics & Overviews
  • Counterexample-guided abstraction refinement for symbolic model checking
  • Bounded Model Checking Using Satisfiability Solving
  • Software Model Checking for People Who Love Automata
• Combined static analysis & model-checking
  • A Unifying View on SMT-Based Software Verification
  • ...
• SMT for Post-Processing Analysis Results
  • SMT-based false positive elimination in static program analysis
  • SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

Incremental, modular & demand-driven analysis

• Classic Fecht-Seidl solving algorithms & their incremental analysis.
• Verification of these solving algorithms.
• Some other papers on incremental/modular analysis.
• Procedure summaries...