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

Research output: Other contribution

Abstract

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.
Original languageEnglish
Number of pages14
Publication statusPublished - 2004

Keywords

  • feature programming, software verification

Cite this

@misc{ceaca597d48a4fc594ff98b56f6fc8e7,
title = "Automated Verification of Features with Situation Calculus: FORTE 2004, Madrid",
abstract = "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.",
keywords = "feature programming, software verification",
author = "Pascal Urso and Pierre-Yves Schobbens",
year = "2004",
language = "English",
type = "Other",

}

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 -