This project presents a solution to model a program in NuSMV syntax using MiniMC. MiniMC is a symbolic execution engine, and we aim to perform Computational Temporal Logic (CTL) analysis using a NuSMV implementation in MiniMC. We found that for programs where we do not need to need to verify the contents of registers, we can detect primitive vulnerable patterns in the program. Among the notable results are that we can detect a fork bomb with great accuracy as well as detect a double-free vulnerability. We conclude that the solution is able to detect some vulnerable patterns in programs, but that it is not able to detect all vulnerable patterns. We note that mostly due to limitations in MiniMC we are not able to detect all vulnerable patterns, as MiniMC is not able to load and store pointers on the heap. Furthermore, due to MiniMC using LLVM IR and subsequently SSA form, detecting patterns operating on registers is difficult.