Paper Number:8 Paper Title: Behavioural Unfolding of Formal Specifications Based on Communicating Extended Automata Authors: N. Rapin, C. Gaston, A. Lapitre and J.P. Gallois ---------(Review1)---------------------------------------------------------- Appropriateness: 4 Originality: 3 Technical strength: 4 Presentation: 3 Overall: 4 Score values 0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). ------(Review 2)------------------------------------------------------------------------------------------------------------ Appropriateness: 3 Originality: 3 Technical strength: 3 Presentation: 2 ------------------------------------------------------------------------------------------------------------------- Overall: 3 Comments to the authors: The paper is supposed to present the theoretical foundations for the toolset AGATHA. Theoretical results are given in behavioral unfolding of specifications of communicating extended automata. Four theorems are given, but no proofs are attached. Although intuitively the results are correct, it will make your results more convincing if you have presented some proofs or proof sketches. Or at least in a reachable technical report. The notation used looks a bit heavy. Some of them should be explained when introduced. For example, in definition 1, you should explain "Fonct", "Pred". You cannot assume audiences are already familiar with your notations. In definition 2, should some of Q, T, V be finite? If so, you have to make it explicit. Your definition 3 seems quite declarative. Can you give an explicit definition of Mod_M (p), like Mode_M (p) =_def {...}. It is not very clear to me what it actually looks like. Perhaps an example is helpful. I believe this definition is very important for later discussion. As claimed to be a theorectial foundation paper, you should also give proofs or proof sketches for your four theorems, rather than just present the theorem itself. More informal elaboration will be helpful. Minors: If you change some capital words like AGATHA, EIOLTS to \textit{AGATHA}, \textit{EIOLTS}, they will become more compact and look better. Acknowledgement should be in a seperate section, as it is not part of conclusion. Score values 0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). ----------(Review 3)-------------------------------------------------------------------------------------------------------- Appropriateness: 4 Originality: 3 Technical strength: 4 Presentation: 2 ------------------------------------------------------------------------------------------------------------------- Overall: 4 Comments to the authors: The authors present the foundation of a verfication tool set. The main idea is to use symbolic execution to capture the behavior of the system. Unlike concrete execution, symbolic execution is capable of representing multiple (possibly infinite) computation paths by a single path of the syntactic execution tree. In principle, one can perform verification of infinite systems on symbolic execution trees. However, there is no guarantee that syntactic execution trees are always finite. The author attacks the problem by a technique called reduction by inclusion: if a symbolic execution state represents a subset of the semantics of a previously visited symbolic execution state, a inclusion transition is generated to avoid creating the smaller execution state. The reduction may introduce inconsistent paths to the symbolic execution representation. However, the simulation relation is still preserved. I think the paper is interesting. Although symbolic execution is not new, verification by symbolic execution is still young and under investigation. The reduction technique presented in the paper is quite interesting. Unfortunately, the proofs are missing due to the space limit. Besides, the representation may need a little improvement. Overall, I think it is a good work and recommand it. Here I would like to ask a technical question. In the inclusion reduction, the inclusion transition is introduced when Mod_M (t(Q)) \subseteq Mod_M (Q'). It makes sense to have this criteria as the newly generated symbolic execution state is "covered" by a previous symbolic execution state. I wonder if it makes sense to check the path condition \pi. Would it exclude some inconsistent paths? Or is the proposed criteria actually stronger than checking the path condition? Going back to semantic domain to check the inclusion seems somewhat contradictory to the main idea of symbolic execution. Here are some of the typos/notational problems I found: pp 4, Definition 3. I cannot find any word about \bar{\nu'}. It appears frequently in the paper as well. pp 4, Definition 4. "let us note P the set of ...". P should be {\cal P}. pp 7, Definition 8. "For all Q = (q, \pi, \sigma : V -> L^P}..." The type of \sigma can be ignored. pp 7, Definition 8. "Or Q' is the least ses regarding ...", ses should be SES.