Verification of database-driven systems via amalgamation
Mikołaj Bojańczyk, Luc Segoufin, Szymon Toruńczyk · 2013
We describe a general framework for static verification of systems that base their decisions upon queries to databases. The database is specified using constraints, typically a schema, and is not modified during a run of the system. The system is equipped with a finite number of registers for storing intermediate information from the database and the specification consists of a transition table described using quantifier-free formulas that can query either the database or the registers.