블라스트 모델 체커

BLAST model checker
폭발.
원저작자더크 베이어, 토마스 헨징거, 란짓 잘라, 루팍 마줌다, 버클리
개발자Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, 시스템 프로그래밍 연구소
안정된 릴리스
2.7.3[1] / 2015년 10월 30일, 6년 전(2015-10-30)
기입처OCaml
운영 체제리눅스
유형정적 코드 분석
면허증.Apache 라이센스 버전 2.0
웹 사이트forge.ispras.ru/projects/blast

Berkeley Lazy Abstraction Software Verification Tool(BLAST)은 C 프로그램용 소프트웨어 모델 검사 도구입니다.BLAST에 의해 대처되는 태스크는 소프트웨어가 관련 인터페이스의 동작 요건을 충족하는지 여부를 확인하는 것입니다.BLAST는 반례 중심의 자동 추상화 정교화를 사용하여 추상 모델을 구축한 후 안전 특성을 모델 점검합니다.추상화는 요청된 정밀도로 즉시 구성됩니다.

성과

BLAST는 Talinn에서 [2]열린 TACAS 2012에서 열린 제1회 소프트웨어 검증 경쟁(2012)에서 DeviceDrivers64 부문에서 1위를 차지했습니다.

BLAST는 로마의 [3]TACAS 2013에서 개최된 제2회 소프트웨어 검증 공모전(2013)에서 3위(DeviceDrivers64 카테고리)를 차지했습니다.

BLAST는 그르노블에서 [4]열린 TACAS 2014에서 열린 제3회 소프트웨어 검증 경쟁(2014)에서 DeviceDrivers64 부문에서 1위를 차지했습니다.

레퍼런스

  1. ^ "Files - BLAST - Open-Source Projects".
  2. ^ 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.
  3. ^ 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.
  4. ^ Dirk Beyer (2014). "Third Competition on Software Verification (Summary of SV-COMP 2014)" (PDF). Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.
메모들
  • Pavel Shved; Mikhail Mandrykin; Vadim Mutilin (2012). "Predicate Analysis with BLAST 2.7.". In Flanagan, Cormac; König, Barbara (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 7214. Springer-Verlag. pp. 525–527. ISBN 978-3-642-28756-5.
  • Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The Software Model Checker Blast". International Journal on Software Tools for Technology Transfer. 9 (5–6): 505–525. doi:10.1007/s10009-007-0044-z. S2CID 1662778.
  • Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar & Gregoire Sutre (2003). "Software Verification with Blast". In Ball, Thomas & Rajamani, Sriram K. (eds.). Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science. Vol. 2648. Springer-Verlag. pp. 235–239. ISBN 3-540-40117-2.

외부 링크


Stub icon

이 컴퓨터 기사는 스텁입니다.위키피디아를 확장함으로써 위키피디아를 도울 수 있습니다.