<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=windows-1251">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Preliminary program of Linux Driver Verification Workshop that will
    be held on the 15th of October 2012 in Amirandes, Heraclion, Crete
    is published [1]:<br>
    <br>
    <table>
      <tbody>
        <tr>
          <td colspan="2"><b>09:00 - 10:30 Session 1, Chair: D. Beyer</b>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Linux Device-Drivers Verification Challenges</i><br>
            A. Khoroshilov, V. Mutilin, E. Novikov
            <br>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>BDD-Based Software Model Checking with CPAchecker</i><br>
            A. Stahlbauer
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Pointer Analysis with Uninterpreted Functions</i><br>
            M. Mandrykin
          </td>
        </tr>
        <tr>
          <td colspan="2">
            <b>11:00 - 12:30 Session 2, Chair: A. Petrenko</b>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Using Aspect-Oriented Programming for Preparing C
              Programs for Static Verification</i><br>
            E. Novikov
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Conditional Model Checking and Applications to Driver
              Verification</i><br>
            D. Beyer
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>On Our Way to Apply Model Checking on the Kernel</i><br>
            A. Lissy
          </td>
        </tr>
        <tr>
          <td colspan="2">
            <b>15:00 - 16:30 Session 3, Chair: A. Khoroshilov</b>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Coccinelle: Theory and Practice</i><br>
            J. Lawall
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Explicit-Value Analysis based on CEGAR and
              Interpolation</i><br>
            S. Löwe
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Verification of Linux Device-Driver Code - The
              unsigned int Case</i><br>
            M. Rathgeber, C. Zengler, W. Küchlin
          </td>
        </tr>
        <tr>
          <td colspan="2">
            <b>17:00 - 18:30 Session 4, Chairs: D. Beyer and A. Petrenko</b>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Discussion of Future Directions in Working Groups</i>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Summary Presentation</i>
          </td>
        </tr>
        <tr>
          <td>  </td>
          <td> <i>Closing Remarks</i></td>
        </tr>
      </tbody>
    </table>
    <br>
    [1] <a class="moz-txt-link-freetext" href="http://linuxtesting.org/07-10-2012">http://linuxtesting.org/07-10-2012</a>
  </body>
</html>