Saturation methods for global model-checking pushdown systems

Thesis

Pushdown systems equip a finite state system with an unbounded stack memory, and are thus infinite state. By recording the call history on the stack, these systems provide a natural model for recursive procedure calls. Model-checking for pushdown systems has been well-studied. Tools implementing pushdown model-checking (e.g. Moped) are an essential back-end component of high-profile software model checkers such as SLAM, Blast and Terminator.

Higher-order pushdown systems define a mo...

Expand abstract

Authors: Hague, M

• Publication date: 2009
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: Oxford University, UK
• Language: English
• Keywords: temporal logic; verification; model-checking; higher-order pushdown automata; pushdown automata
• Subjects: Modal logic; Theory and automated verification; Applications and algorithms; Computer science (mathematics); Computing