Automating Modular Verification

Abstract

Modular techniques for automatic verification attempt to overcome the state-explosion problem by exploiting the modular structure naturally present in many system designs. Unlike other tasks in the verification of finite-state systems, current modular techniques rely heavily on user guidance. In particular, the user is typically required to construct module abstractions that are neither too detailed as to render insufficient benefits in state exploration, nor too coarse as to invalidate the desired system properties.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1999
Accession Number
ADA461302

Entities

People

  • Freddy Y. Mang
  • Luca De Alfaro
  • Rajeev Alur
  • Thomas Henzinger

Organizations

  • University of Pennsylvania

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Automatic
  • Availability
  • California
  • Classification
  • Computer Science
  • Computers
  • Contracts
  • Engineering
  • Explosions
  • Guidance
  • Information Operations
  • Instructions
  • Monitoring
  • Security
  • Three Dimensional
  • Verification

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering
  • Systems Analysis and Design