본 논문은 부울 제약 조건으로 모델링된 프로그램에서 정보 누출량을 정량적으로 측정하는 정량적 정보 흐름 분석(QIF)에 초점을 맞추고 있다. 특히, 정보 누출량을 정량화하는 방법으로 섀넌 엔트로피를 사용하며, 이를 효율적으로 계산하는 확장 가능한 정확한 도구 PSE를 제시한다. PSE는 Algebraic Decision Diagrams와 결합 분해를 결합한 새로운 지식 컴파일 언어 ADDAND를 사용하여 프로그램의 가능한 출력을 열거하지 않고 섀넌 엔트로피를 계산하며, 출력 확률을 계산하는 모델 카운팅 쿼리 또한 최적화한다. 실험 결과, PSE는 기존 최고 성능의 근사적 도구인 EntropyEstimation보다 459개의 벤치마크 중 56개 더 많은 벤치마크를 해결했으며, 두 도구 모두 해결한 벤치마크의 98%에서 EntropyEstimation보다 최소 10배 이상 효율적임을 보였다.
