CSE 401: Final Project

Spring 2006

 Pushdown Temporal Logics For Software Model Checking

David Burkat

Faculty Advisor: Professor Rajeev Alur


In 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.

I developed a framework for proving the undefinability of properties in CaRet and segments of CaRet. This framework involves using Ehrenfeucht-Fraisse style games adapted to CaRet. These games will allow us to prove the expressive limitations of CaRet with respect to Visibly Pushdown Languages.

Additionally, I have found that in a few cases the Inside modality is CaRet definable. While the question of defining Inside in general in CaRet remains an open question, many nontrivial Inside properties are indeed definable.