Accepted papers will be published in a volume of the Springer-Verlag series Lecture Notes in Computer Science (LNCS). These papers must be prepared in the style of that series.
Papers should be submitted electronically in either Postscript or Adobe PDF. Specific instructions will be posted here.
In general, the length of a paper should be commensurate with the contribution it makes. The final versions of all papers, however, must be kept to 18 pages or less when formatted in the LNCS style. It may be advisable to begin to prepare your document in something approximating the LNCS style from an early stage so that you have an accurate knowledge of its length when presented in this format.
One author of each paper must complete and return a form transferring the copyright for the paper to Verlag. The form is available for download in either PDF or HTML formats. You will need the following information to complete the form:
| Conference: | FMCAD 2002: The 4th International Conference on Formal Methods in Computer-Aided Design |
| Volume Editors | M. Aagaard and J. O'Leary |
Once you have completed the form, please fax it to Mark Aagaard at +1 (519) 746-3077.
The FMCAD community is drawn from users of a wide variety of verification techniques and tools. You should strive to make paper accessible to the broader FMCAD community, not just other users of the same tool that you use. At least one reviewer for each tool-based paper submitted to FMCAD will be deliberately drawn from the users of a different tool. Reviewers will be asked to judge, among other things, the accessibility of the paper to the wider FMCAD audience.
One barrier to effective communication, both within the FMCAD community and between the FMCAD community and other communities, is the variety of concrete syntaxes used by different tools for mathematical notation that is unavailable in standard character sets. To avoid this problem we ask that where possible you use common mathematical notations in your paper rather than the concrete syntax of any particular tool. To emphasise that mathematics has been machine checked you may like to depart from the LNCS style and use a Teletype or Sans-Serif font for the text of your expressions rather than the mandated Roman and Italic fonts. For example, you should write something like
,(even (j7k3 + k + 1)) or ,(even (j7k3 + k + 1))
for ordinary mathematics to emphasise machine checking
in preference to
~(even (j * (k EXP 3) + k + 1)),
the same expression in the concrete syntax of, for example, the HOL theorem proving system.
Of course, you may need to use concrete syntax in your paper - for example, if the syntax itself is under discussion - but please explain any aspects that are not obvious.
All papers should be produced using LaTeX2e with the Springer LLNCS document class.
All authors should read these documents and ensure that their contributions meet the specifications contained therein before submitting their camera-ready copy.
We are asking all authors to prepare their submissions using LaTeX2e and the Springer LLNCS document class for the following reasons:
Macro packages for producing papers in the LNCS style are also available for use with the old LaTeX (LaTeX2.09), plain TeX and for Microsoft Word. You should note, however, that papers prepared using these systems will not be annotated with hyper-links in the electronic edition of the conference proceedings. Furthermore, authors using Microsoft Word should know that their paper will by typeset using Times Roman fonts while all other papers will be typeset using Computer Modern Roman fonts, and thus your paper will look a little out of place in the printed proceedings.
Regardless of which system you use to prepare your paper, you should read both the instructions for LNCS authors and the LLNCS document class instructions to ensure that your document mirrors the LNCS style as closely as possible.