Automated Formal Methods (AFM) 2017

May 19 2017 at SRI International, Building G

And May 20, 2017 at Menlo College, Brawner Hall

Moffett Field, CA, USA

In association with 9th NASA Formal Methods Symposium (NFM) 2017

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.

Workshop Description

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.

Workshop Program

The program includes contributed papers and invited talks selected by the international program committee.

Friday, May 19 at SRI International
8:30 Registration and Breakfast
9:00 Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs
Nasrine Damouche and Matthieu Martel
9:30 The Measurement Library: Representing Physical Types in PVS
Ashlie B. Hocking and M. Anthony Aiello
10:00 Moving the Needle on Rigorous Floating-point Precision Tuning
Marek Baranowski, Ian Briggs, Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric and Alexey Solovyev
10:30 Break
11:00 SMT for state-based formal methods: the ASM case study
Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene
11:30 Building Reusable Verification Technology for Improving Software Quality
Jorge Navas
12:00 On Conflict-Driven Reasoning
Maria Paola Bonacina
12:30 Lunch
1:30 More Automated Formal Methods?! If so, why, where & how?
Arun Chakrapani Rao
2:00 The MINERVA Software Development Process
Anthony Narkawicz, Cesar Munoz and Aaron Dutle
2:30 A Brief Introduction to the PVS2C Code Generator
Natarajan Shankar
3:00 Coffee Break
3:30 Capability Hardware Enhanced RISC Instructions (CHERI)
Peter Neumann
4:00 Arsenal
Shalini Ghosh
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.

Saturday, May 20 at Menlo College
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

Program Committee

Saddek BensalemVerimag
Matthew BoltonBuffalo
Maria Paola BonacinaVerona
Alessandro CoglioKestrel Institute
Bruno DutertreSRI, co-Chair
Leonard GerardSRI
Stephane Graham-LengrandEcole Polytechnique
Arie GurfinkelU. of Waterloo
Liana HadareanSynopsys
Ben HockingDependable Computing
Susmit JhaSRI
Dejan JovanovicSRI
Temesghen KahsaiCMU West
Aditya KanadeIISc, Bangalore
Wenchao LiBoston University
Paolo MasciQueen Mary
Mariano MoscatoNIA
Cesar MunozNASA Langley
Anitha MurugesanHoneywell Research
Jorge NavasSRI
Natasha NeogiNIA
Sam OwreSRI
Lee PikeGalois
Elvinia RiccobeneMilan
Kristin RozierIowa
John RushbySRI
Martin SchaefSRI
Natarajan ShankarSRI, co-Chair
Wilfried SteinerTTTech
Ashish TiwariSRI
Alan WassyngMcMaster University

Workshop Organizers


Registration for AFM 2017 is $50 a day (+ 3% for credit card payments). Note that we do not have hotel arrangements. Breakfast, lunch, and breaks are included.
Required fields are marked with a '*'
May 19
May 20