Specification and Verification ofInvariant Properties of Transition Systems
Daniel Găină

Ionuţ Ţuţu

Adrián Riesco

Kyushu University
Fukuoka, JapanLa Trobe University
Melbourne, Australia
Email: daniel@imi.kyushu-u.ac.jp

Simion Stoilow Institute of Mathematics of
the Romanian Academy, Bucharest, Romania
Royal Holloway University of London
Egham, United Kingdom
Email: ittutu@gmail.com

Complutense Universityof Madrid
Madrid, Spain
Email: ariesco@fdi.ucm.es

Abstract—Transition systems provide a natural way to specify
and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper
advances a verification method for transition systems whose
reachable states are described explicitly by membership axioms.
The proof technique is implemented in the Constructor-based
Inductive Theorem Prover (CITP), a proof management tool built
on top of a variation of conditional equational logic enhancedwith many modern features. This approach complements the socalled OTS method, a verification procedure for observationaltransition systems that is already implemented in CITP.
Index Terms—algebraic specification; theorem proving; term
rewriting; transition systems

I. I NTRODUCTION

be ordered, while the second is a membership condition that
requires the rest of the list to be ordered as well.
In this paper, we propose a formal method for analysing
transition systems whose reachable states are described explicitly by membership axioms. The specification and verification
technique is supported by the Constructor-based Inductive
Theorem Prover (CITP) [14], which is implemented in Maude
by using its meta-level – a reflective feature of Maude thatallows specifiers to use modules and terms at the object levelin a consistent way. The formal language of CITP is based on avariation of conditional equational logic with subsort relations,membership axioms, transitions, and constructor operators [12].
All this, combined with the efficient implementation of rewriting modulo axioms, makes Maude suitable for implementing
CITP and for using its notation to define specifications.
The methodology described herein complements the one
already supported by CITP [13] for analysing invariant properties of Observational Transition Systems (OTS) [21]. For the
OTS method, the system states are regarded as ‘black-boxes’,
and are distinguished only by observational functions. Thisapproach was originally developed with the support of the
CafeOBJ language. In OTS, one principal sort/type stands
for the system, and the effects of transitions are obtained byobserving – via functions – how the features of the systemchange with respect to the constructors of the principal sort.

Transition systems describe the behaviour of systems bymeans of states (which give a structural view of the system at
a given time) and the possible transitions between them (which
capture system dynamics). This simple approach allows those
who specify concrete systems to abstract the implementation
details and to focus instead on the high-level features that are
critical for the correct functioning of the system. A prominent
approach to modelling and reasoning about transition systems
is the one based on rewriting logic [17]. This is a formalismof change, where the transitions between states correspond to
rewrite rules, and where the static behaviour of the system is
specified in a variant of equational logic [8]. The variationsof rewriting logic that are relevant to the present study are C ONTRIBUTIONS . The contributions w.r.t. the methodology
supported by CITP can be classified into two main categories.
implemented in Maude [4] and CafeOBJ [5].
1) Induction scheme: To prove properties of infinite-state
Maude implements rewriting based on membership equatransition
systems, we need finite strategies for covering thetional logic [18], which extends many-sorted equational logic
infinitestate
space. By finite strategies we mean proof ruleswith membership axioms. The expressiveness of such axioms
withafinitenumberof hypotheses for inductive reasoning. In
is illustrated by the specification of ordered lists, which cannot
1thepresent
methodology,
each state is described by a collection
be defined using plain many-sorted equational logic. In the
of
all
data
types
involvedin the behaviour of the system. This
short example below, we use a conditional membership axiom
isachievedthroughthedefinitionof a ‘mixfix’ operation:
to state that a list with at least two elements is ordered:
cmb N N’ L : OList if N ≤ N’ ∧ N’ L : OList .

In this case, lists are constructed simply by juxtaposition,
and OList < List is the subsort of ordered lists; the first
condition indicates that the first two elements of the list must
1 They can be defined using predicates, but not as a subsort of all lists.

op [_,...,_]: DataType1 ... DataTypeN → Sys .

The transition system has a finite non-empty set of initial states;
in many cases, that set is a singleton. The issue is that not allcollections of elements [d1,...,dn], where di is an elementof sort DataTypei, are reachable from initial states. In orderto perform inductive reasoning on reachable states, or to defineproperties that hold for all reachable states, we need a subsort
Reach < Sys. In algebraic specification, the (sub)sorts canbe described only by operations or membership axioms. For
example, in the OTS method, the reachable states are describedusing constructor operations. In the present contribution, thereachable states are described by conditional membership axioms of the form cmb t1 : Reach if t2 : Reach, wheret1 and t2 are terms of sort Sys (with universally quantified
variables). These axioms play the role of constructors for thesimultaneous induction scheme implemented in CITP.
2) Automated reasoning: The present methodology enjoys
an increased level of automation due to the term-rewriting
modulo associativity and/or commutativity supported by Maude.
Our proof technique is intimately linked to the structure ofsentences and takes advantage not only of the operational, butalso of the denotational semantics of specifications in orderto improve the users’ interaction with the tool. Therefore, thepresent formal method is equipped with both:a) general tactics derived from the proof rules of the calculusof the underlying logic of CITP [12], which are soundfor all specifications (see Figure 1),b) specialized tactics derived from the proof rules for thedata types declared with initial-algebra semantics suchas Booleans or sequences; those rules are sound only
if the initial data types are protected, meaning that no“junk” (new elements) and no “confusion” (identification ofexisting elements) are added to the initial data types [19].
We argue on concrete examples of formal verification thatthe combination of the above tactics eases greatly the users’burden in discharging proof obligations. Algebraic-specification
languages have libraries for defining the initial data types thatare often used in specifying systems; examples include the
Booleans, natural numbers, associative lists (or sequences), andsets. Due to Gödel’s incompleteness theorem, the properties of
initial data types are usually not recursively enumerable, whichmeans that the general tactics are not sufficient for discharging
properties that involve initial data types. For this reason, we
need specialized tactics to complement the general ones inorder to perform proofs in a more natural and efficient way.
To the best of our knowledge, this combination of tactics is
unique in the formal-methods literature.

Light, HOL4; cf. [24]), they require trained users to direct theprover towards discharging goals which cannot be proved byautomatic techniques. In many cases, the tool needs the users’
help to perform even trivial proofs. The new induction schemeand the decision procedures pointed out above, as well as the
improvements in the interface, try to alleviate this problem,
passing the computational burden to the machine and allowing
the user to focus on the overall proof strategy.
S TRUCTURE OF THE PAPER . Section II presents the basic notions used in the paper. Section III deals with the methodologythat the tool follows, and illustrates the verification of theAlternating Bit Protocol. Section IV discusses related work;
and Section V concludes and outlines a few lines of future
research. The tool is available on the first author’s web page [9].
II. P RELIMINARIESIn what follows, by specification we mean a text that
describes a signature (roughly, a collection of sorts andsymbols), a set of possibly conditional sentences (built using
those symbols) and a class of models (that assign meaning
to the symbols). The sentences are Horn clauses of the form(∀X) ∧ H ⇒ C, where H ∪ {C} is a set of atomic formulas
given as equations t1 = t2 , membership axioms t : s, ortransitions t1 ⇒ t2 , where t, t1 , and t2 are terms and s is asort. Such sentences also define the operational semantics ofthe specification, because they form a term-rewriting systemthat makes the specification executable by rewriting. Moreover,they are compatible with the denotational semantics of thespecification (its class of models), in the sense that every
model of the specification satisfies its sentences.
A goal is a pair hSP ` Ei, where SP is a specification and E
is a set of formulas to prove. A proof rule is a mapping froma goal hSP ` Ei to a list of goals hSP1 ` E1 i . . . hSPn ` En i.
The tactics are obtained by canonically extending proof rules
to mappings from lists of goals to lists of goals. In the current
version of CITP, the user can give commands which may
consist of lists of tactics rather than a single tactic. It follows
that the proof scripts consist of sequences of lists of tactics
instead of trees (whose nodes would be goals, and whose edges
would be lists of tactics). This has the advantage of simplifying
the design of the tool interface and increasing the automation
N EW FEATURES . Compared to the first version of CITP, the level of the proof process by making all goals to be discharged
new features implemented in the tool are:available to the user simultaneously. However, if the user wants• an induction scheme based on constructors given as
to apply a tactic list tctList only to the current goal, then themembership axioms;
command (. tctList) can be issued to the tool. In addition,• a tactic for computing and joining critical pairs, i.e. for(select no) can be used to move the goal no to the top ofpairs of terms resulting from overlapping rewrite rules;
the goal list, thus making it the current goal.
• improved decision procedures for automated reasoning,
Apart from tactics, CITP is equipped with commands for• a new interface designed to improve the users’ interaction,
managing the proof process, which have no effect on the list
and implemented from scratch in Core Maude;of goals to be proven (see Figure 2), but enable the user to• the command-parsing component of the interface washave a better control and understanding of the actual proof.
upgraded to generate better error messages.
Assume that the initial goal is a pair hSP ` γi given
V by aMost of the improvements presented in this paper focus on specification SP and a single sentence γ of the form (∀X) H ⇒reducing the user interaction. In fact, since inductive theorem C, where X is a set of variables and H ∪ {C} is a set of atomic
provers are oftentimes interactive (e.g. Isabelle, Coq, HOL formulas. The idea is to develop tactics that decompose γ into

TACTICA BBREVIATION

Induction
Induction based on mb. ax.
Case analysis
Theorem of constants
Implication
Reduction
Initialization
Critical-pairs left
Critical-pairs right(ind on varList)(indx on varList)
(ca)
(tc)
(imp)
(red)
(init sentence by substitution)(cp-l sentence1 >< sentence2)(cp-r sentence1 >< sentence2)

SelectDot(select no)(. tctList)

Fig. 1: General tactics
C OMMAND

D ESCRIPTION(rollback)returns the proof process to the state
before applying the last list of tactics
displays the goals to discharge
shows the sequence of lists of tactics
applied so far
reduces the term t to its normal form w.r.t.
the specification of the current goal

(show goals)(show proof)(redTerm t)

Fig. 2: CITP commands

numbers, but without marking it as a constructor. Finally, wedefine the behaviour of addition by means of equations (eq),where the metadata attribute allows the users to provide
additional information to the tool, as we will see later.
fmod PNAT issorts PNat PNzNat .
subsorts PNzNat < PNat .
op 0 : → PNat
op s_ : PNat → PNzNat[ctor].
[ctor].

op _+_ : PNat PNat → PNat .
vars M N : PNat .
eq 0 + N = N[metadata "1"].
eq s M + N = s(M + N)
[metadata "2"].
endfm

Since the above specification starts with fmod and ends with
endfm, its semantics is initial, meaning that the class of models
Mod(PNAT) of the specification PNAT consists of all models
that are isomorphic with the model of natural numbers.
Suppose one wants to prove the associativity of addition.
The goal is introduced by the following command:(goal PNAT ` eq (X:PNat + Y:PNat)+ Z:PNat =X:PNat + (Y:PNat + Z:PNat);)

