In this paper, a technology is presented to use event automata to specify the safety properties of C programs and apply bounded model checking to verify whether a C program satisfies an event automaton property. An event automaton can specify a safety property which is based on the events generated by a program. It can also specify a property with infinite states. Since an event automaton separates from C programs, it will not change the structures of programs. The paper introduces the definition of an automaton reachability tree based on an event automaton. It then uses automaton reachability trees and the bounded model checking to build the SMT (satisfiability modulo theory) models of event automata and C programs. Finally, it supplies the SMT models to an SMT solver. An algorithm for generating counterexamples is obtained according to the results of the solver. The case studies and experimental results demonstrate that the presented approach can verify the event properties of software systems.