[YICES] AFM07 Call for Participation

[Sam Owre]

                        CALL FOR PARTICIPATION
                   AFM07 (Automated Formal Methods)
               November 6, 2007, Atlanta, Georgia, USA
                     http://fm.csl.sri.com/AFM07/

         In association with the 22nd IEEE/ACM International
       Conference on Automated Software Engineering (ASE 2007)
                   http://www.cse.msu.edu/ase2007/

    ***Note: Early registration deadline for ASE 2007 is Oct. 7, 2007***

AFM is a one-day workshop centered around, but not exclusive to, the
SRI suite of tools (PVS, SAL and HybridSAL, and Yices), and
experiences and experiments involving the application, integration,
and extension of these and similar tools focused on highly automated
formal methods.  Participation is open to everyone and all are welcome.

The full program includes nine contributed papers (listed below) selected by
the international program committee, short presentations (five minutes, five
slides) on ongoing work from the user community, and a discussion of
plans and ideas for open source enhancements and extensions to PVS and SAL.  
Please contact the program chairs by Oct 31, 2007, if you wish to make a
short presentation. 

Schedule

9-9.30  : Welcome Address
          John Rushby.
          The Road Ahead for PVS, SAL, and Yices

9.30-10 : Venkatesh Choppella, Arijit Sengupta, Edward Robertson and Steve Johnson.
          Specifying and Verifying Data Models in PVS:
	  Preliminary Explorations using a Text Book Example

10-10.30: David Lester.
          Topology in PVS

10.30-11: COFFEE BREAK

11-11.30: Lee Pike.
          Model Checking for the Practical Verificationist:
	  A User's Perspective on SAL  

11.30-12: Srikanth Mujjiga and Srihari Sukumaran.
          Modelling and test generation using SAL for
	  interoperability testing in Consumer Electronics 

12-12.30: Graham Hughes and Tevfik Bultan.
          Extended Interface Grammars for Automated Stub Generation 

12.30-2 : LUNCH

2-2.30  : Andrew Ireland.
          Cooperative Reasoning for Automatic Software Verification

2.30-3  : Sylvain Conchon, Evelyne Contejean, Johannes Kanig and Stéphane Lescuyer.
          Lightweight Integration of the Ergo Theorem Prover inside a Proof
          Assistant

3-3.30  : Paul Jackson, Bill James Ellis and Kathleen Sharp.
          Using SMT solvers to verify high-integrity programs 

3.30-4  : COFFEE

4-4.30  : Bernd Finkbeiner and Sven Schewe.
          SMT-Based Synthesis of Distributed Systems

4.30-5  : Five Minute Madness -- Short sessions

5-6     : Discussion of Open Source Development and Enhancements
          for PVS and SAL.