Patent Document ID: 8850415
Application ID: 12441889

Base Claim:
1. A non-transitory machine-readable medium storing one or more instructions for generating a labeled transition system for use with model checking of source code in a computer, which when executed by a processor of the computer, cause the processor to perform operations comprising: generating a transition system from the source code; generating an extensible markup language (XML) representation of the source code comprised of nodes, each node having an identifier; generating labels for the transition system to form the labeled transition system by running a query on the XML representation of the source code using query language to return an identifier of a node that matches the query and labeling a node in the transition system identified by the same identifier as the node that matched the query; and using the labels and the structure of the labeled transition system as input to model checking techniques to analyze the source code.

---

Claim 6:
6. The processor performed operations of claim 1 , wherein the operations further comprise initially generating an abstract syntax tree representation of the source code, and wherein the operations of generating the transition system and generating the XML representation of the source code are based on the abstract syntax tree representation of the source code.