Automated theorem proving in software engineering

Author(s)

• Schumann, Johann M.
• Loveland, Donald W.

Bibliographic Information

Automated theorem proving in software engineering

Johann M. Schumann ; foreword by Donald Loveland

Springer, c2001

Note

Includes bibliographical references (p. [203]-220) and index

Description and Table of Contents

Description

Growing demands for the quality, safety, and security of software can only be satisfied by the rigorous application of formal methods during software design. This book methodically investigates the potential of first-order logic automated theorem provers for applications in software engineering. Illustrated by complete case studies on protocol verification, verification of security protocols, and logic-based software reuse, this book provides techniques for assessing the prover's capabilities and for selecting and developing an appropriate interface architecture.

Table of Contents

1. Introduction.- 2. Formal Methods in Software Engineering.- 3. Processing of Logic.- 4. Characteristics of Proof Tasks.- 5. Requirements.- 6. Case Studies.- 7. Specific Techniques for ATP Applications.- 8. Conclusions.- References.

by "Nielsen BookData"

Details

• NCID: BA52577580
• ISBN:
  • 3540679898
• Country Code: gw
• Title Language Code: eng
• Text Language Code: eng
• Place of Publication: Berlin
• Pages/Volumes: xiv, 228 p.
• Size: 24 cm
• Subject Headings:
  • LCSH : Software engineering
  • LCSH : Automatic theorem proving