The variable X is chosen for induction and the tactic(ind on X:PNat) is applied. The tool then generates two
subgoals, one for each constructor: zero (0) and successor (s_).
By the theorem of constants (tc), the variables Y and Z aresimpler, basic constituents, e.g. equational formulas, which
can be discharged using term rewriting. There are two tactics introduced as constants to the specifications in the subgoals
designed to eliminate universal quantification: induction and generated by induction. Since logical implication does not occur
the theorem of constants. While the latter is applicable to in any of the formulas to prove, the goals can be discharged by
all variables in X, the former can eliminate only variables of reduction (red), which replaces each term in the equations
constrained sort.2 It is the users’ responsibility to separate to prove with its normal form. The proof of associativity thus
variables of constrained sorts, which will be dealt with by consists of the tactic list (ind on X:PNat tc red). See [9]induction, from the rest of the variables, which will be handled for a detailed presentation of the proof.
by the theorem of constants. Typically, induction is applied first
In the case of large specifications, it is undesirable to display
and then the theorem of constants comes into play. The goals all their sentences during the proof process. Therefore, only
hSP1 ` γ1 i . . . hSPn ` γn i obtained by applying induction and sentences with the attribute metadata "n" will be displayed,
the theorem of constants
V have only quantifier-free formulas, where n is a natural number. The axioms introduced in thei.e. γi is of the form Hi ⇒ Ci for all i ∈ {1, . . . , n}. The proof process will be assigned automatically a natural number
tactic (imp) is designed to eliminate the logical implication. as an attribute, and therefore will always be displayed.
For example, by applying implication to a goal hSPi ` γi i
Example 2: Consider the following specification of two
as above, the result is hSPi + Hi ` Ci i, where SPi + Hi is thefunctions on natural numbers:3
specification obtained from SPi by adding the axioms in Hi .
The goals hSPi + Hi ` Ci i are discharged using term rewriting. fmod FG-FUN is
Example 1: Consider the following specification of natural
numbers with addition. We first define sorts and subsort relations using the keywords sorts and subsorts, respectively.
This allows us to define Peano natural numbers (PNat) andnon-zero Peano natural numbers (PNzNat). We can then define
operations on these sorts using the keywords op; some of these
operations are constructors (ctor), such as 0 and successor,
s_, where the underscore is a placeholder. In the same way,
we define an operation symbol _+_ for the addition of natural
2 We distinguish between constrained sorts, which have constructors
explicitly described in the signature, and loose sorts, with no such constructors.

protecting NAT .
op F : Nat → Nat .
op G : Nat → Nat .
vars X Y : Nat .

ceq F(X) = 5 if X ≤ 7 [metadata "CA-1"].
ceq F(X) = 1 if 8 ≤ X [metadata "CA-2"].
ceq G(Y) = 2 if Y ≤ 4 [metadata "CA-a"].
ceq G(Y) = 7 if 5 ≤ Y [metadata "CA-b"].
endfm
3 To benefit from the usual, decimal representation of natural numbers, we
import the predefined Maude module NAT instead of PNAT from Example 1.

The purpose of this example is to show that in formal
verification one can easily reach subgoals that have inconsistentspecifications, despite the fact that the proof started with agoal whose underlying specification is consistent, so we can
automatically discharge the corresponding subgoal. Note that:1) either X ≤ 7 or 8 ≤ X, for all natural numbers X, and2) the left-hand sides of the conditional equations labelledwith CA-1 and CA-2 are equal.
Therefore, the conditional equations labelled with CA-1 andCA-2 should be regarded as one sentence. The labels CA-1
and CA-2 are used by CITP to perform case analysis. Thistactic is sound if and only if:1) the conditions of CA-1 and CA-2 are disjointly true, and2) the left-hand sides of CA-1 and CA-2 are equal.
A similar remark holds for the sentences labelled with CA-aand CA-b. The goal we are interested in is the following:3) h FG-FUN + {op X#1 : → Nat,eq 8 ≤ X#1,
eq X#1 ≤ 4}`
eq 9 ≤ G(F(X#1:Nat))+ G(X#1:Nat)= true ; i4) h FG-FUN + {op X#1 : → Nat,eq 8 ≤ X#1,
eq 5 ≤ X#1}`
eq 9 ≤ G(F(X#1:Nat))+ G(X#1:Nat)= true ; iNote that the specification of the third goal above is inconsistent
as we cannot have a natural number X#1 that is greater thanor equal to 8 and less than or equal to 4. Formally, since
the specification NAT is imported in protecting mode, no
new elements of sort Nat are introduced, and none of theexisting elements can be made equal (say, by equations);
this implies that X#1 is a natural number; also, the preorder(goal FG-FUN
relation ≤ is interpreted in the obvious way; it follows that` eq 9 ≤ G(F(X:Nat))+ G(X:Nat)= true ;)the equations {eq 8 ≤ X#1, eq X#1 ≤ 4} create confusion
By the theorem of constants (tc), the variable X:Nat is added w.r.t. the initiality of NAT as there is no natural number (into the body of the specification FG-FUN as a fresh constant. place of X#1) satisfying both equations. CITP recognizes thiscontradiction and discharges the third goal automatically.
The new goal is the following:
The remaining three goals are discharged by the reductionh FG-FUN + {op X#1 : → Nat}tactic (red). Therefore, the proof of the goal
` eq 9 ≤ G(F(X#1))+ G(X#1)= true ; i
In order to apply case analysis (ca), the tool selects theground term 9 ≤ G(F(X#1))+ G(X#1) from the formula toprove eq 9 ≤ G(F(X#1))+ G(X#1)= true. Note that:
1) CA-1 and CA-2 match the subterm G(F(X#1)) of
the term 9 ≤ G(F(X#1))+ G(X#1) via the substitution
X:Nat ← X#1, and there are no proper subterms of
G(F(X#1)) that can be matched by any CA-axioms;
2) CA-a and CA-b match the subterm G(X#1) of theterm 9 ≤ G(F(X#1))+ G(X#1) via the substitution
Y:Nat ← X#1, and there are no proper subterms of
G(X#1) that can be matched by any CA-axioms.
Case analysis splits the goal above into four subgoals byadding to the specification FG-FUN + {op X#1 : → Nat}
one condition from each of the two groups of sentences below:(goal FG-FUN `eq 9 ≤ G(F(X:Nat))+ G(X:Nat)= true ;)consists of the list of tactics (tc ca red); see [9] for the full
specification and proof script. Here it is also worth noting thatcase analysis (ca) plays an essential role in the OTS method;see [13] for a formalization of (ca) and its applications.
III. F ORMAL METHOD

The new list of goals is as follows:

The verification method described in Example 1 forms thebasis for two main directions through which one can proveinvariant properties of transition systems:
1) One technique is designed for OTS, where the structure of
the states is not accessible to the users; instead, the states
are distinguished by so-called observation functions [13].
2) The other approach is built for transition systems whosestates are described explicitly using membership equations.
Clearly, the two methods share common tactics like the theoremof constants, implication, or reduction. The implementation of
the tool is modular in that regard, allowing users to reuse thecode of the shared tactics. In this paper, we focus on the lattermethodology; cf. [13], which deals with the former.

1) h FG-FUN + {op X#1 : → Nat,

A. Alternating Bit Protocol

1) ceq F(X#1) = 5 if X#1 ≤ 7 .
ceq F(X#1) = 1 if 8 ≤ X#1 .
2) ceq G(X#1) = 2 if X#1 ≤ 4 .
ceq G(X#1) = 7 if 5 ≤ X#1 .

eq X#1 ≤ 7,
eq X#1 ≤ 4}`
eq 9 ≤ G(F(X#1:Nat))+ G(X#1:Nat)= true ; i2) h FG-FUN + {op X#1 : → Nat,eq X#1 ≤ 7,
eq 5 ≤ X#1}`
eq 9 ≤ G(F(X#1:Nat))+ G(X#1:Nat)= true ; i

The specification and verification methodology supported by
the tool is presented through a case study. The example chosen
is of the Alternating Bit Protocol (ABP), a protocol operating
at the data-link layer of networks that ensures the reliability of
the communication between a sender and a receiver [1]. The
overall structure of the ABP is illustrated in Figure 3.
The protocol consists of two processes, Sender and Receiver,each having a data buffer and a one-bit state. Sender andcmb [B1,N,( h B1,pac(N) i ,Ch1),B2,D,Ch2]: Reachif [B1,N,Ch1,B2,D,Ch2]: Reach[metadata "ctor-send1"].

data channel

Sender

data

bit

data

bit

Receiveracknowledgement channel

Fig. 3: The Alternating Bit Protocol

3) Receiver writes its current bit B2 to the acknowledgement
channel Ch2.
cmb [B1,N,Ch1,B2,D,(B2,Ch2)]: Reachif [B1,N,Ch1,B2,D,Ch2]: Reach[metadata "ctor-send2"].

4) Sender acknowledges that the package has been delivered
Receiver use channels to communicate with each other, as they
when its bit B1 is the last bit of the acknowledgement
do not share any common memory: (a) a data channel fromchannel (Ch2,B1).5 It immediately flips its bit B1 andSender to Receiver for sending bit-packet pairs, and (b) an
updates the number N of the packet to be transmitted.
acknowledgement channel from Receiver to Sender for sending
cmb [not B1,s N,Ch1,B2,D,Ch2]: Reachsingle confirmation bits. The protocol works as follows:
if [B1,N,Ch1,B2,D,(Ch2,B1)]: Reach• Initially both channels are empty and Sender’s bit is different[metadata "ctor-rec1"].
from Receiver’s bit.
5) Receiver gets a new packet P and stores it in the packet list D• Sender repeatedly writes bit-packet pairs hbit, paci on thewhen the last bit B2 from the data channel Ch1, h B2,P idata channel, where bit is the Sender’s bit and pac is theis different from its own bit (not B2).
Sender’s data to transmit. If the Sender reads bit fromcmb [B1,N,Ch1,B2,(P,D),Ch2]: Reach
Receiver over the acknowledgement channel, then it is aif [B1,N,(Ch1, h B2,P i ),not B2,D,Ch2]: Reachconfirmation that the packet has been delivered. In that case,[metadata "ctor-rec2"].
Sender flips its bit and selects the next packet to send.
• Receiver writes its bit on the acknowledgement channel
6) The data channel is not reliable: at any time, any element
repeatedly. When it reads a pair hbit, paci such that bit isof the channel (from an arbitrary position) might be lost.
different from its bit, it stores the package and flips its bit.
cmb [B1,N,(Ch1,Cn1),B2,D,Ch2]: Reach
B. Specification

if [B1,N,(Ch1,BP,Cn1),B2,D,Ch2]: Reach[metadata "ctor-drop1" nonexec].

This section gives an overview of the ABP specification. The
complete specification can be found in [10]. The state space is
explicitly described by tuples that consist of all the data types
that define the protocol. Here, the state space is represented
by the sort Sys, which has only one constructor:

7) Dropping one element from the acknowledgement channel
is modelled similarly to item 6 above.
8) In addition to losing data, the elements of the data channel(once again, from arbitrary positions) can also be duplicated.

sorts Reach Sys . subsort Reach < Sys .
op [_,_,_,_,_,_] : Bit PNat Channel1
Bit Data Channel2 → Sys [ctor].

cmb [B1,N,(Ch1,BP,BP,Cn1),B2,D,Ch2]: Reachif [B1,N,(Ch1,BP,Cn1),B2,D,Ch2]: Reach[metadata "ctor-dup1" nonexec].

The first two arguments are the Sender’s bit and packet, which,for simplicity, we identify by a natural number; Channel1
corresponds to the data channel; the arguments four and five
are the Receiver’s bit and packet list, respectively; Channel2
corresponds to the acknowledgement channel. As explainedin Section I, all terms built using this constructor have thesort Sys; but when reasoning about the ABP, we are actuallyinterested in the subset of terms that denote reachable states(i.e. states of sort Reach4 ). Hence, the strategy is to use
membership axioms in order to define these particular terms:
1) In the initial state, Sender’s bit is true, the packet number is0, and both communication channels are empty, Receiver’s
bit is false, and Receiver’s packet list is empty.

9) Duplication in the acknowledgement channel is modelledsimilarly to item 8 above.
The constructors of a given sort can be either functions or
membership axioms. In this case, the sort Reach is described by
the nine membership axioms listed above. The prefixes ctorfrom the metadata attributes, e.g. ctor-init or ctor-send1,
are necessary for the tool to recognize that these membershipaxioms are constructors for Reach, and to generate appropriate
induction schemes for formal verification.
The specification ABP obtained in this way [10] can be enhanced with transitions rl T1 ⇒ T2 [metadata "trans"]for each conditional membership axiom cmb T2 : Reach if
T1 : Reach [metadata "ctor-trans"]. For example,
the corresponding transition for the conditional membershipaxiom ctor-send1 would be:

mb [t,0,empty,f,empty,empty]: Reach[metadata "ctor-init"].

2) Sender writes the current bit-packet pair h B1,pac(N) ito the data channel Ch1.
4 Sys and Reach are the standard names for such sorts. However, they are
not predefined; users can use any other names they consider to be suitable.

rl [B1,N,Ch1,B2,D,Ch2] ⇒[B1,N,( h B1,pac(N) i ,Ch1),B2,D,Ch2][metadata "send1"].
5 Notice the convenience of using the associative list-concatenation operation(and pattern matching) instead of the left-associative append operation.

This makes it possible to apply model-checking techniques
which states that, if the Receiver’s bit is equal tofor formal verification. However, model checking is outside
Sender’s bit, B1, then all the bits in the data chanthe scope of this paper. It is worth pointing out though thatnel are equal to B1. Notice that inv2 is not a termconditional membership axioms and transitions are in one-torewriting rule, because there are variables in the condione correspondence. Because of this, one may be tempted totion [B1,N,(Ch1, h B,P i ,Cn1),B1,D,Ch2]: Reacheliminate membership axioms and keep only the transitions.
such as N that do not occur in the left-hand side of theBut, denotationally, in the absence of membership axioms,
rule. This is the reason for using the attribute nonexec.
there are no terms of sort Reach, and one cannot formalize
The operational semantics of a specification is therefore
invariant properties that hold for all reachable states. Moreover,given by all sentences of the specification that do not havetransitions such as send1 do not play any role in the deductive
the attribute nonexec. After applying the tactic list
verification described in the following section, hence our(indx on varList red cs red tc red imp red)
methodological preference for membership axioms.
one may need to initialize non-executable sentences inIn the present contribution, dropping elements from arbitraryorder to complete the verification process. According
positions in the communication channels is modelled faithfully.
to our experience, the tactic list above followed by theThis is possible thanks to (a) the matching equations provided
initialization of such sentences and the joining of criticalby Maude for the conditions of the Horn sentences, and (b) thepairs is sufficient for completing the verification process.
support for the associative data types that are used to describe
the communication channels. The formal verification involving
The proof strategy for proving the properties of the specification
the matching of associative data types is facilitated by the tactic
ABP consists in the following sequence of tactic lists:(cs) – case analysis for sequences and sets [13] – which breaks(indx on varList red cs red tc red imp red)a goal into subcases that are easier to analyse.
C. Formal verification
The methodology described in Section II is developed further
in order to support the verification of safety properties fortransition systems whose states are described explicitly. For
that purpose, the new features added to the proof strategy
presented in Section II can be summarized as follows:• Induction is replaced by a simultaneous induction scheme(indx on varList) based on constructors given as membership axioms, where varList is a list of variables.
• In order to preserve the confluence property, after eachapplication of a tactic it is necessary to reduce to thenormal form each term occurring in the formulas to prove.
This is achieved by applying the tactic (red).
• In addition, it is often necessary to apply case analysis(cs) on the sequence data type. In our case study, thisinitial data type models the communication channels. Thistactic is applied after induction. So far, the verification
strategy consists of the following tactic list:(indx on varList red cs red tc red imp red)

However, that alone is not sufficient for discharging all
the goals generated by the induction scheme.
• Even if the specification of the initial goal is confluent,
after applying the tactic list above, some specifications of
the goals generated by the verification strategy proposed
may lose the confluence property. For this purpose, wehave developed tactics for joining critical pairs:(cp-l sentence1 >< sentence2), and(cp-r sentence1 >< sentence2).
•

Last but not least, extra care is needed for proving formulasthat are not term-rewriting rules. Consider the invariant:ceq B = B1
if [B1,N,(Ch1, h B,P i ,Cn1),B1,D,Ch2]: Reach[metadata "inv2" nonexec].

(cp-l sentence1 >< sentence2 red)
(init sentence by substitution red)

Most of the tactics in the above proof strategy were definedfor the OTS method [13]. The new tactics implemented forthe present verification method are the simultaneous induction
scheme based on constructors given as membership axioms(indx on varList) and the joining of critical pairs (cp-lsentence1><sentence2) and (cp-r sentence1><sentence2).
We employ the above strategy to prove that the ABP
specification satisfies the following safety property: all thepackets sent are received in the same order in which they weresent. This property is formalized by the two sentences below.
ceq mk(N)= D if [B,N,Ch1,B,D,Ch2]:= S[metadata "goal1"].
ceq mk(N)= pac(N),D if[B,N,Ch1,not B,D,Ch2]:= S[metadata "goal2"].

Here, the function mk : PNat → Data is defined by two
equations: (a) eq mk(0) = pac(0) and (b) eq mk(s N) =pac(s N) mk(N). That is, for every natural number N, mk(N)is the list of packets that correspond to the natural numbers N,
N-1, . . . , 0. The sentence goal1 states that, if Sender’s bit isequal to Receiver’s bit, then N packets delivered were received
in the same order in which they were sent. The sentence goal2
states that, if Sender’s bit is different from Receiver’s bit, thenthe last packet delivered was not received.
In order to prove the two goals described above, we need fivelemmas. The first four are proved by simultaneous induction,
while the fifth lemma is derived from the others. The proofs ofthese lemmas are similar to the proofs of goal1 and goal2.
Because of this, we focus only on proving the two goals. Moreinformation about the lemmas can be found at [10].
I NDUCTION . After applying (indx on S:Reach) to goal1
and goal2, the tool generates nine subgoals, each subgoalcorresponding to one of the nine constructors. Ifcmb T2 : Reach if T1 : Reach[metadata "ctor-trans"].

is one of the constructors, then the corresponding subgoal ish ABP + {mb T1 : Reach [metadata "trans"],
goal1(S ← T1) [metadata "trans"],goal2(S ← T1) [metadata "trans"]}` {goal1(S ← T2),goal2(S ← T2)} i

solid background in algebraic specification allows one tocombine general tactics that are sound for all specifications
with specialized tactics that are sound for initial data types –and often used in practice to increase the performance of theverification method. This is one example of decision procedurethat increases the automation level of the current methodology.
All nine subgoals can be handled in this manner.

The underlying specification of the subgoal above is obtained C ONTRADICTION . Since there are no matching equations
involving sequences in the goals obtained after the applicationfrom ABP by adding:of (indx on S:Reach), the tactic (cs) just splits each1) the variables in ctor-trans as constants,
goal into two subgoals. Therefore, the result is a list of2) the membership axiom mb T1 : Reach, andeighteen subgoals. For example, the subgoals corresponding to3) the induction hypothesis
ctor-init are as follows:{goal1(S ← T1), goal2(S ← T1)}.
The label trans is for the user to recognize the induction case h ABP ` ceq pac(0)= empty if t := f[metadata "goal1"]; ito prove. There are nine subgoals, and each subgoal has two
h
ABP
`
ceq
pac(0)=
pac(0)
if nilformulas to prove. This means eighteen cases to discharge.
[metadata "goal2"]; i
CITP performs several other transformations; all are soundw.r.t. the semantics and help the user discharge the goals easier. The tactic (tc) has no effect on the eighteen goals, because
Take, for example, the subgoal corresponding to ctor-init: there are no variables in the formulas to prove. The tactich ABP `
(imp) adds the conditions of the formulas to the specification.
{ceq mk(N) = D
For example, the goals corresponding to init become:if [B,N,Ch1,B,D,Ch2]:=[t,0,empty,f,empty,empty][metadata "goal1"];
ceq mk(N) = pac(N),D
if [B,N,Ch1,not B,D,Ch2] :=[t,0,empty,f,empty,empty][metadata "goal2"];} i

Based on the initiality of tuples, the goal is refined into:h ABP `
{ceq mk(N) = D
if B := t ∧ N := 0 ∧ Ch1 := empty∧ B := f ∧ D := empty∧ Ch2 := empty[metadata "goal1"];
ceq mk(N) = pac(N),D
if B := t ∧ N := 0
∧ not B = f ∧ D := empty∧ Ch2 := empty[metadata "goal2"];} i

For each matching equation V := T in the condition, where
V is a variable and T is term, the tool transforms the goalby removing the matching equation and substituting the term
T for the variable V in the formula to prove. This procedure
is performed sequentially for all matching equations V := T,from left to right. Then all terms are reduced to their normal
forms. The user can see only the final result:h ABP `
{ceq pac(0)= empty if t := f[metadata "goal1"];
ceq pac(0)= pac(0) if nil[metadata "goal2"];} iThis splitting of conditions based on tuple matching, andfollowed by the application of substitutions V ← T, andthen by reductions to normal forms are integrated into thetactic (indx on S:Reach) to ease the user’s task. It avoids
complicated proofs of obvious properties. We argue that a

h ABP + {eq f = t} ` eq pac(0)= empty[metadata "goal1"]; ih ABP ` eq pac(0)= pac(0)[metadata "goal2"]; i

Since the second goal is a tautology, it is discharged automatically by the tool. We thus focus only on the first goal. For
that purpose, we start with the specification of bits:
fmod BIT issort Bit .
op f : → Bit [ctor].
op t : → Bit [ctor].
op not_ : Bit → Bit .
eq not f = t .
eq not t = f .
ceq true = false if t = f[metadata "contradict"].
endfm

The specification BIT is declared with initial semantics andit is imported in the specification ABP in protecting mode.
This means that there are exactly two (distinct) values for thebits, t and f. The addition of eq f = t to ABP gives rise to aninconsistency. From a model-theoretic point of view, the classof models of the specification ABP + {eq f = t} is empty.
It follows that ABP + {eq f = t} entails any formula. In
particular, ABP + {eq f = t} entails eq pac(0)= empty.
But the only inconsistency recognized by CITP is on the sort
Bool. In other words, if CITP can proveh ABP + {eq f = t} ` eq true = false ; ithen the goalh ABP + {eq f = t} ` eq pac(0) = empty ; iis discharged. Here, the conditional equation contradictfrom the specification BIT comes into play. This conditional

equation states that any inconsistency created on the sort Bit
will determine an inconsistency on the sort Bool. Notice that
contradict has no role in the denotational semantics of thespecification BIT. It is used by the tool to discharge goals withspecifications that satisfy sentences in contradiction with theinitial semantics. It follows that CITP discharges the goal[B1#1,N#2,Ch1#3,B2#4,D#5,(Ch2#6,B1#1)](indx on S:Reach red cs red tc red imp red)

ceq B2 = B1
if [B1,N,Ch1,B2,D,(Ch2,B1,Cn2)]: Reach[nonexec metadata "inv3"].

where:
1) B1#1 is a Bit-constant representing Sender’s bit,2) N#2 is a natural number representing the index of the next
packet to be delivered by Sender,
3) Ch#3 is a Channel1-constant for the data channel,h ABP + {eq f = t} ` eq pac(0) = empty ; i4) B2#4 is a Bit-constant representing Receiver’s bit,5) D#5 is a Data-constant for packets delivered to Receiver,
because the specification ABP + {eq f = t} trivially entails
6) Ch2#6 is a constant of sort Channel2 such thatthe equation eq f = t, which is in contradiction with the(Ch2#6,B1#1)represents the acknowledgement channel.
initiality of the specification BIT. This tactic may look strange
for engineers with no training in the theory of algebraic By the membership axiom 1, the last bit of the acknowledgespecification; but in practice it often happens to reach subgoals ment channel is equal to Sender’s bit. By the equation 4, thewith inconsistent specifications (see Example 2); the approach Sender’s bit B1#1 is different from the Receiver’s bit B2#4.
described above is simple and efficient in such situations.
The third lemma in [10], labelled inv3 below, states that,iftheacknowledgement channel contains a bit that is equal to
C RITICAL PAIRS . What we have presented above is only one
Sender’sbit, then the Receiver’s bit is also equal to Sender’spart of the proof corresponding to the constructor ctor-init.
bit,
which
is a contradiction with the equation 4.
By applying the tactic list
to goal1 and goal2, the simultaneous induction scheme
generates nine goals – expanded to eighteen subgoals, as eachof the nine goals contains two formulas. Fifteen goals aredischarged by reduction or contradiction as we have describedabove. We are left with three goals to prove, as follows:
1) the constructor ctor-rec1 and the formula goal1,
2) the constructor ctor-rec2 and the formula goal1, and3) the constructor ctor-rec2 and the formula goal2.
The tool provides sufficient information for the users tounderstand the current state of the proof. By looking at the
attributes of the formulas to prove and the induction hypotheses
one can recognize each case mentioned above. All three ofthese subgoals are discharged by joining critical pairs and byinitializing one of the five lemmas previously mentioned (andproved). The theorem-proving technique presented in this paper
is interactive, which means that the user needs insight into
ABP to discharge the remaining cases. We will present theproof of the goal corresponding to ctor-rec1 and goal1:
h mod ABP-L is...
mb [B1#1,N#2,Ch1#3,B2#4,D#5,(Ch2#6,B1#1)]:
Reach[metadata "1" metadata "rec1"].
eq B2#4 = not B1#1 [metadata "4"].
ceq mk(N#2)= D#5 if B1#1 := B2#4
[metadata "2"
metadata "goal1" metadata "rec1"].
ceq mk(N#2) = pac(N#2),D#5
if not B1#1 := B2#4
[metadata "3"
metadata "goal2" metadata "rec1"].
...
endm` eq pac(s N#2),pac(N#2),D#5 = D#5[metadata "goal1"]; i

Notice that the following configuration is reachable

The proof script for the goal corresponding to ctor-rec1 andgoal1 is as follows:(. cp-l 1 >< 4)(. init inv3 by B1:Bit ← B1#1 ;N:PNat ← N#2 ; B2:Bit ← B2#4 ;D:Data ← D#5 ;Ch1:Channel1 ← Ch1#3 ;Ch2:Channel2 ← Ch2#6 ;Cn2:Channel2 ← (empty).Channel2 ; )Remember that the dot prefix means that the tactics are applicable only to the current goal. The tactic (. cp-l 1 >< 4)
thus joins the critical pairs generated by the axioms:
mb [B1#1,N#2,Ch1#3,B2#4,D#5,(Ch2#6,B1#1)]:
Reach[metadata "1"].
eq B2#4 = not B1#1
[metadata "4"].

More concretely, (. cp-l 1 >< 4) tries to unify a subterm of
the membership axiom 1 with the left-hand side of equation 4.
If the unification is successful, then it adds to the specificationof the current goal the membership axiom obtained from 1 by
substituting the right-hand side of the equation 4 for the subtermof the membership axiom 1 used for unification. Otherwise,
cp-l leaves the goal unchanged. Therefore, the following
membership axiom is added to the specification:
mb [B1#1,N#2,Ch1#3,not B1#1,D#5,(Ch2#6,B1#1)]:
Reach

The tactic init instantiates inv3 by the given substitution
and reduces all terms of the newly obtained sentence to theirnormal forms. The result is a goal obtained from the current
goal by adding the following equation to the specification:
eq not B1#1 = B1#1 .

Finally, the goal obtained in this way is discharged automatically by CITP because its underlying specification isinconsistent; see [10] for the full proof.

IV. R ELATED W ORK
The Alternating Bit Protocol is a well-established benchmark
in the area of formal methods, being used for more thanfour decades to test the strength and capabilities of various
verification technologies. The safety property of interest in
this case is that of reliable communication: all messages from
Sender are successfully delivered to Receiver, in the correct
order, even though the communication channels can lose or
duplicate messages. The result advanced in this paper is a fullymechanized proof with a high degree of automation, meaningthat most of the routine proofs are performed automatically.
Several variants of the ABP have been studied in the formalverification literature, among which [2], [3] are some of theearliest verification efforts (based on process algebra andbranching-time temporal logic). In many cases, in order tocope with the infinite state-space of the ABP, the solution
relies on imposing bounds or restrictions on communication
channels, reducing in this way the generality of the protocol.
A number of related studies use a combination of theoremproving and model-checking techniques in order to reason
about safety properties of the ABP. For example, in [20] theauthors use the Isabelle theorem prover to show that a cleverly
designed finite system is a suitable abstraction of the protocol,thus enabling the verification of safety properties of the ABP bymeans of model checking. In that case, theorem proving is used
for representing both the finite and the infinite-state systems,
and for verifying the soundness of the abstraction, meaning thatthe finite-state system has all the traces of the ABP. Similarly,[16] shows how ACL2 can be used to prove that a variantof the protocol is stuttering bisimilar to a finite-state system,
which can then be model-checked as well, while in [15], [25]the authors use the PVS theorem prover for analysing the
ABP by integrating static analysis, theorem proving, and othercomparable abstraction techniques.
Another prominent approach to verifying the ABP is basedon the use of co-algebraic languages for describing processes.
For instance, in [6] this has allowed the development of formal
correctness proofs for the protocol by representing Prasad’s
Calculus of Broadcasting Systems in the Coq theorem prover.
The proof presented in [7] is also co-algebraic, and it is basedon the circular co-inductive rewriting algorithm from BOBJ.
What distinguishes the tool and technique that we haveproposed in this paper is that:
1) It makes use of a single, general algebraic framework
for reasoning about the ABP, without the need to encode
within the framework a specialized language for describing
the protocol or to develop a finite-state abstraction of it;in particular, in contrast to [16], [20], the verification is
performed entirely by theorem proving.
2) There are no compromises in the specification of the
ABP; for instance, at any time, both the data and theacknowledgement channel can lose or duplicate information, not only from one of their end-points, but fromarbitrary positions; since the technique implicitly supports

associative data types, such properties can be specified ina straightforward way.
3) It combines general tactics, which are universal in thesense that they correspond to the underlying logic of CITP
(and can be used for all specifications), with specializedtactics, which are tailored to the data types declared withinitial semantics (and can be used only for specifications
that protect such data types).
The closest related work on proving safety properties of
the ABP is that on the framework of observational transition
systems [13], [21], where the focus is on proving the reliablecommunication between Sender and Receiver based on simultaneous induction. In [22], [23], the same property is proved
using a technique based on narrowing, which supports partiallythe unification of associative data types. Because of this, thespecification of the ABP from [22] models the dropping ofelements only from the first position of the communication
channels. The same compromise w.r.t. the specification of the
ABP was made in [21] as well.
It is worth mentioning that the specification ABP that wehave described in this paper (available at [10]) is much morecompact than the specification of the ABP that relies on the
OTS method [11]. On the other hand, the OTS method generates
no critical pairs for the case studies that we have analysedso far. This means that the OTS method has a higher levelof automation. Figure 4 presents a comparison of the formal
proof described here and the ones from [21], [22], and [13].
The human proof effort is significantly higher in [21]and [22] than in [13] and the present work. In the present
case study, there is no need to create a new module to define
extra predicates necessary for proving the desired properties.
Therefore, in the second row of the table in Figure 4, the numberof lines of code for these extra predicates in the present work
is 0. The number of state predicates in [22] is less than thenumber of invariants in the present work, but the definition ofpredicates in [22] takes almost the same number of lines ofcode as the specification. The specifications in [13] and thepresent contribution are closer to a real description than thespecifications in [21] and [22] since they model the droppingand duplication of elements from arbitrary positions of thechannels. There is no significant difference in length between
the proof presented in [13] and the proof described here; but
the specification in [13] is significantly longer than the one
given in this paper, and the difference would be more visible
for larger examples. In addition, the present specification canbe enhanced with transitions, which makes it possible to applymodel-checking techniques as well for verification.
V. C ONCLUSIONS AND O NGOING W ORK
In this paper, we have presented a proof technique fortransition systems that is supported by CITP. The tool isimplemented in Maude and presents important advantages
over previous versions of CITP and other state-of-the-art
theorem provers, including a new induction scheme based onmembership axioms, a tactic for joining critical pairs, andimproved decision procedures. We have exemplified theseC RITERIAM EASURE

Model
Model + Extra predicates
State predicates/invariants
Lemmata
Proof scripts
Proof scripts / # predicates

LOC
LOC

#
#
LOC
LOC

[21]

[22]

[13]

This work

286
286 + 63
11
7
5189
471

208
208 + 200
3
10
213
71

195
195 + 0
7
1
80
11

114
114 + 07
093
13

Fig. 4: Comparison with similar case studies

features in a case study on the verification of the ABP; theresults obtained encourage us to continue this line of research.
As future work, we are interested in developing newcommands for performing bounded rewriting, hence preventing
infinite computations, and also for applying specific equations
or rules to a goal. We are also conducting more case studies
to assess the strong points of the current implementation andprovide a solid example database for future users.
From the point of view of the interface, we aim to provide
a graphical user interface that includes options for saving thecurrent proof and editing commands. Moreover, a web interface
would allow users to use the tool without installing it, whileproviding an easy way to access the proofs developed so far.
R EFERENCES[1] K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on
reliable full-duplex transmission over half-duplex links. Commun. ACM,
12(5):260–261, May 1969.
[2] J. A. Bergstra and J. W. Klop. Verification of an alternating bit protocol
by means of process algebra. In W. Bibel and K. P. Jantke, editors,
Mathematical Methods of Specification and Synthesis of Software Systems’85, Proceedings of the International Spring School, Wendisch-Rietz, GDR,
April 22–26, 1985, volume 215 of LNCS, pages 9–23. Springer, 1985.
[3] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification offinite-state concurrent systems using temporal logic specifications. ACM
Trans. Program. Lang. Syst., 8(2):244–263, 1986.
[4] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, andC. L. Talcott, editors. All About Maude – A High-Performance Logical
Framework, How to Specify, Program and Verify Systems in Rewriting
Logic, volume 4350 of LNCS. Springer, 2007.
[5] R. Diaconescu and K. Futatsugi. CafeOBJ Report – The Language,
Proof Techniques, and Methodologies for Object-Oriented Algebraic
Specification, volume 6 of AMAST Series in Computing. World Scientific,
1998.
[6] E. Giménez. An application of co-inductive types in Coq: Verification of
the alternating bit protocol. In S. Berardi and M. Coppo, editors, Typesfor Proofs and Programs, International Workshop TYPES’95, Torino,
Italy, June 5–8, 1995, Selected Papers, volume 1158 of LNCS, pages
135–152. Springer, 1995.
[7] J. A. Goguen and K. Lin. Behavioral verification of distributed concurrent
systems with BOBJ. In 3rd International Conference on Quality Software(QSIC 2003), 6–7 November 2003, Dallas, TX, USA, page 216. IEEE
Computer Society, 2003.
[8] J. A. Goguen and J. Meseguer. Completeness of many-sorted equational
logic. SIGPLAN Notices, 17(1):9–17, 1982.
[9] D. Găină. Constructor-based Inductive Theorem Prover. http://imi.
kyushu-u.ac.jp/∼daniel/citp.html, 2018. [Online; accessed July 2018].
[10] D. Găină. The Alternating Bit Protocol – Explicitly described states.
http://imi.kyushu-u.ac.jp/∼daniel/examples/abpr/abp.html, 2018. [Online;
accessed July 2018].
[11] D. Găină. The Alternating Bit Protocol – The OTS/CafeOBJ method.
http://imi.kyushu-u.ac.jp/∼daniel/examples/abp/abp.html, 2018. [Online;
accessed July 2018].
[12] D. Găină, K. Futatsugi, and K. Ogata. Constructor-based Logics. J. UCS,
18(16):2204–2233, 2012.

[13] D. Găină, D. Lucanu, K. Ogata, and K. Futatsugi. On Automation of
OTS/CafeOBJ Method. In S. Iida, J. Meseguer, and K. Ogata, editors,
Specification, Algebra, and Software, volume 8373 of LNCS, pages
578–602. Springer, 2014.
[14] D. Găină, M. Zhang, Y. Chiba, and Y. Arimoto. Constructor-based
Inductive Theorem Prover. In R. Heckel and S. Milius, editors, Algebra
and Coalgebra in Computer Science – 5th International Conference,
CALCO 2013, volume 8089 of LNCS, pages 328–333. Springer, 2013.
[15] K. Havelund and N. Shankar. Experiments in theorem proving andmodel checking for protocol verification. In M. Gaudel and J. Woodcock,editors, FME ’96: Industrial Benefit and Advances in Formal Methods,
Third International Symposium of Formal Methods Europe, Co-Sponsoredby IFIP WG 14.3, Oxford, UK, March 18–22, 1996, Proceedings, volume1051 of LNCS, pages 662–681. Springer, 1996.
[16] P. Manolios, K. S. Namjoshi, and R. Summers. Linking theorem proving
and model-checking with well-founded bisimulation. In N. Halbwachs
and D. A. Peled, editors, Computer Aided Verification, 11th International
Conference, CAV ’99, Trento, Italy, July 6–10, 1999, Proceedings, volume1633 of LNCS, pages 369–379. Springer, 1999.
[17] N. Martı́-Oliet and J. Meseguer. Rewriting logic as a logical and semantic
framework. In D. M. Gabbay and F. Guenthner, editors, Handbook of
Philosophical Logic, Second Edition, Volume 9, pages 1–87. Kluwer
Academic Publishers, 2002. First published as SRI Technical Report
SRI-CSL-93-05, August 1993.
[18] J. Meseguer. Membership algebra as a logical framework for equational
specification. In F. Parisi-Presicce, editor, Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, volume1376 of LNCS, pages 18–61. Springer, 1997.
[19] J. Meseguer and J. A. Goguen. Initiality, induction, and computability.
In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics,
pages 459–541. Cambridge University Press, New York, NY, USA, 1986.
[20] O. Müller and T. Nipkow. Combining model checking and deduction for
i/o-automata. In E. Brinksma, R. Cleaveland, K. G. Larsen, T. Margaria,
and B. Steffen, editors, Tools and Algorithms for Construction andAnalysis of Systems, First International Workshop, TACAS ’95, Aarhus,
Denmark, May 19–20, 1995, Proceedings, volume 1019 of LNCS, pages
1–16. Springer, 1995.
[21] K. Ogata and K. Futatsugi. Simulation-based Verification for Invariant
Properties in the OTS/CafeOBJ Method. Electr. Notes Theor. Comput.
Sci., 201:127–154, 2008.
[22] C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD
thesis, University of Illinois at Urbana-Champaign, 2012.
[23] C. Rocha and J. Meseguer. Proving safety properties of rewrite theories.
In A. Corradini, B. Klin, and C. Cı̂rstea, editors, Algebra and Coalgebrain Computer Science – 4th International Conference, CALCO 2011,
Winchester, UK, August 30 – September 2, 2011. Proceedings, volume6859 of LNCS, pages 314–328. Springer, 2011.
[24] D. Rosén and N. Smallbone. TIP: Tools for Inductive Provers. In
M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic
for Programming, Artificial Intelligence, and Reasoning – 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24–28, 2015,
Proceedings, volume 9450 of LNCS, pages 219–232. Springer, 2015.
[25] V. Rusu and E. Singerman. On proving safety properties by integrating
static analysis, theorem proving and abstraction. In R. Cleaveland, editor,
Tools and Algorithms for Construction and Analysis of Systems, 5thInternational Conference, TACAS ’99, Held as Part of the European
Joint Conferences on the Theory and Practice of Software, ETAPS’99,
Amsterdam, The Netherlands, March 22–28, 1999, Proceedings, volume1579 of LNCS, pages 178–192. Springer, 1999.