### Abstract

Original language | English |
---|---|

Number of pages | 14 |

Publication status | Published - 2004 |

### Keywords

- feature programming, software verification

### Cite this

}

**Automated Verification of Features with Situation Calculus : FORTE 2004, Madrid.** / Urso, Pascal; Schobbens, Pierre-Yves.

Research output: Other contribution

TY - GEN

T1 - Automated Verification of Features with Situation Calculus

T2 - FORTE 2004, Madrid

AU - Urso, Pascal

AU - Schobbens, Pierre-Yves

PY - 2004

Y1 - 2004

N2 - A well-known way to reason about infinite-state systems is mathematical induction. However, describing such systems for a first-order automated induction prover is a complex task requiring a specialist. To handle this complexity we propose to use the situation calculus as a basis. We deal with the qualification problem by adding a feature construct on top of the situation calculus. We report on a preliminary case study demonstrating the use of our fully automated tool.

AB - A well-known way to reason about infinite-state systems is mathematical induction. However, describing such systems for a first-order automated induction prover is a complex task requiring a specialist. To handle this complexity we propose to use the situation calculus as a basis. We deal with the qualification problem by adding a feature construct on top of the situation calculus. We report on a preliminary case study demonstrating the use of our fully automated tool.

KW - feature programming, software verification

M3 - Other contribution

ER -