# Difference between revisions of "ICMS 2014 session on automated proofs by induction"

(organizer) |
(aims and scope) |
||

Line 1: | Line 1: | ||

==Organizer== | ==Organizer== | ||

[[User:David Monniaux|David Monniaux]], [http://www.cnrs.fr/ CNRS] / [http://www-verimag.imag.fr/~monniaux VERIMAG] | [[User:David Monniaux|David Monniaux]], [http://www.cnrs.fr/ CNRS] / [http://www-verimag.imag.fr/~monniaux VERIMAG] | ||

+ | |||

+ | ==Aims and scope== | ||

+ | In many contexts one proves properties of the form <math>\forall n \in \mathbb{N}~ P(n)</math>. For instance, formal verification of software proves safety'' properties of the form “for any number of program steps, the output satisfies the specification”. | ||

+ | |||

+ | In easy cases, <math>P(n)</math> can be proved by induction: <math>P(0)</math> holds and <math>P(n) \Rightarrow P(n+1)</math> holds for all <math>n</math>. In most cases, however, one must invent some property <math>Q</math> that is “inductive” (<math>Q(0)</math> holds and <math>Q(n) \Rightarrow Q(n+1)</math> holds for all <math>n</math>) and such that <math>Q(n) \Rightarrow P(n)</math> holds. | ||

+ | In software verification, such a property is called an “inductive invariant”. | ||

+ | |||

+ | Over the years, a variety of approaches have been proposed to automatically or semi-automatically obtain inductive properties (model-checking, abstract interpretation, predicate abstraction), with building blocks such as Craig interpolation, Kleene and policy iterations, quantifier elimination etc. | ||

+ | |||

+ | The session aims at bringing together designers of software verification tools and automated theorem provers, and users of these tools. |

## Revision as of 20:20, 13 February 2014

## Organizer

David Monniaux, CNRS / VERIMAG

## Aims and scope

In many contexts one proves properties of the form . For instance, formal verification of software proves safety* properties of the form “for any number of program steps, the output satisfies the specification”.*

In easy cases, can be proved by induction: holds and holds for all . In most cases, however, one must invent some property that is “inductive” ( holds and holds for all ) and such that holds. In software verification, such a property is called an “inductive invariant”.

Over the years, a variety of approaches have been proposed to automatically or semi-automatically obtain inductive properties (model-checking, abstract interpretation, predicate abstraction), with building blocks such as Craig interpolation, Kleene and policy iterations, quantifier elimination etc.

The session aims at bringing together designers of software verification tools and automated theorem provers, and users of these tools.