article

An approach to systems verification

Authors:

William R. Bevier,

Warren A. Hunt, Jr.,

J. Strother Moore,

William D. YoungAuthors Info & Claims

Journal of Automated Reasoning, Volume 5, Issue 4

Pages 411 - 428

Published: 01 November 1989 Publication History

Abstract

No abstract available.

Cited By

View all

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Kaufmann MPecchiari P(2023)Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theoremJournal of Automated Reasoning10.1007/BF0024446316:1-2(181-222)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF00244463
Moore J(2022)A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocolFormal Aspects of Computing10.1007/BF012110816:1(60-91)Online publication date: 2-Jan-2022
https://dl.acm.org/doi/10.1007/BF01211081
Show More Cited By

Index Terms

An approach to systems verification

Recommendations

Verification approach of metropolis design framework for embedded systems

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Specification and automated verification of concurrent software systems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 5, Issue 4

Dec. 1989

132 pages

ISSN:0168-7433

Editor:
Larry Wos

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 1989

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Kaufmann MPecchiari P(2023)Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theoremJournal of Automated Reasoning10.1007/BF0024446316:1-2(181-222)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF00244463
Moore J(2022)A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocolFormal Aspects of Computing10.1007/BF012110816:1(60-91)Online publication date: 2-Jan-2022
https://dl.acm.org/doi/10.1007/BF01211081
Müller PShankar N(2021)The First Fifteen Years of the Verified Software ProjectTheories of Programming10.1145/3477355.3477362(93-124)Online publication date: 4-Oct-2021
https://dl.acm.org/doi/10.1145/3477355.3477362
Lööw AKumar RTan YMyreen MNorrish MAbrahamsson OFox AMcKinley KFisher K(2019)Verified compilation on a verified processorProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314622(1041-1053)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314622
Visser WBjørner NShankar NHerbsleb JDwyer MHerbsleb J(2014)Software engineering and automated deductionFuture of Software Engineering Proceedings10.1145/2593882.2593899(155-166)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2593882.2593899
Bjørner D(2011)DomainsRainbow of computer science10.5555/2001113.2001130(167-183)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2001113.2001130
Yang JHawblitzel C(2011)Safe to the last instructionCommunications of the ACM10.1145/2043174.204319754:12(123-131)Online publication date: 1-Dec-2011
https://dl.acm.org/doi/10.1145/2043174.2043197
Klein G(2010)From a verified kernel towards verified systemsProceedings of the 8th Asian conference on Programming languages and systems10.5555/1947873.1947877(21-33)Online publication date: 28-Nov-2010
https://dl.acm.org/doi/10.5555/1947873.1947877
Yang JHawblitzel C(2010)Safe to the last instructionACM SIGPLAN Notices10.1145/1809028.180661045:6(99-110)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806610
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

Verification approach of metropolis design framework for embedded systems

Modeling and Verification of Reactive Systems using Rebeca

Specification and automated verification of concurrent software systems

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations