عنوان
پدید آورنده
موضوع
رده
کتابخانه
محل استقرار
INTERNATIONAL STANDARD BOOK NUMBER
(Number (ISBN
3662226464
(Number (ISBN
9783662226469
NATIONAL BIBLIOGRAPHY NUMBER
Number
b567027
TITLE AND STATEMENT OF RESPONSIBILITY
Title Proper
Automated theorem proving in software engineering
General Material Designation
[Book]
First Statement of Responsibility
Johann M. Schumann ; foreword by Donald Loveland.
.PUBLICATION, DISTRIBUTION, ETC
Place of Publication, Distribution, etc.
Berlin ; New York
Name of Publisher, Distributor, etc.
Springer, [
Date of Publication, Distribution, etc.
2001] ©2001
PHYSICAL DESCRIPTION
Specific Material Designation and Extent of Item
(xiv, 228 pages) : illustrations
CONTENTS NOTE
Text of Note
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.
SUMMARY OR ABSTRACT
Text of Note
The growing demand for high quality, safety, and security of software systems can only be met by rigorous application of formal methods during software design. Tools for formal methods in general, however, do not provide a sufficient level of automatic processing. This book methodically investigates the potential of first-order logic automated theorem provers for applications in software engineering. Illustrated by complete case studies on verification of communication and security protocols and logic-based component reuse, the book characterizes proof tasks to allow an assessment of the provers capabilities. Necessary techniques and extensions, e.g., for handling inductive and modal proof tasks, or for controlling the prover, are covered in detail. The book demonstrates that state-of-the-art automated theorem provers are capable of automatically handling important tasks during the development of high-quality software and it provides many helpful techniques for increasing practical usability of the automated theorem prover for successful applications.
TOPICAL NAME USED AS SUBJECT
Automatic theorem proving.
Génie logiciel.
Software engineering.
PERSONAL NAME - PRIMARY RESPONSIBILITY
Johann M. Schumann ; foreword by Donald Loveland.
PERSONAL NAME - ALTERNATIVE RESPONSIBILITY
Johann M Schumann
ELECTRONIC LOCATION AND ACCESS
Electronic name
مطالعه متن کتاب [Book]
Y
