A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
type: Item
instance of: scholarly article
title: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
zbMATH Open document ID: 1115.68051
author: Deepak Kapur
published in: Journal of Systems Science and Complexity
publication date: 2007-05-24T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 5156698
zbMATH Keywords: automated software analysis and verification
zbMATH Keywords: inductive assertion
zbMATH Keywords: loop invariant
zbMATH Keywords: quantifier elimination
describes a project that uses: QEPCAD
describes a project that uses: REDLOG
describes a project that uses: RRL
MaRDI profile type: Publication
full work available at URL: s11424-006-0307-x
OpenAlex ID: W2159289729
cites work: Logical analysis of programs
cites work: Q4411947
cites work: Precise interprocedural analysis through linear algebra
cites work: Static Analysis
cites work: Q4153620
cites work: Basic principles of mechanical theorem proving in elementary geometries
cites work: A refutational approach to geometry theorem proving
cites work: The synthesis of loop predicates
cites work: Affine relationships among variables of a program
cites work: Computer Aided Verification
cites work: Automatic Generation of Polynomial Loop Invariants
cites work: Theoretical Aspects of Computing - ICTAC 2004
cites work: Non-linear loop invariant generation using Gröbner bases
cites work: Comprehensive Gröbner bases
cites work: Applying Linear Quantifier Elimination
cites work: Weak quantifier elimination for the full linear theory of the integers
cites work: Q4221106
cites work: Q4226937
cites work: The complexity of almost linear diophantine problems
cites work: Partial cylindrical algebraic decomposition for quantifier elimination
DOI: 10.1007/S11424-006-0307-X
description: scientific article; zbMATH DE number 5156698