Constructor-based Inductive Theorem Prover (CITP)


CITP is a tool for proving inductive properties of software systems specified with constructor- based logics. CITP is implemented in Core Maude.


Download

CITP consists of one file citp.maude .


Instructions

In order to use CITP, copy citp.maude, start Maude and type in citp. See the following PDF for the list of commands available for CITP.


Examples


The followings are examples of specifications and proofs perfomed by CITP.


  1. PNAT

    Associativity and commutativity of addition.


  2. Parameterized lists with void elements


  3. FUN

    Demonstrates the strength of case analysis performed by CITP.


  4. Mutual Exclusion Protocol (QLOCK)

    Assume that many agents (or processes) are competting for a common equipment, but at any moment of time only one agent can use the equipment That is, the agents are mutually excluded in using the equipment. A protocol which can achieve the mutual exclusion is called "mutual exclusion protocol" (slides).


  5. Decoding Stream (DS)

    One agent puts repeatedly pairs < bit, d > of bits and encoded datas into a channel which automatically decode the information. When the agent gets < bit', d' > from the channel such that bit = bit', it is a confirmation that the data sent for decoding was received. In this case, the agent stores the data received into a list structure, alternates the bit, and selects the next encoded data for sending. We assume that the channel is unreliable, meaning that the data in the channel may be lost, but not exchanged or damaged.


  6. Alternating Bit Protocol (ABP)

    Alternating Bit Protocol (ABP) is a communication protocol that enables to send reliable messages on unreliable channels. Two processes, Sender and Receiver, that do not share any common memory use two channels to communicate with each other. Sender sends repeatedly a pair < bit1, pac > of a bit and a packet to the receiver over one of the channels, let's say channel1. When Sender gets bit1 from Receiver over the other channel, let's say channel2, it is a confirmation from Receiver that the packet sent was received. In this case Sender alternates bit1 and selects the next packet for sending. Receiver puts bit2 into channel2 repeatedly. When Receiver gets a pair < b, p > such that b is different from bit2 it stores p into a list and alternates bit2. Initially both channels are empty and the Sender's bit is different from the Receiver's bit. We assume that the channels are unreliable, meaning that the data in the channels may be lost, but not exchanged or damaged (snapshot).


  7. Spanning Tree

    Every connected graph has a spanning tree (slides).


  8. Cloud

    A cloud computing scenario (slides).

References


Back

daniel(domain of mail address: at jaist.ac.jp)