Automatic Test Data Generation and Model Checking with CHR

This addresses verification challenges for satellite control software developers, but it is incremental as it applies an existing method to a new domain.

The paper tackled the problem of verifying mission-critical satellite control software by applying Constraint Handling Rules (CHR) to automate test data generation and model checking, resulting in an example application that demonstrates feasibility in this domain.