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

m |
|||

Line 5: | Line 5: | ||

==Aims and scope== | ==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'' | + | 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 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. |

## Revision as of 15:35, 24 February 2014

A session on software for automated proofs by induction will be held at the 4th International Congress on Mathematical Software (ICMS), August 5(Tue)-9(Sat) 2014, Seoul, Korea, a satellite conference of the International congress of mathematicians.

## 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, in areas such as computer algebra, automated program analysis and automated theorem proving.

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

## Topics

Topics include, non-exhaustively:

- abstract interpretation
- predicate abstraction
- policy iteration
- approaches based Craig interpolation
*k*-induction

## Publications

- A
*short abstract*will appear on the permanent conference web page (see below) as soon as accepted. - An extended abstract will appear on the permanent conference web page (see below) as soon as accepted. It will also appear on the proceedings that will be distributed during the meeting.
- We plan to invite speakers of the session to a special journal issue after the conference (more information about this later).

## Submission guidelines

If you would like to give a talk at ICMS, you need to submit first a short abstract and then later an extended abstract. See the guidelines for the details.

Please note the deadlines :

- March 31 for a short abstract (200 words)
- April 30 for an extended abstract (2-3 pages)

Submissions should be sent to induction2014 AT imag DOT fr, with ICMS in the email title.

After the meeting, the submission guideline for a journal special issue will be communicated to you by the session organizers.