Formal Analysis and Verification of Database Query Languages

2/3/2016

By Raju Halder, HASLab/INESC TEC & University of Minho.

Abstract. In this talk, we describe the abstract interpreta- tion of Database Query Languages and its various applications. We formalized a complete denotational semantics, both at concrete and abstract levels, of database applications instrumented with data manipulation language operations such as SELECT, UPDATE, INSERT, DELETE. The theoretical formal framework serves as a foundation of several interesting practical applications, e.g. fine grained access control of data, persistent watermarking, cooperative query answering, etc. In this direction, the issue of semantics-based dependence refinement in database language is also addressed which leads to a more precise analysis of database applications, including program slicing, language-based information flow security analysis, etc. The semantics-based analysis of Hibernate Query Language this way leads to a formal verification of persistent object’s properties as well.

Keywords. Software Engineering, Formal Methods, Database Query Languages.

About the speaker. Raju Halder is currently a re- searcher at HASLab/INESC TEC and University of Minho. He received his Ph.D degree in Computer Science from Ca’ Foscari University of Venice, Italy. Prior to HASLab, Raju was a Post-Doctoral researcher at Macquarie University (Australia) and then joined the Indian Institute of Technology Patna. Before the Ph.D, he also worked at IBM India Pvt. Ltd. Raju is the recipient of “Italian Ministry of Education, Universities and Research (MIUR)” fellowship; he also got two Best Paper Awards at CISIM’11 and ACSS’15. Raju has served as PC member and reveiwer for tens of conferences. His research interests include Abstract Interpretation, Model Checking, Program Analysis and Verification, Databases, etc.

LOCATION AND TIME

Address:  University of Minho, Gualtar campus, Braga, Portugal.

Building. Departamento de Informatica, Building 07.

Coffee session: at 1:30PM-2PM, Sala de Estar, 4th floor.

Talks session: at 2PM-3PM, Sala de Estar, 4th floor.