A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs

Deepak Kapur

doi:10.1007/s11424-006-0307-x

ScienceGate Book Chapters

JOURNAL ARTICLE

A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs

Deepak Kapur

Year: 2006 Journal: Journal of Systems Science and Complexity Vol: 19 (3)Pages: 307-330 Publisher: Springer Science+Business Media

DOI: 10.1007/s11424-006-0307-x

Get Full-Text PDF Get Analytical Report

Keywords:

Quantifier elimination Parameterized complexity Precondition Heuristics Computer science Invariant (physics) Initialization Parametric statistics Heuristic Abstract interpretation Automated theorem proving Mathematical proof Theoretical computer science Algorithm Mathematics Programming language Mathematical optimization Artificial intelligence

Metrics

Cited By

1.33

FWCI (Field Weighted Citation Impact)

Refs

0.80

Citation Normalized Percentile

Is in top 1%

Is in top 10%

Citation History

Topics

Formal Methods in Verification

Physical Sciences → Computer Science → Computational Theory and Mathematics

Logic, programming, and type systems

Physical Sciences → Computer Science → Artificial Intelligence

Software Testing and Debugging Techniques

Physical Sciences → Computer Science → Software

A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs

Metrics

Citation History

Topics

Related Documents

Automatically Generating Loop Invariants Using Quantifier Elimination

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants

Parameterized Verification with Automatically Computed Inductive Assertions?

Heuristic Methods for Mechanically Deriving Inductive Assertions.

Experience with inductive assertions for proving programs correct