Table of Contents

1. Introduction

2. Installation

CBMC, SATABS, Eclipse plugin

3. CBMC – Bounded Model Checking

A Short Tutorial, Loop Unwinding, Test Suite Generation

4. SATABS – Predicate Abstraction with SAT

Introduction, Background, Tutorials

5. Modeling

Nondeterminism, Assumptions and Assertions, Pointers, Floating Point

6. Hardware/Software Co-Verification

Introduction, Tutorial, Mapping Variables, Synchronizing Inputs

7. Build Systems, Libraries and Instrumentation

Introduction, Integration into Build Systems with goto-cc, Visual Studio Builds, Variants of goto-cc, Architectural Settings, Property Instrumentation with goto-instrument, The CPROVER API Reference