++++++++++++++++++ FME2001: - Review reports for paper 33 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 33 CATEGORY: 2 TITLE: Combining Theorem Proving and Model Checking --- A Case Study AUTHOR(S): Dennis Dams Dieter Hutter Natalia Sidorova -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper reports on a case study proving the Bounded Retransmission Protocol correct by abstracting it. The abstraction techniques are completely standard and the paper focusses on automating the inductive proofs the safety of data abstractions. It is described how the INKA system was extended by known heuristics to perform those proofs automatically. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 1 Please comment your rating: - the core of the paper is about heuristics for inductive theorem proving. This is neither very appropriate for FME, nor do the presented heuristics add up to anything very coherent. In a nutshell, there is no abstract contribution to the field, just a fuzzily described heuristic which may or may not work on similar examples. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 2 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 5 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: - the abstraction idea is standard (eg Dingel and Filkorn, CAV95), but the authors even fail to refer to closely related case studies. For example Mueller and Nipkow, TACAS 95, verify the ABP (which is closely related to the BRP) including the safety of an abstraction. Finally, we are past the stage where pushing a single well known example through a theorem prover constitutes a scientific paper. 6. How WORTHWILE is the goal of the authors? Comment: quite worthwhile 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: quite well 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: sound but sketchy 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: - there is no comparison with other inductive theorem provers, especially the Boyer-Moore system. But such comparisons are important to evaluate the novelty and competitiveness of the heuristics. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: 3.3: the beginning is completely unclear: "If the first element of l arrives at least once...": I would hope the prefix property holds otherwise as well. "It can be proved": how? In INKA? On paper? By model checking? Further down: "where the last one" Which last one? The last element of the list? The whole sentence is cryptic. 4: (3) is the standard data refinement proof obligation which has been treated by inductive theorem proving for ages. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 33 CATEGORY: 2 TITLE: Combining Theorem Proving and Model Checking --- A Case Study AUTHOR(S): Dennis Dams Dieter Hutter Natalia Sidorova -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Data abstraction can be used to reduce the state space of a model checking problem. The authors descibe heuristics to enable a theorem prover to automatically carry out inductive proofs of safety properties of data abstractions. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: Automation of tools is an important issue in FM, however, the scope of the paper is rather narrow. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The heuristics used for inductive proofs of safety of data abstractions. 6. How WORTHWILE is the goal of the authors? Comment: Very! Automation must be one of the prime objectives of FM. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is very well motivated and explained referring e.g. to the difficulty of manual analysis. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes, although there are some clerical mistakes, see 12 below. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The methodology is sound. The relevance of the experimental results is justified by the claim that they are applicable to other examples as well. However, little evidence is given to back up that claim. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Good. The problem and the solution are well explained. 11. Were there any formatting or mechanical problems with this paper?: No. Are the figures and length acceptable?: Yes. Are the references correct?: Yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: On page 9, line 1, "aelem" should be "anat". On page 9, line 2, "consP" should be "is_cons". On page 10, formula (4), "a_tcons" should be "a_tcons1" +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 33 CATEGORY: 2 TITLE: Combining Theorem Proving and Model Checking --- A Case Study AUTHOR(S): Dennis Dams Dieter Hutter Natalia Sidorova -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes refinements made to a theorem prover, INKA, that allow a proof of the correctness of an abstract interpretation to be carried out without user guidance. The abstract interpretation is used to generate a finite-state model of a version of the alternating bit protocol, which can then be verified using a model checker. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: Automated theorem provers are used in many applications of formal methods; hence, techniques developed for enabling automated proofs are of importance. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 ================ NB: There should be a correlation between the two rates above. *** why? the paper could address a relevant topic, without being acceptable for publication! ================= 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: This is what I find difficult to determine. The idea of using theorem provers to check the correctness of proposed abstractions is not new (see past issues of the CAV conference). The algorithms added to INKA for case analysis and automatic derivation of induction schemes appear to be quite similar to algorithms used in existing theorem provers such as the Boyer-Moore, ACL2, and PVS provers. The paper does not present any detailed comparisons with this earlier work, which makes it difficult to determine how these algorithms improve on existing methods. 6. How WORTHWILE is the goal of the authors? Comment: The goal of automating proofs as much as possible is definitely worthwhile, as well as their original motivation, which is to verify the correctness of proposed abstractions. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: quite well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: yes 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: yes to all but the second question (see answer to #5) 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: the writing quality is good overall. Detailed comparisons with related work, such as the strategies used in the Boyer-Moore, ACL2 and PVS theorem provers, is missing. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: see answer to #5 [ By the second sub-referee: 1. On page 2, the authors write Our goal is to provide a mechanism for establishing the correctness of user-constructed abstractions. Here, we investigage the use of theorem proving for this purpose. ... I would point their attention to Panagiotis Manolios, Kedar Namjoshi, and Robert Sumners. Linking Theorem Proving and Model-Checking with Well-Founded Bisimulations. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification, CAV '99, volume 1633 of LNCS, pages 369-379. Springer-Verlag, 1999 It is available from http://www.cs.utexas.edu/users/pete/publications.html. And the reason it is relevant is that they also describe the use of theorem proving to prove abstractions correct, but their approach allows them to preserve both safety and liveness properties. Finally, they also verify a variant of the alternating-bit protocol. 2. There are similarities with their heuristics and the ones in ACL2. For example, ACL2 has to deal with the problem in Section 4.2 (induction vs. case analysis). They reference Bundy's work on rippling, but in Section 4.1, they should reference Boyer/Moore or ACL2 because they invented this way of proving theorems about recursive functions and this is what all the work on induction I have seen builds on. In Section 4.3, they do reference Boyer/Moore for the idea of generalization. In Section 4.4, they discuss nested induction and ACL2 does do that also. ] +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++