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