Witness Generation for JSON Schema

JSON Schema is an important, evolving standard schema language for families of JSON documents. It is based on a complex combination of structural operators, Boolean operators, including full negation, and mutually recursive variables. The static analysis of JSON Schema documents comprises practically relevant problems, including schema satisfiability, inclusion, and equivalence. These three can be reduced to witness generation: given a schema, generate an element of the schema -if it exists -otherwise report failure. Schema satisfiability, inclusion, and equivalence have been shown to be decidable, by reduction to reachability in alternating tree automata. However, no witness generation algorithm has yet been formally described. We contribute a first, direct algorithm for JSON Schema witness generation. We study its effectiveness and efficiency, in experiments over several schema collections, including thousands of real-world schemas. Our focus is on the completeness of the language (where we only exclude the "uniqueItems" operator) and on the ability of the algorithm to run in reasonable time on a large set of real-world examples, despite the exponential complexity of the problem.