Saturation methods for global model-checking pushdown systems

Saturation methods for global model-checking pushdown systems

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

Full description

Bibliographic Details
Main Author: Hague, Matthew
Other Authors: Ong, C.-H. Luke
Published: University of Oxford 2009
Subjects:
005.3
Computer science (mathematics) : Applications and algorithms : Computing : Modal logic : Theory and automated verification : higher-order pushdown automata : pushdown automata : verification : temporal logic : model-checking
Online Access:http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.504366

Internet

http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.504366

Similar Items