Table of contents

Library Scat.Examples

Examples of the report listed in the same order than in the report

Library Scat.BasicExamples

Tools for examples + basic tests

Library Scat.LoopsUnrolling

Unrolling of loops (trace partitioning)

Library Scat.NaiveAbstractionLib

Abstractions that are specific to "polyhedral" domain

Library Scat.NaiveGuardAbstractions

Naive context-dependent abstraction of guards

Library Scat.NaiveTermAbstractions

Naive context-dependent abstractions of concrete terms.

Library Scat.Certificate

An extensible language of certificate (through type certif below)

Library Scat.Concrete

Syntax and semantics of concrete programming language

Library Scat.Atoms

Syntax and semantics of atomic statements.

Library Scat.Assertions

Assertion language used in certificates.
- Environment of Assertions
- Abstract syntax of assertions

Library Scat.Conditions

Library Scat.Kernel

The kernel of our verifier: the abstract programming language

Library Scat.KernelVCG

VCG of kernel programs
- Frames of programs
- VCG code

Library Scat.KernelProof

Correctness of Kernel checker

Library Scat.Guassign

Technical stuff about conditions in order to support guassign

Library Scat.Renaming

Handling of variables (frames, renaming) for conditions

Library Scat.BoundedIteration

Library Scat.MiscUtils

This page has been generated by coqdoc