Resource-constrained model checking of recursive programs

DOI10.1007/3-540-46002-0_17MaRDI QIDQ4472242zbMATH OpenFDO

Authors Samik Basu, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan

Publication date 4 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2280/22800236.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• LTL model checking for recursive programs
• A BDD-based model checker for recursive programs
• Efficient CTL model-checking for pushdown systems
• Efficient CTL model-checking for pushdown systems
• Model checking LTL with regular valuations for pushdown systems

Cited in

(7)

• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
• Modeling and verification of infinite systems with resources
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
• LTL model checking for recursive programs
• A BDD-based model checker for recursive programs
• On-the-fly reachability and cycle detection for recursive state machines

This page was built for publication: Resource-constrained model checking of recursive programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4472242)