자동화된 형식 검증 (automated formal verification)의 지형은 현저하게 다른 트레이드오프 (trade-offs)를 가지는 기술들로 채워져 있습니다. 어떤 기술들은 표현력 (expressiveness)과 정밀도 (precision)에 집중하여 복잡한 속성의 검증을 지원하는 반면, 다른 기술들은 확장성 (scalability)과 실용성 (practicality)을 선호하여 다양한 기능을 사용하는 더 큰 프로그램에 적용 가능하도록 합니다. 본 논문은 독특한 트레이드오프를 달성하는 동시성 속성 (concurrency properties)을 위한 새로운 자동화된 검증 기술인 Petrify를 제시합니다. Petrify는 Java 바이트코드 (Java bytecode) 프로그램의 의미론 (semantics)을 Petri nets (PNs)로 인코딩하며, 이는 LoLA와 같은 최첨단 모델 체킹 (model checking) 도구에 의해 분석될 수 있습니다. 우리의 실험이 보여주듯이, Petrify의 접근 방식은 표현력과 실용성의 흥미로운 조합을 제공합니다. 즉, PNs는 프로그램의 동시적 동작 (concurrent behavior)에 대한 상당히 정밀한 인코딩인 동시에, Petrify의 PN 인코딩은 간결하여 분석이 파라미터 크기에 상당히 둔감하게 유지됩니다. 바이트코드를 대상으로 하는 또 다른 실용적인 이점은 Petrify 기술을 구현한 프로토타입 도구인 jPetrify가 다른 유사한 도구들이 오래된 버전의 Java로 제한되는 것과 달리, 모든 버전의 Java로 작성된 프로그램과 심지어 Kotlin (Java 바이트코드로 컴파일되는 또 다른 언어)의 하위 집합에도 적용 가능하다는 점입니다. 본 논문의 실험은 데드락 (deadlock)과 같은 근본적인 속성을 분석하는 데 집중하고 있지만, Petrify의 접근 방식은 다른 종류의 동시성 분석으로 확장하기에 용이하며, 우리는 이를 향후 연구에서 다룰 계획입니다.