PAPER TITLE: Reasoning about Systems with Many Data Values without Data Independence Assumption (extended abstract)
AUTHORS: Yung-Pin Cheng and Keh-Ren Wu

Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
-------(Review 1)-----------------------------------------------------------------------------------------------------------
Appropriateness:          3
Originality:              3
Technical strength:       2
Presentation:             1
-------------------------------------------------------------------------------------------------------------------
Overall:                  2

Comments to the authors:

    Paper proposes use of refactoring to transform system models
    with many data values into a form suitable for analysis by induction.
    There is no convincing demonstration as to why this technique may
    be better than other techniques for parameterizing systems, and 
    perhaps a more detailed treatment is needed. 
    Errors in your English are noticeable, and should be removed before 
    submission. Consider the sentence: "Under that assumption, properties on small 
    finite instantiations can be inferred to systems parameterized by 
    arbitrary number of size". It is hard to parse and is confusing.
    The introduction, motivation and background to your work is good,
    but takes up 4 of the 6 pages. ABP requires little explanation. 
    When you get to refactoring in section 5, you did not make clear what 
    you were doing. I would much rather see some representation of the 
    resultant refactored code, and only a listing of (say) the receiver ABP code.
    The very brief sections 5 and 6 should be extended to show more detail.
    Finally - I was not convinced in the end of the usefulness of this from this
    paper. 
    





Score values 
0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
------(Review2)-------------------------------------------------------------------
Appropriateness: 4
Originality: 1
Technical strength: 2
Presentation: 2
-------------------------------------------------------------------------
Overall: 2

Comments to the authors: 

This paper presents the following approach: To verify a system which is  
parameterized with respect to data values 1) Use an automatic refactoring 
tool to transform the input system to a system which is parameterized with 
respect to the number of processes, 2) Find a network invariant that is 
strong enough to prove the property of interest, 3) Automatically check if 
the invariant conditions are satisfied. The paper presents an application 
of the proposed technique to the Alternating Bit Protocol.

I do not understand what are the new contributions presented in this 
paper. It seems to me that this paper basically summarizes the results 
from previously published papers by the authors. What are the new
contributions in this paper compared to FSE'03 and ISSTA'03 papers by the 
first author?

This paper looks unfinished. Section 6 needs more detailed discussion 
on how to find the network invariant. This is a crucial step in the 
presented approach but it is not discussed in detail. I think the fact 
that the user has to provide the network invariant seems to me to be a big 
drawback of the presented approach. The authors state that finding a 
network invariant is undecidable in general. Are there any automated 
techniques which can generate a network invariant in some restricted 
cases? 
 
In Section 3 the authors describe two approaches to automated verification
of infinite state spaces. There is another approach which is not discussed:
Using symbolic representations which can encode infinite sets (such as
linear arithmetic constraints or automata) and computing conservative
approximations of fixpoints required in symbolic verification. Results
on this approach has been reported in major verification conferences
such as CAV and TACAS.

Corrections:

Section 1, last line of paragraph 1:
change
"... parameterized systems and etc. ..." 
to
"... parameterized systems etc. ..."

Page 2, second column, line 22:
change
"... X onto a fixed, finite types ..."
to
"... X onto a fixed, finite type ..."

Page 2, second column, line 24:
change
"... equality test like ..."
to 
"... equality tests such as ..."

Page 2, second column, line 32:
change
"... protocols, and etc. ..."
to
"... protocols, etc. ..."

Page 3, last sentence of Section 3.
" The tool support of refactoring has been reported in [12]."
[12] is not the right citation here.

Page 5, column 1, line 8:
change
"CCS is a two-way ..."
to
"CCS has a two way ..."

Page 5, column 2, the line under Fig. 3:
"-data_in:packet_1" is broken to two lines. 

Page 6, reference [3]:
It seems that the font size for this reference is bigger than the font 
size for the other references.

Page 7, reference [19]:
This is reference is empty.


Score values 
0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
------(Review 3)-------------------------------------------------------------------
Appropriateness: 3
Originality: 2
Technical Strength: 1
Presentation: 2
-------------------------------------------------------------------------
Overall: 2


The concept of refactoring is interesting and has been 
used in previous work of the authors.  
The presentation can be more detailed. 
The work also lacks a theoretical framework for refactoring and 
thus the authors cannot prove properties about their techniques.