This volume contains the papers presented at SBMF 2009: the Brazilian S- posium on Formal Methods, held during August 19-21, 2009 in Gramado, Rio Grande do Sul, Brazil. The SBMF programme included three invited talks given by Leonardo de Moura (Microsoft Research), Sebastian Uchitel (University of Buenos Aires and Imperial College London), and Daniel Kro ]ning (University of Oxford). The symposium was accompanied by two short courses: - Introduction to Software Testing, given by Marci o Eduardo Delamaro (U- versity of Sao Paulo) - Formal Models for Automatic Test Case Generation, given by...