Coursework from a software testing, analysis, and verification class (CS 329): JUnit 5 test design, coverage criteria, static analysis with an AST library, and formal verification in Dafny.
The class covered proving software correct rather than only checking it by hand. That spanned three areas: designing thorough test suites, analyzing and transforming code with an abstract syntax tree, and writing formally verified code with pre/post-condition contracts.
- Test design and coverage — black-box and white-box tests in JUnit 5, driven to MC/DC (modified condition/decision coverage), not just line coverage
- Static analysis — using an AST library to implement constant propagation (folding known constant values through the tree to simplify code) and type checking (rejecting programs where incompatible types interact)
- Formal verification — Dafny, where
requires,ensures, andmodifiesclauses let the verifier prove a function meets its specification at compile time - Reasoning about correctness — MC/DC decision analysis, type proofs, weakest preconditions, and specification-based black-box testing
The per-assignment code lived in separate repositories provided by the professor and kept private for reuse in later terms, so the assignment folders here (hw0–hw6, proj1-constant-propagation, proj2-type-checking) are empty placeholders naming each unit. What remains committed is my written work:
Final.pdf/Final.docxMidterm.pdf/Midterm.docx
The folder names map to the topics: JUnit 5, Dafny tutorial, specification-based black-box testing, MC/DC and type proofs, formal verification, weakest preconditions, constant propagation, and type checking.
- Java with JUnit 5
- Dafny for formal verification
- An abstract syntax tree library for the static-analysis projects