Using SMT solvers to verify high-integrity programs

摘要

This volume contains the proceedings of the Second Workshop on Automated Formal Methods held on November 6, 2007, in Atlanta, Georgia, as part of the Automated Software Engineering (ASE) Conference. The first AFM workshop was held as part of the Federated Logic Conference in July 2006 in Seattle, Washington. The focus of the AFM workshop is on topics related to the SRI suite of formal methods tools including PVS, SAL, and Yices. We received 13 submissions of which 9 were accepted for presentation at the workshop. >In addition to the contributed papers, the conference included a presentation by John Rushby on The Road Ahead for PVS, SAL, and Yices, a session of short presentations of ongoing research, and a discussion of open source extensions and enhancements of these verification tools.