Verifying programs with unreliable channels
From MaRDI portal
Publication:1923094
DOI10.1006/inco.1996.0053zbMath0856.68096OpenAlexW2123160677MaRDI QIDQ1923094
Bengt Jonsson, Parosh Aziz Abdulla
Publication date: 1 October 1996
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/1ac3c57ecd88eee3527187e2f3a91cc8fe111a85
Related Items
Expired data collection in shared dataspaces., Eliminating the storage tape in reachability constructions., Reachability problems on reliable and lossy queue automata, Ideal Abstractions for Well-Structured Transition Systems, Forward analysis and model checking for trace bounded WSTS, Parameterized Verification of Communicating Automata under Context Bounds, Unnamed Item, The inclusion structure of partially lossy queue monoids and their trace submonoids, On deciding synchronizability for asynchronously communicating systems, Rational, recognizable, and aperiodic partially lossy queue languages, On selective unboundedness of VASS, The transformation monoid of a partially lossy queue, Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes, Unnamed Item, Unnamed Item, Cardinality constraints for arrays (decidability results and applications), Guessing the Buffer Bound for k-Synchronizability, Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines, Multiparty half-duplex systems and synchronous communications, Verification in loosely synchronous queue-connected discrete timed automata., Undecidable problems in unreliable computations., Monotonic Abstraction for Programs with Dynamic Memory Heaps, Existential Definability over the Subword Ordering, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Model checking parameterized asynchronous shared-memory systems, Mixing Lossy and Perfect Fifo Channels, On the Reachability Analysis of Acyclic Networks of Pushdown Systems, An extension of lazy abstraction with interpolation for programs with arrays, Deciding properties of integral relational automata, A Sound Algorithm for Asynchronous Session Subtyping, The decidability of verification under PS 2.0, Data flow analysis of asynchronous systems using infinite abstract domains, An automatic abstraction technique for verifying featured, parameterised systems, Forward Analysis and Model Checking for Trace Bounded WSTS, Computable fixpoints in well-structured symbolic model checking, The Two-Phase Commitment Protocol in an Extended π-Calculus, Ordinal recursive complexity of unordered data nets, Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms, Conversation protocols: a formalism for specification and verification of reactive electronic services, A classification of the expressive power of well-structured transition systems, Well-structured transition systems everywhere!, Ensuring completeness of symbolic verification methods for infinite-state systems, Quantitative analysis of probabilistic lossy channel systems, A Kleene theorem and model checking algorithms for existentially bounded communicating automata, Simulating perfect channels with probabilistic lossy channels, Unnamed Item, A general approach to comparing infinite-state systems with their finite-state specifications, Parameterized verification of coverability in infinite state broadcast networks, Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness, Well (and Better) Quasi-Ordered Transition Systems, On the termination and structural termination problems for counter machines with incrementing errors, A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations, Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols, Stochastic Games with Lossy Channels, The ω-Regular Post Embedding Problem, Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems, Forward analysis for WSTS, part I: completions, Decidability Results for Restricted Models of Petri Nets with Name Creation and Replication, The Parametric Complexity of Lossy Counter Machines, Complexity Hierarchies beyond Elementary, Monotonic Abstraction in Parameterized Verification, AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES, \(\pi\)-calculus with noisy channels, Monotonic Abstraction in Action, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Some complexity results for stateful network verification, Verification of probabilistic systems with faulty communication, Verification of programs with half-duplex communication, Verifying lossy channel systems has nonprimitive recursive complexity., Counter machines and verification problems., Model checking of systems with many identical timed processes, Non-deterministic transducer models of retransmission protocols over noisy channels, Automated formal analysis and verification: an overview, Finite reasons for safety, Undecidable verification problems for programs with unreliable channels, Generalized Post embedding problems, Guessing the buffer bound for k-synchronizability
