Supervisor Meeting 4

By Rice's Theorem any non-trivially property of a program is undecidable. One method to overcome this limitation is abstract interpretation. Despite this no general solution employing this technique exist for the SQL DML

By Rice's Theorem any non-trivially property of a program is undecidable. One method to overcome this limitation is abstract interpretation. Despite theoretical solutions having been proposed for the DML of relational databases, no solutions exist for the triggers. You can't reason about the soundness of your analysis if arbitrary insertions can be made without triggers, thus an analysis of the DML is unsatisfactory.

• Can we use Halder and Cortesi's abstract interpretation framework to define a general SQL DML analysis tool?

• Can we define abstract primitives that are sufficiently expressive for most testing use cases, yet proven to be weak enough to not be affected by Rice's Theorem?

• Can we prove, using Halder and Cortesi's framework, that the tool is sound?

• Can we prove, ..., that the tool derives the best approximations?

• Under which conditions can we prove the tool to be complete?

• Can we create an interface, that allows for quick and easy regression testing?

• Create schema syntax and parser.

• Create a very simple DML syntax and parser.

• Create syntax and parser for the Semantic Integrity Constraint Representation Model to model triggers.

• Define concrete semantics

• Create and implement abstract semantics

• Define primitives

• Abstraction function

• Prove soundness

• Prove termination

• Prove optimal approximation

• Implement Jupyter notebook like interface

• Implement REPL interface