Analyzing pushdown systems with stack manipulation

DOI10.1016/j.ic.2017.12.003zbMath1388.68187OpenAlexW2779664120MaRDI QIDQ1706143

Fu Song

Publication date: 21 March 2018

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2017.12.003

zbMATH Keywords

reachability analysissoftware verificationpushdown systemsBoolean programsaturation procedure

Mathematics Subject Classification ID

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

Uses Software

• SPIN
• Bebop
• PuMoC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient CTL model-checking for pushdown systems
• Model checking dynamic pushdown networks
• Well-Structured Pushdown Systems
• Nested Timed Automata
• The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems
• Pushdown Model Checking for Malware Detection
• Model Checking Dynamic Pushdown Networks
• Analysis of recursively parallel programs
• Dense-Timed Pushdown Automata
• Efficient CTL Model-Checking for Pushdown Systems
• A semantics-based approach to malware detection
• An Automata-Theoretic Approach to Infinite-State Systems
• Reachability Analysis of the HTML5 Parser Specification and Its Application to Compatibility Testing
• Efficient Malware Detection Using Model-Checking
• Pushdown Systems with Stack Manipulation
• Introspective pushdown analysis of higher-order programs
• Well-Structured Pushdown System: Case of Dense Timed Pushdown Automata
• Weighted Pushdown Systems with Indexed Weight Domains
• On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• STACS 2005
• Computer Aided Verification
• Computer Aided Verification
• Weighted Pushdown Systems with Indexed Weight Domains
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• CONCUR 2005 – Concurrency Theory
• Reachability analysis of pushdown automata: Application to model-checking