Automatic verification of recursive procedures with one integer parameter.

DOI10.1016/S0304-3975(02)00397-3zbMath1053.68060OpenAlexW2030788986MaRDI QIDQ1401233

Peter Habermehl, Richard Mayr, Ahmed Bouajjani

Publication date: 17 August 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(02)00397-3

zbMATH Keywords

Model checkingVerificationContext-free processes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (7)

On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension ⋮ Reachability in pushdown register automata ⋮ Forward and backward application of symbolic tree transducers ⋮ Church synthesis on register automata over linearly ordered data domains ⋮ Unnamed Item ⋮ On Synthesis of Specifications with Arithmetic ⋮ Shortest Paths in One-Counter Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Subclasses of Presburger arithmetic and the polynomial-time hierarchy
• The complexity of Presburger arithmetic with bounded quantifier alternation depth
• Pushdown processes: Games and model-checking
• Model checking the full modal mu-calculus for infinite sequential processes
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• On Context-Free Languages
• Diophantine equations, Presburger arithmetic and finite automata
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Automatic verification of recursive procedures with one integer parameter.