Applications

Aria supports various applications across testing, verification, synthesis, and optimization.

Testing

Constrained Random Testing: Generate test cases satisfying logical constraints using aria/sampling and aria/allsmt.
Combinatorial Testing: Generate diverse test suites with aria/bool/features for covering parameter interactions.

Verification

Predicate Abstraction: Abstract program states using aria/symabs/predicate_abstraction for verification.
Symbolic Abstraction: Abstract infinite state spaces with aria/symabs for model checking.
Interactive Theorem Proving: Formal verification with aria/itp framework supporting multiple theories.

Synthesis

Program Synthesis: Synthesize programs from specifications using aria/synthesis (SyGuS, PBE).
Syntax-Guided Synthesis: Generate programs matching given grammars with aria/synthesis/sygus_*.

Optimization

Optimization Modulo Theory: Solve optimization problems over logical theories using aria/optimization.
MaxSAT Solving: Solve maximum satisfiability problems with aria/bool/maxsat.

Learning & AI

Machine Learning Features: Extract features for ML-based solver selection with aria/ml.