[YICES] AFM07 Call for Participation
owre at csl.sri.com
Sat Oct 6 02:28:44 PDT 2007
CALL FOR PARTICIPATION
AFM07 (Automated Formal Methods)
November 6, 2007, Atlanta, Georgia, USA
In association with the 22nd IEEE/ACM International
Conference on Automated Software Engineering (ASE 2007)
***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
9-9.30 : Welcome Address
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
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.
More information about the YICES