To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Gallium - 29/09/2006 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                                Amphi Turing

                        Vendredi 29 septembre, 10h30

                            -------------------
                            Richard B. Kieburtz
                            -------------------

  Portland State University and OGI School of Science & Engineering, OHSU

               ==============================================
               Programmed strategies for program verification
               ==============================================


  Plover is an automated property-verifier for Haskell programs that has
  been under development for the past three years as a component of the
  Programatica project.  In Programatica, predicate definitions and property
  assertions written in P-logic, a programming logic for Haskell, can be
  embedded in the text of a Haskell program module.  Plogic properties
  refine the type system of Haskell but cannot be verified by type-checking
  alone; a more powerful logical verifier is needed.  Plover codes the proof
  rules of P-logic, and additionally, embeds strategies and decision
  procedures for their application and discharge.  It integrates a reduction
  system that implements a rewriting semantics for Haskell terms with a
  congruence-closure algorithm that supports reasoning with equality.  It
  can employ splitting strategies to explore alternative valuations of
  expressions of type Bool or other finite data types, but these strategies
  lead to exponential growth of terms and must be employed cautiously.
  Plover itself is written in Stratego, which has proven to be a powerful
  language in which to write a verifier.  This talk will explain the design
  and implementation of some of the strategies that enable Plover to
  comprehend Haskell and to discharge some valid property assertions.