Article

The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems

Authors:

Sérgio Vale Aguiar Campos,

Edmund M. Clarke,

Marius MineaAuthors Info & Claims

CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification

Pages 452 - 455

Published: 22 June 1997 Publication History

Abstract

No abstract available.

Cited By

View all

Wan WBentahar JYahyaoui HBen Hamza A(2016)Verifying concurrent probabilistic systems using probabilistic-epistemic logic specificationsApplied Intelligence10.1007/s10489-016-0790-245:3(747-776)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10489-016-0790-2
Basagiannis SKatsaros PPombortsis A(2006)Interlocking control by distributed signal boxesProceedings of the 4th international conference on Parallel and Distributed Processing and Applications10.1007/11946441_32(317-328)Online publication date: 4-Dec-2006
https://dl.acm.org/doi/10.1007/11946441_32
Shankar SAsa SSipos VXu XRedmiles DEllman TZisman A(2005)Reasoning about real-time statecharts in the presence of semantic variationsProceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering10.1145/1101908.1101945(243-252)Online publication date: 7-Nov-2005
https://dl.acm.org/doi/10.1145/1101908.1101945
Show More Cited By

The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems

Recommendations

Verus: a tool for quantitative analysis of finite-state real-time systems

Symbolic model checking is a technique for verifying finite-state concurrent systems. Models with up to 10³⁰ states can often be verified in minutes. In this paper, we present a new tool to analyze real-time systems, based on this technique. We have ...
Verus: a tool for quantitative analysis of finite-state real-time systems
LCTES '95: Proceedings of the ACM SIGPLAN 1995 workshop on Languages, compilers, & tools for real-time systems

Symbolic model checking is a technique for verifying finite-state concurrent systems. Models with up to 10³⁰ states can often be verified in minutes. In this paper, we present a new tool to analyze real-time systems, based on this technique. We have ...
Verus: Verifying Rust Programs using Linear Ghost Types

The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification

June 1997

481 pages

ISBN:3540631666

Editor:
Orna Grumberg

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 June 1997

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wan WBentahar JYahyaoui HBen Hamza A(2016)Verifying concurrent probabilistic systems using probabilistic-epistemic logic specificationsApplied Intelligence10.1007/s10489-016-0790-245:3(747-776)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10489-016-0790-2
Basagiannis SKatsaros PPombortsis A(2006)Interlocking control by distributed signal boxesProceedings of the 4th international conference on Parallel and Distributed Processing and Applications10.1007/11946441_32(317-328)Online publication date: 4-Dec-2006
https://dl.acm.org/doi/10.1007/11946441_32
Shankar SAsa SSipos VXu XRedmiles DEllman TZisman A(2005)Reasoning about real-time statecharts in the presence of semantic variationsProceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering10.1145/1101908.1101945(243-252)Online publication date: 7-Nov-2005
https://dl.acm.org/doi/10.1145/1101908.1101945
Gu Z(2005)Solving real-time scheduling problems with model-checkingProceedings of the Second international conference on Embedded Software and Systems10.1007/11599555_20(186-197)Online publication date: 16-Dec-2005
https://dl.acm.org/doi/10.1007/11599555_20
Giese HTichy MBurmester SSchäfer WFlake S(2003)Towards the compositional verification of real-time UML designsACM SIGSOFT Software Engineering Notes10.1145/949952.94007828:5(38-47)Online publication date: 1-Sep-2003
https://dl.acm.org/doi/10.1145/949952.940078
Giese HTichy MBurmester SSchäfer WFlake SPaakki JInverardi P(2003)Towards the compositional verification of real-time UML designsProceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering10.1145/940071.940078(38-47)Online publication date: 1-Sep-2003
https://dl.acm.org/doi/10.1145/940071.940078
Ruf JKropf TBolsens I(2000)Analyzing real-time systemsProceedings of the conference on Design, automation and test in Europe10.1145/343647.343775(243-249)Online publication date: 1-Jan-2000
https://dl.acm.org/doi/10.1145/343647.343775

View Options

View options

Login options

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

Abstract

Cited By

Recommendations

Verus: a tool for quantitative analysis of finite-state real-time systems

Verus: a tool for quantitative analysis of finite-state real-time systems

Verus: Verifying Rust Programs using Linear Ghost Types

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations