Program Specification and Verification
- An Introduction to Program Analysis: Data Flow Analysis, Constraint-Based Analysis
- An Introduction to Program Analysis: Abstract Interpretation, Type and Effect Systems
- Data Flow Analysis: Interprocedural Analysis, Theoretical Properties
- Data Flow Analysis: Monotone Frameworks, Equation Solving
- Constraint-Based Analysis: Abstract Control Flow Analysis without Context Information
- Constraint-Based Analysis: Syntax-directed Control Flow Analysis
- Constraint-based Control Flow Analysis, Adding Context Information
- Abstract Interpretation: Representation Functions, Approximation of Fixed Points
- Abstract Interpretation: Galois Connections
- Type and Effect Systems: Types and Effects, Type Inference
- Type and Effect Systems: Side Effect Analysis, Exception Analysis
- Decision Procedures: Boolean Satisfiability, Boolean Decision Diagrams
- Decision Procedures: SAT and SMT, Theory Solvers in SMT
- Decision Procedures: Separation Logic, Symbolic Execution, Concolic Testing
- Model Checking: Model Checking and Temporal Logic
- Model Checking: Symbolic Model Checking with Boolean Decision Diagrams