Specification Inference Modulo Oracles for Database-Backed Web Applications

Nitesh Trivedi

doi:10.1007/978-981-95-3585-9_10

Return

Specification Inference Modulo Oracles for Database-Backed Web Applications

2026-01-01

PRE

Nitesh Trivedi *

Subhajit Roy

DOI：10.1007/978-981-95-3585-9_10

Original

Original request for help

Save

Abstract

En 中文

In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.

Keywords:

Specification Inference

Oracle

SMT Solvers