一句话：为 ORM 控制器推断关系代数摘要，并借助现成关系代数求解器验证数据库应用性质。
数据库访问应用常通过 ORM 框架操作持久化对象，直接分析其代码以验证性质较为困难。本文提出一种面向 ORM 控制器的新方法：不直接检查 ORM 代码，而是为每个控制器推断其行为的通用关系代数摘要；随后将摘要交给现成的关系代数求解器，以验证开发者给出的性质或规约。摘要还可辅助程序理解并支持其他应用。作者在基于 Spring 的 MVC 应用中实现了原型工具，并进行了初步评估。实验表明该方法效率较高，在人工受试者给出的一组性质检查中取得了良好结果。
In this work we describe a novel approach for modeling, analysis and verification of database-accessing applications that use the ORM (Object Relational Mapping) paradigm. Rather than directly analyze ORM code to check specific properties, our approach infers a general-purpose relational algebra summary of each controller in the application. This summary can then be fed into any off-the-shelf relational algebra solver to check for properties or specifications given by a developer. The summaries can also aid program understanding, and may have other applications. We have implemented our approach as a prototype tool that works for 'Spring' based MVC applications. A preliminary evaluation reveals that the approach is efficient, and gives good results while checking a set of properties given by human subjects.
@inproceedings{ChawlaAKBK22,
title = {Verification of ORM-based controllers by summary inference},
author = {Geetam Chawla and Navneet Aman and Raghavan Komondoor and Ashish Bokil and Nilesh Kharat},
booktitle = {ICSE},
year = {2022},
doi = {10.1145/3510003.3510148}
}