CPA체커

CPAchecker

CPAchecker는 C 프로그램의 정식 소프트웨어 검증 [1]및 프로그램 분석을 위한 프레임워크 및 도구입니다.예를 들어 게으른 추상화 등의 아이디어와 개념은 소프트웨어 모델 체커 [2]BLAST로부터 계승되었습니다.CPAchecker는 모델 체크와 프로그램 분석을 하나의 형식주의로 표현할 수 있는 개념인 구성 가능한 프로그램 분석 아이디어를 기반으로 합니다.CPAchecker는 실행 시 도달 가능성 분석을 수행합니다.즉, 주어진 규격을 위반하는 특정 상태에 잠재적으로 도달할 수 있는지 여부를 확인합니다.[4]

CPAchecker의 응용 프로그램 중 하나는 Linux 장치 드라이버 [5]검증입니다.

성과

CPAchecker는 2개의 카테고리(전체 및 ControlFlow)에서 1위를 차지했습니다.TACAS 2012에서 개최된 제1회 소프트웨어 검증 대회(2012년)[6]에 참가했습니다.

CPAchecker는 로마 [7]TACAS 2013에서 개최된 제2회 소프트웨어 검증 대회(2013년)에서 1위(전체 카테고리)를 차지했습니다.

아키텍처

CPAchecker는 Control-Flow Automaton(CFA; 제어흐름자동화) 상에서 동작합니다.CPA 알고리즘에 의해 특정 C 프로그램을 분석하기 전에 CFA로 변환됩니다.CFA는 에지가 가정 또는 할당을 나타내고 노드가 프로그램 위치를 나타내는 방향 그래프입니다.

레퍼런스

  1. ^ CPAchecker 공식 웹사이트 : http://cpachecker.sosy-lab.org
  2. ^ Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar (2007). "The Software Model Checker BLAST: Applications to Software Engineering" (PDF). International Journal on Software Tools for Technology Transfer (STTT). 9: 505–525. doi:10.1007/s10009-007-0044-z. S2CID 1662778.
  3. ^ Dirk Beyer and Thomas A. Henzinger and Grégory Théoduloz (2007). "Configurable Software Verification: Concretizing the Convergence of model Checking and program analysis" (PDF). Proceedings of the 19th International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-540-73367-6.
  4. ^ Dirk Beyer and M. Erkan Keremoglu (2011). "CPAchecker: A Tool for Configurable Software Verification" (PDF). Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-642-22109-5.
  5. ^ Linux 드라이버 검증:http://linuxtesting.org/project/ldv
  6. ^ Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)" (PDF). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.
  7. ^ Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)" (PDF). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.

외부 링크