Graph Connectivity Verifier

Fall 2024

This was a group project focused on verifying graph connectivity for both undirected and directed graphs using Depth-First Search (DFS), Z3 constraints, and Tarjan’s algorithm. The program takes user-inputted graphs from text files and determines their connectivity properties, such as reachability, weak connectivity, and strong connectivity.
My contributions included developing the connectivity verification for undirected graphs, implementing DFS-based connectivity checks, and integrating Z3 constraints for logical verification. Additionally, I implemented test cases to validate correctness and collaborated on ensuring the efficiency and accuracy of the implementation.