rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    title: Automated theorem proving in software engineering
  name:
    name part: Schumann, Johann M.
    name part: 1960-
    role:
      role term: creator
  name:
    name part: SpringerLink (Online service)
  type of resource: text
  genre: bibliography
  genre: Electronic books.
  origin info:
    place:
      place term: gw
    date issued: 2001
    issuance: monographic
  language:
    language term: eng
  physical description:
    form: remote
    extent: 1 online resource (xiv, 228 pages) : illustrations.
  abstract: 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.
  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.
  note: Johann M. Schumann ; foreword by Donald Loveland.
  note: Includes bibliographical references (pages [203]-220) and index.
  subject:
    topic: Software engineering
  subject:
    topic: Automatic theorem proving
  subject:
    topic: Génie logiciel
  subject:
    topic: Théorèmes
    topic: Démonstration automatique
  subject:
    topic: Automatisches Beweisverfahren
  subject:
    topic: Software Engineering
  subject:
    topic: Automatic theorem proving
  subject:
    topic: Software engineering
  classification: QA76.758 .S38 2001eb
  classification: 005.1
  classification: ST 230
  classification: ST 304
  related item:
    title info:
      title: Automated theorem proving in software engineering
    name:
      name part: Schumann, Johann M., 1960-
    identifier: (DLC) 2001020538
    identifier: (OCoLC)46359489
  identifier: 9783662226469 (electronic bk.)
  identifier: 3662226464 (electronic bk.)
  identifier: 3540679898
  identifier: 9783540679899
  identifier: 3642087590
  identifier: 9783642087592
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: GW5XE
    record creation date: 131029
    record change date: 20260422165542.7
    record identifier: in00003541189
    language of cataloging:
      language term: eng