SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Automated Deduction and Formal Methods
 by Dr. John Rushby.

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.


Abstract
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.
BibTEX Entry
@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/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy