Deciding Linear Inequalities by Computing Loop Residues.

Abstract

The real and integer feasibility of sets of linear inequalities of the form x < or = y + c can be decided quickly by examining the loops in certain graphs. The method is generalized first to real feasibility of inequalities in two variables and arbitrary coefficients, and ultimately to real feasibility of arbitrary sets of linear inequalities. The method is well suited to applications in program verification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 10, 1978
Accession Number
ADA055868

Entities

People

  • Robert Shostak

Organizations

  • SRI International

Tags

Communities of Interest

  • C4I
  • Human Systems

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • California
  • Coefficients
  • Computer Programming
  • Inequalities
  • Information Science
  • Linear Programming
  • Mathematical Logic
  • Mathematical Programming
  • Mathematics
  • Real Variables
  • Scientific Research
  • Sequences
  • Universities
  • Verification

Readers

  • Graph Algorithms and Convex Optimization.
  • Systems Analysis and Design