Automatic verification of concurrent systems using a formula-based compositional approach