List operations.

This module implements imperative sets as hash tables.

Implementation of an LRU cache for memoising functions.

Core module signatures used in Cyclist.

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

A node in a cyclic proof.

A proofrule used by a cyclic prover.

A cyclic proof object.

A cyclic prover object.

Tactics for combining sequent-level rules.

An abduction rule used in an abductive cyclic prover.

A cyclic abducer (cf.

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

Signatures for containers and essential types.

A functorised list.

A multiset container.

A list-based set container.

An ordered map using the standard Map module.

Operations on pairs.

An ordered container based on the standard Set module.

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

String BasicType with assorted containers.

Int BasicType with assorted containers.

Combinators for manipulating functions.

Functions for manipulating optional values.

A set of tags.

A set of tag pairs with a few convenience functions.

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

An abstract datatype for managing variables.

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

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

Module providing SL term substitution-related functionality.

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

An ordered pair of SL terms.

A union-find structure for SL terms.

A stack structure for prophecy variables.

Sets of disequalities over terms.

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

Multiset of points-tos.

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

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

Multiset of tagged predicates.

Symbolic heaps.

Symbolic heaps.

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.

SL sequent, as a pair of SL formulas.

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

A CTL temporal logic formula

An LTL temporal logic formula