Rajath Mahendrappa Kotyal shows how individually plausible requirements can conflict, using an order and backorder example to illustrate ambiguity before code is written.
He describes a process that refines natural language, translates requirements into logical formulas and checks them with a solverFormal verification uses precisely stated properties and logical methods to check whether a system or argument satisfies those properties.. Multiple translations are compared to reveal different interpretationsEvaluation is the systematic assessment of a system's behaviour or results against explicit criteria..
The tool can ask people to clarify conflicting or underspecified rules, or abstain when it cannot resolve them. Kotyal emphasizes that people remain responsible for correctness and domain knowledge.
Watch on YouTube
