Call for Papers
Pre-proceedings (zip file)
H. Kirchner's invited talk: pdf
R. Schmidt's invited talk: pdf

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 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.


  • Hélène Kirchner, INRIA. Slides
  • Renate Schmidt,University of Manchester. Slides

    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,


    For further information please contact the co-chairs:
    Maria Paola Bonacina
    Università degli Studi di Verona, Italy
    Maribel Fernández
    King's College London, UK