Spin model checker the primer and reference manual

Semantics Engine. Three Examples. The Never Claim. Depth-First Search. Checking Safety Properties. Depth-Limited Search. Breath-First Search.

Checking Liveness Properties. Adding Fairness. Complexity Revisited. Partial Order Reduction. Statement Merging. State Compression.

Collapse Compression. The Minimized Automaton Representation. Bitstate Hashing. Bloom Filters. The Role of Abstraction. Embedded Assertions. A Framework for Abstraction. Soundness and Completeness. Selective Data Hiding. Bolder Abstractions.

Dealing with False Negatives. Thorny Issues with Embedded C Code. The Model Extraction Process. The Halting Problem Revisited. SPIN Structure. Random Simulation.

Interactive Simulation. Generating and Compiling a Verifier. Search Depth. Cycle Detection. Inspecting Error Traces. Internal State Numbers. Special Cases. Disabling Partial Order Reduction. Boosting Performance. Separate Compilation. Lowering Verification Complexity. Syntax Checking.

Property- Based Slicing. Simulation Parameters. Verification Parameters. The Automaton View Option. An Example. Types of Events. Defining Events. Matching a Timeline. Automata Definitions. Variations on a Theme. Timelines with One Event. Timelines with Multiple Events. General Approach. Keeping it Simple. Managing Complexity. Subscriber Model. Switch Model. Remote Switches. Adding Features.

Three-Way Calling. The Sieve of Eratosthenes. Process Scheduling. A Client-Server Model. A Square-Root Server. Adding Interaction. Adding Assertions. A Comment Filter. Grammar Rules. Meta Terms.

Control Flow Constructors. Basic Statements. Predefined Functions and Operators. Data References. Issues to Consider. Deferring File Inclusion. Manual Pages for Embedded C Code. Compile-Time Options. Postscript Generation. Model Checker Generation. LTL Conversion. Miscellaneous Options. Tuning Partial Order Reduction. Increasing Speed. Decreasing Memory Use. Debugging PAN Verifiers. Experimental Options. Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source code.

Learn algorithms for solving classic computer science problems with this concise guide covering everything from fundamental …. Modern C introduces you to modern day C programming, emphasizing the unique and new features of …. Skip to main content. Start your free trial. Book description Master SPIN, the breakthrough tool for improving software reliability SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs.

Show and hide more. Table of contents Product information.