Tools and Algorithms for the Construction and Analysis of Systems

From MaRDI portal
Publication:5308427


DOI10.1007/b96393zbMath1126.68466MaRDI QIDQ5308427

P. Madhusudan, Rajeev Alur, Kousha Etessami

Publication date: 28 September 2007

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

Full work available at URL: https://doi.org/10.1007/b96393


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

03B44: Temporal logic


Related Items

CaRet With Forgettable Past, Reducing behavioural to structural properties of programs with procedures, Model checking probabilistic systems against pushdown specifications, Temporal logics for concurrent recursive programs: satisfiability and model checking, Visibly pushdown modular games, Regular languages of nested words: fixed points, automata, and synchronization, Visibly linear temporal logic, Synthesis from component libraries with costs, Model checking dynamic memory allocation in operating systems, Summarization for termination: No return!, Compositional verification of sequential programs with procedures, Verification of well-formed communicating recursive state machines, Verification of scope-dependent hierarchical state machines, Reasoning about XML with temporal logics and automata, On the complexity of checking semantic equivalences between pushdown processes and finite-state processes, The complexity of model checking multi-stack systems, A generic framework for checking semantic equivalences between pushdown automata and finite-state automata, Visibly rational expressions, Propositional dynamic logic with recursive programs, Hybrid and First-Order Complete Extensions of CaRet, CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties, ProMoVer: Modular Verification of Temporal Safety Properties, Model Checking Procedural Programs, Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic, Model Checking Recursive Programs with Exact Predicate Abstraction, An Automata-Theoretic Approach to Infinite-State Systems


Uses Software