Equality detection for linear arithmetic constraints

DOI10.1631/jzus.A0820812zbMath1237.91075MaRDI QIDQ621462

Ming Gu, Li Li, Xiaoyu Song, Kai-Duo He

Publication date: 2 February 2011

Published in: Journal of Zhejiang University. Science A (Search for Journal in Brave)

zbMATH Keywords

linear arithmeticmodel checkingsatisfiability modulo theories (SMT)

Mathematics Subject Classification ID

Decision theory (91B06) Linear programming (90C05)

Uses Software

• SIMPLIFY
• CVC Lite
• MathSAT
• CVC
• FOCI
• LPbook

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A canonical form for generalized linear constraints
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Fourier-Motzkin elimination and its dual
• An interpolating theorem prover
• Simplify: a theorem prover for program checking
• Incremental Linear Constraint Solving and Detection of Implicit Equalities
• Computer Aided Verification
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Computer Aided Verification
• Linear programming. Foundations and extensions

This page was built for publication: Equality detection for linear arithmetic constraints