Logic verification of ANSI-C code with SPIN

DOI10.1007/10722468_8MaRDI QIDQ2753757zbMATH OpenFDO

Authors Gerard J. Holzmann

Publication date 6 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722468_8

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• Software model checking
• Software verification with BLAST

Cited in

(7)

• Syntax-directed model checking of sequential programs
• FORMAL VERIFICATION OF P SYSTEMS USING SPIN
• C Wolf -- A toolset for extracting models from C programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Learning of event-recording automata
• Network event recognition
• Verifying time partitioning in the DEOS scheduling kernel

Describes a project that uses

Uses Software

• Java PathFinder
• Bandera
• SPIN

This page was built for publication: Logic verification of ANSI-C code with SPIN

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753757)