Automated Verification of Features with Situation Calculus: FORTE 2004, Madrid

Résultats de recherche: Autre contribution


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.
langue originaleAnglais
Nombre de pages14
Etat de la publicationPublié - 2004

Contient cette citation