Article

On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

Authors:

Parosh Aziz Abdulla,

Ahmed Bouajjani,

Bengt JonssonAuthors Info & Claims

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

Pages 305 - 318

Published: 28 June 1998 Publication History

Abstract

No abstract available.

Cited By

View all

Akroun LSalaün G(2018)Automated verification of automata communicating via FIFO and bag buffersFormal Methods in System Design10.1007/s10703-017-0285-852:3(260-276)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0285-8
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009860
Geffroy TLeroux JSutre GErdogmus HHavelund K(2017)Backward coverability with pruning for lossy channel systemsProceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software10.1145/3092282.3092292(132-141)Online publication date: 13-Jul-2017
https://dl.acm.org/doi/10.1145/3092282.3092292
Show More Cited By

Index Terms

On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

Index terms have been assigned to the content through auto-classification.

Recommendations

Model Checking Probabilistic Lossy Channel Systems
Simulating perfect channels with probabilistic lossy channels

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on ...
Reachability analysis of protocols with FIFO channels
SIGCOMM '83: Proceedings of the symposium on Communications Architectures & Protocols

In a complete protocol design process, it is often important to validate the protocol for general correctness properties such as boundedness, deadlock absence, and well-formedness. However, for any general protocol modeled as a number of communicating ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

June 1998

550 pages

ISBN:3540646086

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 June 1998

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Akroun LSalaün G(2018)Automated verification of automata communicating via FIFO and bag buffersFormal Methods in System Design10.1007/s10703-017-0285-852:3(260-276)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0285-8
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009860
Geffroy TLeroux JSutre GErdogmus HHavelund K(2017)Backward coverability with pruning for lossy channel systemsProceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software10.1145/3092282.3092292(132-141)Online publication date: 13-Jul-2017
https://dl.acm.org/doi/10.1145/3092282.3092292
Konnov ILazić MVeith HWidder JCastagna GGordon A(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009860(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009860
Park CIm HRyu S(2016)Precise and scalable static analysis of jQuery using a regular expression domainACM SIGPLAN Notices10.1145/3093334.298922852:2(25-36)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/3093334.2989228
Park CIm HRyu SIerusalimschy R(2016)Precise and scalable static analysis of jQuery using a regular expression domainProceedings of the 12th Symposium on Dynamic Languages10.1145/2989225.2989228(25-36)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2989225.2989228
Bouajjani AEmmi M(2014)Bounded phase analysis of message-passing programsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0276-z16:2(127-146)Online publication date: 1-Apr-2014
https://dl.acm.org/doi/10.1007/s10009-013-0276-z
Kloos JMajumdar RNiksic FPiskac R(2013)Incremental, Inductive CoverabilityProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958084(158-173)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958084
Esparza JKiefer SLuttenberger M(2008)Derivation Tree Analysis for Accelerated Fixed-Point ComputationProceedings of the 12th international conference on Developments in Language Theory10.1007/978-3-540-85780-8_24(301-313)Online publication date: 16-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-85780-8_24
Abdulla PDeneux JMahata PNylén A(2007)Using forward reachability analysis for verification of timed petri netsNordic Journal of Computing10.5555/1515784.151578514:1(1-42)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.5555/1515784.1515785
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Cited By

Index Terms

Recommendations

Model Checking Probabilistic Lossy Channel Systems

Simulating perfect channels with probabilistic lossy channels

Reachability analysis of protocols with FIFO channels

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations