Lecture Notes in Computer Science, Volume 967.
From ZUM '95: The Z Formal Specification Notation; 9th International Conference of Z Users.
Edited by Jonathan P. Bowen and Michael G. Hinchey.
Springer-Verlag, Limerick, Ireland.
September, 1995.
Pages 105–113.

Mechanization makes it feasible to calculate properties of formally specified systems. This ability creates new opportunities for using formal methods as an exploratory tool in system design. Achieving enough efficiency to make this practical raises challenging problems in automated deduction. These challenges can be met only by approaches that integrate consideration of its mechanization into the design of a specification language.

@inproceedings{Rushby95:ZUM,
    AUTHOR = {John Rushby},
    TITLE = {Mechanizing Formal Methods: Opportunities and Challenges},
    BOOKTITLE = {{ZUM} '95: The {Z} Formal Specification Notation; 9th International Conference of {Z} Users},
    YEAR = {1995},
    EDITOR = {Jonathan {P.} Bowen and Michael {G.} Hinchey},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {967},
    PAGES = {105--113},
    ADDRESS = {Limerick, Ireland},
    MONTH = {sep},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/zum95/}
}

• zum95-slides.dvi.gz
• zum95-slides.ps.gz
• zum95.dvi.gz
• zum95.pdf
• zum95.ps.gz