Systems, methods and media for dynamically shaped tensors using liquid types

A method for verifying source code of a computer program written in a programming language, the method comprising:

• receiving the source code;
• identifying a reference to a tensor variable in the source code;
• compiling the source code to generate a constraint, the constraint specifying that:
• the tensor variable is represented by a first sized array of a sized array data type, the sized array data type being defined by the programming language such that a sized array of the sized array data type comprises:
• a first number of array elements, the first number being one or more;
• an associated type parameter that specifies a type for the array elements, the type parameter being selected from of a plurality of types, the plurality of types including the sized array data type;
• and
• an associated size parameter that specifies a size of the sized array, the size corresponding to the first number;
• and
• generating one or more constraint solutions based on the constraint to verify the source code by:
• using a satisfiability modulo theories (SMT) solver to infer a valid typing for the source code;
• and
• determining whether the generated constraint satisfies the inferred valid typing.