This will be the sixth in the Automated Formal Methods (AFM) workshop series. Earlier workshops were AFM06, AFM07, AFM08, AFM09, and AFM10 It is colocated with the NASA Formal Methods (NFM) 2017 symposium. AFM functions both as a user's meeting for SRI's tools such as PVS, SAL, and Yices, and as a workshop for those interested in state of the art automation for formal methods generally.
AFM is a one-day workshop and a one-day tutorial centered around the use and integration of highly automated formal verification tools for specification, interactive theorem proving, satisfiability (SAT) and satisfiability modulo theories (SMT), model checking, program verification, static analysis, runtime verification, code generation, and testing, as well as interfaces, documentation, and education.
This workshop was originally initiated as a users' group meeting for the SRI formal verification tools, which now include PVS, SAL, HybridSAL, SALLY, Yices, NL-Yices, Joogie, Bixie, and SeaHorn, together with technologies under development, such as ARSENAL, Radler, PCE, and ETB However, topics are not restricted to these tools: we welcome contributions on all aspects of state of the art automation.
The program includes contributed papers and invited talks selected by the international program committee.
| 8:30 | Registration and Breakfast |
| 9:00 | Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs |
| 9:30 | The Measurement Library: Representing Physical Types in PVS |
| 10:00 | Moving the Needle on Rigorous Floating-point Precision Tuning |
| 10:30 | Break |
| 11:00 | SMT for state-based formal methods: the ASM case study |
| 11:30 | Building Reusable Verification Technology for
Improving Software Quality |
| 12:00 | On Conflict-Driven Reasoning |
| 12:30 | Lunch |
| 1:30 | More Automated Formal Methods?!
If so, why, where & how? |
| 2:00 | The MINERVA Software Development Process |
| 2:30 | A Brief Introduction to the PVS2C
Code Generator |
| 3:00 | Coffee Break |
| 3:30 | Capability Hardware Enhanced RISC Instructions (CHERI) |
| 4:00 | Arsenal |
| 4:30 | Open discussion |
| 5:30 | Close of Workshop |
| 6:00 | Dinner (Cost is $36 per person) |
The tutorials cover many of the formal methods tools developed at SRI.
| 8:30 | Registration and Breakfast |
| 9:00 | Yices2 Tutorial |
| 10:00 | Break |
| 10:30 | Sally tutorial |
| 11:30 | Seahorn tutorial |
| 12:30 | Lunch |
| 1:30 | PVS tutorial |
| 2:30 | Radler tutorial |
| 3:30 | Break |
| 4:00 | Hybrid SAL, TeLeX, Arsenal |
| 5:30 | End of Tutorials |
| Saddek Bensalem | Verimag |
| Matthew Bolton | Buffalo |
| Maria Paola Bonacina | Verona |
| Alessandro Coglio | Kestrel Institute |
| Bruno Dutertre | SRI, co-Chair |
| Leonard Gerard | SRI |
| Stephane Graham-Lengrand | Ecole Polytechnique |
| Arie Gurfinkel | U. of Waterloo |
| Liana Hadarean | Synopsys |
| Ben Hocking | Dependable Computing |
| Susmit Jha | SRI |
| Dejan Jovanovic | SRI |
| Temesghen Kahsai | CMU West |
| Aditya Kanade | IISc, Bangalore |
| Wenchao Li | Boston University |
| Paolo Masci | Queen Mary |
| Mariano Moscato | NIA |
| Cesar Munoz | NASA Langley |
| Anitha Murugesan | Honeywell Research |
| Jorge Navas | SRI |
| Natasha Neogi | NIA |
| Sam Owre | SRI |
| Lee Pike | Galois |
| Elvinia Riccobene | Milan |
| Kristin Rozier | Iowa |
| John Rushby | SRI |
| Martin Schaef | SRI |
| Natarajan Shankar | SRI, co-Chair |
| Wilfried Steiner | TTTech |
| Ashish Tiwari | SRI |
| Alan Wassyng | McMaster University |