We introduce an updated version of the Pono model checker. Pono is a versatile SMT-based model checker that integrates multiple verification algorithms and interfaces with a wide range of SMT solvers through a solver-agnostic back end. It emphasizes usability, offering support for commonly used input formats and providing C++ and Python APIs for programmatic access. The new version 2.0 introduces several important new features, including support for liveness properties, new interpolation-based safety-checking engines, a new VMT-LIB front end, and a number of usability and performance enhancements. An evaluation of the new version demonstrates significant improvements in performance over its previous version and comparable performance to other state-of-the-art model checkers. These results highlight Pono  2.0’s effectiveness as a general-purpose and easily extensible verification platform.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness (Long Tool Paper)

  • Áron Ricardo Perez-Lopez,
  • Po-Chun Chien,
  • Florian Lonsing,
  • Samantha Archer,
  • Ahmed Irfan,
  • Clark Barrett

摘要

We introduce an updated version of the Pono model checker. Pono is a versatile SMT-based model checker that integrates multiple verification algorithms and interfaces with a wide range of SMT solvers through a solver-agnostic back end. It emphasizes usability, offering support for commonly used input formats and providing C++ and Python APIs for programmatic access. The new version 2.0 introduces several important new features, including support for liveness properties, new interpolation-based safety-checking engines, a new VMT-LIB front end, and a number of usability and performance enhancements. An evaluation of the new version demonstrates significant improvements in performance over its previous version and comparable performance to other state-of-the-art model checkers. These results highlight Pono  2.0’s effectiveness as a general-purpose and easily extensible verification platform.