Tools and Algorithms for the Construction and Analysis of Systems

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

Mathematics Subject Classification ID

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

03B44: Temporal logic

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

• SPIN