CSE 401: Final Project
Pushdown Temporal Logics For Software Model Checking
Faculty Advisor: Professor Rajeev Alur
AbstractIn this project I analyze the expressive power of a newly formulated temporal logic to determine its suitability for the specification and algorithmic verification of structured program correctness requirements. This temporal logic, known as CaRet, attempts to capture system specifications reliant on call-return matching while remaining model checkable in exponential time. More specifically, I developed a framework within which I explored both CaRet definable and CaRet undefinable properties.