Article

Logic Verification of ANSI-C Code with SPIN

Author:

Gerard J. HolzmannAuthors Info & Claims

Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification

Pages 131 - 147

Published: 30 August 2000 Publication History

Abstract

No abstract available.

Cited By

View all

Su WLiu YGanesan GHolzmann GSmolka SZadok EKuenning GShilane PWon Y(2021)Model-Checking Support for File System DevelopmentProceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3465332.3470878(103-110)Online publication date: 27-Jul-2021
https://dl.acm.org/doi/10.1145/3465332.3470878
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Chen JEbnenasir AKulkarni S(2014)The Complexity of Adding MultitoleranceACM Transactions on Autonomous and Adaptive Systems10.1145/26296649:3(1-33)Online publication date: 7-Oct-2014
https://dl.acm.org/doi/10.1145/2629664
Show More Cited By

Index Terms

Logic Verification of ANSI-C Code with SPIN
1. Theory of computation
  1. Logic

Recommendations

Object Code Verification
Formal verification of SystemC^FLspecifications using SPIN
MINO'06: Proceedings of the 5th WSEAS international conference on Microelectronics, nanoelectronics, optoelectronics

The formal language SystemC^FL is the formalization of SystemC. The language semantics of SystemC^FL was formally defined in a standard structured operational semantics (SOS) style. For verification purposes, in this paper, we present an approach to use ...
Verification-Preserving Inlining in Automatic Separation Logic Verifiers

Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification

August 2000

341 pages

ISBN:3540410309

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 30 August 2000

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 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Su WLiu YGanesan GHolzmann GSmolka SZadok EKuenning GShilane PWon Y(2021)Model-Checking Support for File System DevelopmentProceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3465332.3470878(103-110)Online publication date: 27-Jul-2021
https://dl.acm.org/doi/10.1145/3465332.3470878
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Chen JEbnenasir AKulkarni S(2014)The Complexity of Adding MultitoleranceACM Transactions on Autonomous and Adaptive Systems10.1145/26296649:3(1-33)Online publication date: 7-Oct-2014
https://dl.acm.org/doi/10.1145/2629664
Amani SChubb PDonaldson ALegg AOng KRyzhyk LZhu Y(2014)Automatic verification of active device driversACM SIGOPS Operating Systems Review10.1145/2626401.262642448:1(106-118)Online publication date: 15-May-2014
https://dl.acm.org/doi/10.1145/2626401.2626424
BjØrner DHavelund K(2014)40 Years of Formal MethodsProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_4(42-61)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_4
Mukherjee RMukherjee SDasgupta PGhosal SShroff GChandra SNagappan N(2013)Model checking of global power management strategies in software with temporal logic propertiesProceedings of the 6th India Software Engineering Conference10.1145/2442754.2442759(29-34)Online publication date: 21-Feb-2013
https://dl.acm.org/doi/10.1145/2442754.2442759
Ball TLevin VRajamani S(2011)A decade of software model checking with SLAMCommunications of the ACM10.1145/1965724.196574354:7(68-76)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1145/1965724.1965743
Nyström JEarle CThompson S(2009)Automatic assessment of failure recovery in Erlang applicationsProceedings of the 8th ACM SIGPLAN workshop on ERLANG10.1145/1596600.1596604(23-32)Online publication date: 5-Sep-2009
https://dl.acm.org/doi/10.1145/1596600.1596604
Vree AVlaovič BBrezočnik Z(2009)Sdl2pml - Tool for automated generation of Promela model from SDL specificationComputer Standards & Interfaces10.1016/j.csi.2008.09.00531:4(779-786)Online publication date: 1-Jun-2009
https://dl.acm.org/doi/10.1016/j.csi.2008.09.005
Holzmann GJoshi RGroce A(2008)Model driven code checkingAutomated Software Engineering10.1007/s10515-008-0033-915:3-4(283-297)Online publication date: 1-Dec-2008
https://dl.acm.org/doi/10.1007/s10515-008-0033-9
Show More Cited By

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

Index Terms

Recommendations

Object Code Verification

Formal verification of SystemCFLspecifications using SPIN

Verification-Preserving Inlining in Automatic Separation Logic Verifiers

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

Formal verification of SystemC^FLspecifications using SPIN