An approach for modeling and detecting software performance antipatterns based on first-order logics