++++++++++++++++++ FME2001: - Review reports for paper 39 +++++++++++++++++++++ - 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: 39 CATEGORY: 1 TITLE: Formal Implementation of a Verification Algorithm using the B Method AUTHOR(S): Ludovic Casset -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): I think he is defining, modeling, and verifying a Java byte code verifier. He writes "To obtain the formal description, we worked on the formalisation of the defensive Java Virtual Machine (DJVM), a machine performing tests on an instruction just before executing it". 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: 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. 4. CONFIDENCE LEVEL: Please provide a rating of 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: 2 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: verified termination of byte code verifier 6. How WORTHWILE is the goal of the authors? Comment: the goal of insuring that Java program executions are safe is a good one. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: I found the motivation section very difficult to follow. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: probably. 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: this is verification of a practical system. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: This paper is difficult to understand. The big picture is poorly explained. I am not sure what is being developed or verified. There are lots of grammar mistakes and the sentence structure is very awkward in many places. For example section 4.2 begins "The main theorem is another kind of specification. It is an abstract specification at the opposite of the previous one, which is more concrete." 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: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 39 CATEGORY: 1 TITLE: Formal Implementation of a Verification Algorithm using the B Method AUTHOR(S): Ludovic Casset -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a formal description, implementation, and verification of a part of the Java Byte Code Verifier within the B-method. The design and verification of the central program loop is a significant issue which the paper addresses. This is an excellent case study. 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: An application of a tool-supported formal method to a real implementation and verification problem is of significant interest. 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: 4 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 description and verification of the byte code verifier, and the design presented to enable verification of large loops are both new and of some significance. The paper is essentially a large case study, but novel methods have been developed for it. 6. How WORTHWILE is the goal of the authors? Comment: The use of formal methods to verify a critical part of a system is extremely worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The general goal, using formal methods on a case study to learn about and refine the method itself, is not clearly stated. The specific goal, of proving (part of) the JVM is clearly stated. Some of the aspects of the case study are not made clear. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes, but the explanations can be a little unclear in places. 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 paper does seem to be about a new formal technique, the way loops can be handled within B; and about how to model and analyse something like a byte code verifyier. The case study does make a case for the technique. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Some minor grammatical errors. I suggest the author asks someone to read through the paper when it is revised. 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: There are a number of minor grammatical errors that will need to be corrected. You need more/clearer explanations about how stacks are `merged'. You talk about their `joint' (join?), but in the code (e.g. in Fig 8) you use Meet. Is `merge' taking the least upper bound? Since it is central to the process, it should also be made more explicit at what point you actually check the types of elements of the stack during the verification process. (Seems to be part of the IF condition in Fig 8). The example in Fig 5 could be used a little more extensively. In particular, you could say more about it, and give the fixed point associated with each point in the stack, or even show how the implementation calculates it. Also, you have `psuh0' for push0, and `if 5' should read `if 4' +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 39 CATEGORY: 1 TITLE: Formal Implementation of a Verification Algorithm using the B Method AUTHOR(S): Ludovic Casset -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper is supposed to describe the implementation and verification of JVM bytecode verifier. Unfortunately, there are two major problems: 1. The model of the JVM is extremely abstract and thus almost trivial. 2. The specifications are either almost directly executable (as in the case of operations computing tables pointwise from other tables) or degenerated to the point where merely termination is required. It is the second point that kills the paper, as I will detail below. 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: The fact that it is relevant does NOT mean it is a good paper, but merely that it could have been interesting. 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: 1 By now there is a widely accepted model of what the bytecode verifier should be doing and how this should be described. Freund and Mitchell have specified this model in some detail for a large subset of JVM instructions. This, and related publications are cited in the beginning and lead one to think that the author builds on this work. However, such an abstract specification never enters the picture at all. Instead we start from specifications that are already close to executable, even if the verbose notation hides this a little. Even worse, the only specification of the main loop is that it should terminate, and the main theorem of the paper is its termination. This termination proof is made out to be very difficult, but is really very simple: a two-dimensional table with entries from a finite ordered set is modified in each loop iteration such that at least one entry increases. Thus the sum of the entries in the table must increase. I am afraid the state of the art in program verification is more advanced than that. The fact that the development took place in B is not enough of a justification to publish it. The author even cites two other proofs [Ber-00, Nip-00] that tackle the real problems. Furthermore, the model of the JVM in this paper is extremely limited: it only has integers and address. The introduction of class types would complicate matters (incl the termination proof) severely. There are also some inaccuracies, like the permission of TOP on the stack, which the real JVM disallows. NB: There should be a correlation between the two rates above. NO! See 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: Very little 6. How WORTHWILE is the goal of the authors? Comment: Worthwhile yes, but only very limited. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: 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: 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Finally, the paper is written very badly, both contents and language wise. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: [Pus-98] is missing. Long live MS Word! 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Fig 1: The sigma after Init is bogus. If does not test the value of L but the top of the stack! What is "consistency and coherence" of Freund and Mitchell's system? Fig 2: The diagram is badly drawn: there should only be one bottom. Fig 4: This whole example is badly wrong. The first stack should only have 2 entries addri and integer The second stack should only have 1 entry integer (or even 0 if "if" pops the top element) The TOP elements are bogus and the merge should lead to an error. Fig 17: you must explain the abbreviations in the first line. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++