First-Order Quantified Separator in Alloy Analyzer

First-Order Logic

Alloy

Example Driven Synthesis

Description and Significance First-order logic is used to express system invarients, but it’s formal complexity hinders wide-scale adoption. During debugging of formal expression, counter-examples are often used to identify cases that have unexpected behavior for a given invariant. These examples can be used to identify what is called a separator – an expression that separates positive and negative examples.

Student Involvement Students will use Alloy – a modeling tool based on first-order and relational logics and transitive closure – to create a separator when given examples. The goal of the project is to identify if using formal methods is a viable method for synthesis of a separator.

Project Results One An successfully submitted a Student Research Competition paper to the Automated Software Engineering Conference of 2025 on Folloy - the tool created to synthesize separators in Alloy.