Index of modules

An abduction rule used in an abductive cyclic prover.

A cyclic abducer (cf.

List operations.

Given a BasicType build a module with several containers for it.

A list of term pairs.

A functorised list.

Combinators for manipulating functions.

This module implements imperative sets as hash tables.

Int BasicType with assorted containers.

A set of term pairs

A list-based set container.

Implementation of an LRU cache for memoising functions.

Functor putting together the different containers.

Create an ordered container.

Create functions for equality, comparison, hashing and printing for a pair of types.

Create an ordered map using a tree-based representation.

Create an ordered container whose underlying representation is a list.

Create an ordered container that behaves like a bag (add always increases size by one).

Given a type with comparison, equality and printing facilities, build the same facilities for lists of that type.

Implementation of an LRU cache for memoising functions whose arguments can be compared for equality and can be hashed.

Functor building an implementation of the hashtable structure.

This functor makes a mk_unifier function for a particular implementation of a container.

An ordered map with terms as keys.

A multiset container.

Functions for manipulating optional values.

A structure representing a set of constraints on ordinal-valued variables.

Operations on pairs.

A cyclic proof object.

A node in a cyclic proof.

A proofrule used by a cyclic prover.

A cyclic prover object.

Tactics for combining sequent-level rules.

An ordered set of terms.

Core module signatures used in Cyclist.

This module contains functions to answer various abduction questions for use in program verification.

Sets of disequalities over terms.

SL formula, basically a list of symbolic heaps, denoting their disjunction, along with a set of contraints on predicate ordinal labels (tags).

SL formula, basically a list of symbolic heaps, denoting their disjunction.

Symbolic heaps.

Symbolic heaps.

Inductive rule type consisting of a symbolic heap and a predicate head.

Predicate occurrences consisting of a predicate identifier and a list of terms as parameters.

Points-to atom, consisting of a pair of a term and a list of terms.

Multiset of points-tos.

A stack structure for prophecy variables.

SL sequent, as a pair of SL formulas.

Module providing SL term substitution-related functionality.

Module defining SL terms, which consist of variables (free or existentially quantified), or the constant nil.

An ordered pair of SL terms.

Tagged predicate, as a pair of an integer and a predicate.

Multiset of tagged predicates.

A union-find structure for SL terms.

This module specialises the generic Unification module to the SL instantiation of cyclist and provides extra functionality to support the unification of its various elements

Provides an abstract view of a proof as a graph and allows checking its soundness.

String BasicType with assorted containers.

Substitutions over terms

A set of tag pairs with a few convenience functions.

A set of tags.

A CTL temporal logic formula

An LTL temporal logic formula

An ordered map using the standard Map module.

An ordered container based on the standard Set module.

A library of types and combinators supporting continuation-passing-style unifiers

Signatures for containers and essential types.

Abstract type of variables

An abstract datatype for managing variables.