Automated Reasoning
Tarski takes the artifacts and their manually assigned traces as input, and automatically deduces, using the user-defined trace types and their semantics, new traces as output. The solid arrows represent the manually assigned traces, while the dashed arrows are the traces automatically inferred by Tarski. Tarski takes the artifacts and their given and inferred traces as input, and automatically determines, using the user-defined trace types and their semantics, the inconsistent traces as output. Tarski provides an explanation of inconsistent traces by giving all the manually assigned traces causing the inconsistency.