Saturation methods for global model-checking pushdown systems
<p>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 implem...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2009
|
| Subjects: |