A symbolic model checking appproach to verifying transact-SQL

Today, the trend in software is toward bigger, more complex systems. As a new computational infra-structure has became available, new applications which were previously too expensive or too complex have become common. In this context, the popularization of Relational database management systems (RDBMS) has implied the development of different integrated applications. It makes it possible to develop a simple data repository application or a complex system in which every business rule is implemented, for example, through stored procedures. As the strategic value of software increases for many companies, the industry looks for techniques to automate the production of software and to improve quality and reduce cost and time-to-market. Therefore, new approaches are demanded in order to capture specific errors as a consequence of integrations between applications and databases. The propose of this paper is to present an approach to validate SQL specifications - implemented as Transact-SQL queries or stored procedures - using model checking.