Scholarlink

During the past decade of continuous development, the theorem prover Vampire  has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling Vampire to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use Vampire  in practice and review the main changes Vampire has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.

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

The Vampire Diary

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Filip Bártek,
  • Ahmed Bhayat,
  • Robin Coutelier,
  • Márton Hajdu,
  • Matthias Hetzenberger,
  • Petra Hozzová,
  • Laura Kovács,
  • Jakob Rath,
  • Michael Rawson,
  • Giles Reger,
  • Martin Suda,
  • Johannes Schoisswohl,
  • Andrei Voronkov

摘要

During the past decade of continuous development, the theorem prover Vampire  has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling Vampire to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use Vampire  in practice and review the main changes Vampire has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.