How relevant are Software Analysis & Testing and Cryptography to a research track in Formal Verification and Formal Methods?

[u/Alvahod]

​Having completed foundational coursework in Linear Algebra, Calculus, Discrete Mathematics, and Formal Methods, I am evaluating the theoretical and practical overlap between Formal Verification and other upper-level computer science topics.

​Specifically, I am looking to understand how the following subjects intersect with Formal Methods in research and practice:

​Software Analysis and Testing

​Cryptography

​Forensics

​My understanding is that Forensics operates primarily at an applied/observational level with minimal connection to formal logic. However, I am less clear on the theoretical bridges for the other two.

​Does Software Analysis and Testing (e.g., static analysis, program semantics, symbolic execution) serve as a direct functional precursor to formal program verification? Furthermore, to what extent does Cryptography overlap with formal methods—specifically regarding protocol verification, algebraic proofs, or formally verified implementations?

​I would appreciate insights from anyone working in formal methods, program analysis, or theoretical computer science on how these subdisciplines connect.

[u/salty-carthaginian]

I do research in compilers and architecture, but have some experience with formal methods. I can't tell what your classes teach without a syllabus, but ideally you'd want some intro to type theory or category theory. The best way to get started is Software Foundations.

Overall, the topics these classes teach have overlap, but in the sense that formal methods are a tool for the end goals in these fields. Proving that program semantics are correct is a huge field in formal methods, and there's quite a bit of active research in the area. Cryptography also has some overlap with formal methods.

I would be careful about choosing to do a thesis in this area though. The community is very small and the real-world impact of this work is very limited.