Convergence Testing in Term-Level Bounded Model Checking

Abstract

We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it converges for many practical examples, including pipelined processors. We give a new formal definition of convergence that generalizes previously stated criteria. We also give a sound semi-decision procedure to check this criterion based on a translation to quantified separation logic. Preliminary results on simple pipeline processor models are presented.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2003
Accession Number
ADA461050

Entities

People

  • Randal Bryant
  • Sanjit A. Seshia
  • Shuvendu K. Lahiri

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Human Systems

DTIC Thesaurus Topics

  • Abstracts
  • Arithmetic
  • Automata
  • Computer Science
  • Consistency
  • Convergence
  • Equations
  • Language
  • Models
  • Notation
  • Pipelines
  • Sequences
  • Simulations
  • Symbols
  • Transitions
  • Translations
  • Verification

Readers

  • Integrated Circuit Design and Technology.
  • Mathematical Modeling and Probability Theory.