Tools and Algorithms for the Construction and Analysis of Systems
From MaRDI portal
Publication:5308427
DOI10.1007/b96393zbMath1126.68466MaRDI QIDQ5308427
Kousha Etessami, P. Madhusudan, Rajeev Alur
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
Related Items
Emergence in Context-Free Parallel Communicating Grammar Systems: What Does and Does not Make a Grammar System More Expressive Than Its Parts, Unnamed Item, Unnamed Item, CaRet With Forgettable Past, A Branching Time Variant of CaRet, Verification of programs with exceptions through operator precedence automata, Interval Temporal Logic for Visibly Pushdown Systems, Model Checking Temporal Properties of Recursive Probabilistic Programs, Branching Temporal Logic of Calls and Returns for Pushdown Systems, 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 structured context-free languages, 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, Visibly linear dynamic logic, Context-free timed formalisms: robust automata and linear temporal logics, Operator precedence temporal logic and model checking, Reachability of scope-bounded multistack pushdown systems, Multi-matching nested relations, Temporal logics with language parameters, 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, Unnamed Item, 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