Automated Synthesis of Scalable Aggregators

Synthesizing high-performance, formally verified aggregators for UNIX command parallelization systems.

Main Directories

• /sysnthesis: Synthesis engine

• /lean4: Utilities components for synthesis and verification

• /benchmarks: Aggregator benchmarking infrastructure, scripts, and inputs

  • simple-infra
  • covid-mts
  • nlp
  • oneliners
  • unix50

• /py-2: Hand-written python aggregator for comparison

• Development Journal

Run Docker

./run-container.sh

Run Benchmarks

See: benchmark directions