대부분의 양자 프로그래밍 연구는 양자 프로그램에 대해 이상적이고 노이즈가 없는 (noise-free) 의미론을 고려하는 반면, 본 연구에서는 실제 노이즈가 있는 하드웨어에서 실행되는 양자 프로그램에 대해 추론합니다. 우리는 양자 프로그램에 하드웨어 의존적인 의미론을 부여하기 위해 양자 하드웨어 벤더들이 발표한 오류 모델 (error models)을 고려합니다. 본 연구는 논리적 기초부터 자동화된 검증 및 합성에 이르기까지 노이즈 인지 (noise-aware) 양자 프로그래밍에 대한 포괄적인 연구를 제시합니다. 우리는 노이즈 인지 양자 호어 논리 (quantum Hoare logic)를 개발하였으며, 이를 사용하여 특정 하드웨어에서 양자 프로그램의 유계 검증 (bounded verification)을 위한 알고리즘적 방법과 노이즈 최적화된 루프 없는 (loop-free) 양자 프로그램의 자동 합성을 도출합니다. 이러한 방식으로, 우리는 패리티 체크 (parity checks), 양자 상태 준비 (quantum state preparation), 양자 상태 판별 (quantum state discrimination)과 같이 양자 알고리즘에서 흔히 발생하는 하드웨어 의존적 서브루틴 (subroutines)을 합성합니다. 우리는 IBM Qiskit 툴킷에서 제공하는 하드웨어 사양을 바탕으로 우리의 방법을 평가합니다. 서로 다른 노이즈 모델에 대해 서로 다른 최적의 서브루틴을 찾아내는 것 외에도, 우리의 합성 도구는 양자 프로그래밍의 최적성을 위해 고전적 확률적 분기 (classical probabilistic branching)가 필요함을 보여줍니다.