Lecture Notes in Computer Science, Number 1102.
From Computer-Aided Verification, CAV '96.
Edited by Rajeev Alur and Thomas A. Henzinger.
Springer-Verlag, New Brunswick, NJ.
July/August, 1996.
Pages 169–183.

The automated deduction and model checking communities have developed techniques that are impressively effective when applied to suitable problems. However, these problems seldom coincide exactly with those that arise in formal methods. Using small but realistic examples for illustration, I will argue that effective deductive support for formal methods requires cooperation among different techniques and an integrated approach to language, deduction, and supporting capabilities such as simulation and the construction of invariants and abstractions. Successful application of automated deduction to formal methods will enrich both fields, providing new opportunities for research and use of automated deduction, and making formal methods a truly useful and practical tool.

@inproceedings{Rushby96:CAV,
    AUTHOR = {John Rushby},
    TITLE = {Automated Deduction and Formal Methods},
    BOOKTITLE = {Computer-Aided Verification, {CAV} '96},
    YEAR = {1996},
    EDITOR = {Rajeev Alur and Thomas {A.} Henzinger},
    SERIES = {Lecture Notes in Computer Science},
    NUMBER = {1102},
    PAGES = {169--183},
    ADDRESS = {New Brunswick, {NJ}},
    MONTH = {July/August},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cav-cade96/}
}

• cav-cade96-slides.ps.gz
• cav-cade96.dvi.gz
• cav-cade96.ps.gz