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 (77)
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
This page was built for publication: Verifying programs with unreliable channels
