Web applications are highly concurrent programs. They are hard to get right due to the complex interactions between agents that may be involved in the same time in several dynamically created transactions, where they might play different roles. This complexity makes also the automatic verification of such programs extremely difficult.
The contribution of Nisarg’s internship work helped
– define a new formal model for web applications allowing dynamic creation of nested transactions,
– develop an algorithmic approach for efficient verification of safety properties of these applications.
The proposed approach is based on checking the robustness against asynchrony of the given program, i.e., whether its concurrent behaviors can be captured by a stronger semantics where transactions are executed according to a particular scheduling policy, reducing significantly the amont of parallelism between transactions, and therefore reducing also the complexity of the verification problem.