Loading...
Please wait, while we are loading the content...
Similar Documents
Automated Generation of Loop Invariants by Recurrence Solving in Theorema (2004)
| Content Provider | CiteSeerX |
|---|---|
| Author | Jebelean, Tudor Kovács, Laura Ildikó |
| Description | Proc. of SNASC’04 (Symbolic and Numeric Algorithms for Scientific Computing |
| Abstract | Abstract. Most of the properties established during program verification are either invariants or depend crucially on invariants. The effectiveness of automated verification of (imperative) programs is therefore sensitive to the ease with which invariants, even trivial ones, can be automatically deduced. We present a method for invariant generation that relies on combinatorial techniques, namely on recurrence solving and variable elimination. The effectiveness of the method is demonstrated on examples. |
| File Format | |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Automated Verification Program Verification Combinatorial Technique Recurrence Solving Invariant Generation Loop Invariant Variable Elimination Trivial One |
| Content Type | Text |
| Resource Type | Article |
