Reading list

Dynamic Invariant Generation

• The Daikon system for dynamic detection of likely invariants
• Using dynamic analysis to discover polynomial and array invariants

Testing

• A survey of symbolic execution techniques
• Evaluating fuzz testing
• Mutation (read Mutation Testing from Fuzzing Book)

Verification

• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations: abstraction domain used by MN-BaB (one of the top performers at VNN-COMP)
• An axiomatic basis for computer programming
• Model checking: algorithmic verification and debugging: model checking, abstract interpretation, symbolic testing
• Towards Verifying the Geometric Robustness of Large-scale Neural Networks

Attacking

• A Branch and Bound Framework for Stronger Adversarial Attacks of ReLU Networks

Synthesis/Repair

• Genprog: A generic method for automatic software repair
• Syntax-guided synthesis

Complexity Analysis

• Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints

Modern Applications

• A review of formal methods applied to machine learning

Book

• Fuzzing Book by A. Zeller
• Formal Reasoning About Programs by A. Chlipala
• Static Program Analysis by Anders Møller and Michael I. Schwartzbach
• Intro to Abstraction Interpretation Abramsky and Hakin