Tools and Algorithms for the Construction and Analysis of Systems

DOI10.1007/b107194zbMath1087.68598OpenAlexW2497867240MaRDI QIDQ5703798

Publication date: 10 November 2005

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

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Model-Checking HyperLTL for Pushdown Systems, Realizability of concurrent recursive programs, Delay-bounded scheduling without delay!, Verification of SpecC using predicate abstraction, Parameterized Verification of Communicating Automata under Context Bounds, Automated Synthesis of Distributed Controllers, The Complexity of Reversal-Bounded Model-Checking, SAT-Based Model Checking, Model Checking Concurrent Programs, Combining Model Checking and Testing, Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous, Static analysis of embedded real-time concurrent software with dynamic priorities, On Distributed Monitoring and Synthesis, The complexity of model checking multi-stack systems, Reducing behavioural to structural properties of programs with procedures, A pragmatic approach to stateful partial order reduction, Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions, Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis, Symbolic predictive analysis for concurrent programs, Recent advances on reachability problems for valence systems (invited talk), An automata-theoretic approach to the verification of distributed algorithms, Verification of STM on relaxed memory models, Bounded underapproximations, Verifying parallel programs with dynamic communication structures, Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning, Reachability of scope-bounded multistack pushdown systems, Faster Algorithms for Weighted Recursive State Machines, Temporal logics for concurrent recursive programs: satisfiability and model checking, Budget-bounded model-checking pushdown systems, Analysis of correct synchronization of operating system components, Compositional verification of sequential programs with procedures, Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, Leafy automata for higher-order concurrency, The decidability of verification under PS 2.0, Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete, Bounded Context Switching for Valence Systems, Verification of well-formed communicating recursive state machines, Verification of Boolean programs with unbounded thread creation, On the path-width of integer linear programming, Context-Bounded Analysis of TSO Systems, Model checking with bounded context switching, Reachability Analysis of Pushdown Systems with an Upper Stack, Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism, Decidable models of integer-manipulating programs with recursive parallelism, Games on Multi-stack Pushdown Systems, CCA-Secure Keyed-Fully Homomorphic Encryption, Realizability of Concurrent Recursive Programs, Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads, Interprocedural Analysis of Concurrent Programs Under a Context Bound, Context-Bounded Analysis of Concurrent Queue Systems, Program Analysis Using Weighted Pushdown Systems, Fine-grained complexity of safety verification, Verification of Parameterized Communicating Automata via Split-Width, On exteriority notions in book embeddings and treewidth, Context-Free Ambiguity Detection Using Multi-stack Pushdown Automata, Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations, Reasoning about Threads with Bounded Lock Chains, Verifying Parallel Programs with Dynamic Communication Structures, Games on Higher Order Multi-stack Pushdown Systems, Reducing concurrent analysis under a context bound to sequential analysis, Data Multi-Pushdown Automata, On the Complexity of Bounded Context Switching., On Symbolic Verification of Weakly Extended PAD, Verification of Asynchronous Programs with Nested Locks

Uses Software