APLAS 2025
Mon 27 - Thu 30 October 2025 Bengaluru, India

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 \textit{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 \textit{soundness} and \textit{maximality} of the constructed hypothesis. We implement our algorithm in a tool, WEBSPEC, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. WEBSPEC infers \textit{semantically equivalent} specifications as the ground-truth in all cases.