IWS 2012

2nd Joint International Workshop on Strategies
in Rewriting, Proving and Programming
1st July 2012
An IJCAR workshop

Strategies are ubiquitous in automated reasoning engines, high-level programming languages, and verification tools. The useability, performance, and practical impact of these systems depends on the strategy used. Nevertheless, much knowledge about strategies and search plans remains hidden in the implementations of theorem provers, proof assistants, model builders, interpreters, SAT and SMT solvers, decision procedures for satisfiability, termination provers and verifiers.
The Second Joint International Workshop on Strategies in Rewriting, Proving and Programming aims at providing a forum to communicate research about strategies, in order to favour dissemination of knowledge that may remain otherwise accessible only as code; facilitate synergies between the different contexts where strategies are applied, in the neighbouring fields of automated reasoning and programming languages; understand the nature of strategies, their descriptions, properties, usage and behaviour, whether measured empirically or analysed in theory; advance tools, such as strategy languages, for the design of strategies, viewed broadly as means to control modelling, search (e.g., for proofs or models), transformation (e.g., of programs), and access (e.g., to resources).
Since FLoC 2010, where its first edition was held, the Joint International Workshop on Strategies in Rewriting, Proving and Programming (IWS) merges two successful series of worshops: the Strategies in Automated Deduction workshops and the Workshops on Reduction Strategies (WRS).

TOPICS

Topics of interest include, but are not restricted to:

Strategies in automated theorem provers, automated model builders, decision procedures, combinations of decision procedures, SAT-solvers and SMT-solvers.
Strategies and tacticals in interactive theorem provers and proof assistants.
Strategies in interpreters of programming languages, rewriting engines and termination provers.
Strategies in program analysers and tools for verification modulo theories.
Performance evaluation: empirical evaluation, comparison and optimisation of strategies.
Strategy analysis: evaluation, comparison, and optimisation of strategies by mathematical approaches to model search spaces and measure search complexity.
Strategy languages: essential constructs, meta-level features, design, implementation and application.
Applications and case studies where strategies play a major role.

System descriptions and demonstrations are also welcome.

INVITED SPEAKERS

Hélène Kirchner, INRIA. Slides

Renate Schmidt,University of Manchester. Slides

PROGRAMME COMMITTEE

Maria Paola Bonacina, Università degli Studi di Verona (co-chair)

Dan Dougherty, Worcester Polytechnic Institute

Bruno Dutertre, SRI International

Maribel Fernández, King's College London (co-chair)

Mnacho Echenim, Université de Grenoble

Swen Jacobs, EPFL

Salvador Lucas, Universidad Politécnica de Valencia

Christophe Ringeissen, INRIA

Stephan Schulz, eprover.org

FURTHER INFORMATION

For further information please contact the co-chairs:
Maria Paola Bonacina
Università degli Studi di Verona, Italy
Email: mariapaola.bonacina@univr.it
and
Maribel Fernández
King's College London, UK
Email: Maribel.Fernandez@kcl.ac.uk