Thesis icon

Thesis

Saturation methods for global model-checking pushdown systems

Abstract:

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

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Oxford college:
St John's College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author

Contributors

Role:
Supervisor
Publication date:
2009
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
URN:
uuid:40263ddb-312d-4e18-b774-2caf4def0e76
Local pid:
ora:8542

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP