Beagle

Overview

Beagle is an automated verification tool for concurrent systems. The name is chosen to reflect our wishes on the tool: small in size but powerful in finding interesting things (usually bugs in the model), fitting the characteristic of a beagle.

A system in Beagle is modeled as a set of interacting labeled transition systems. Each transition system can be extended with variables. The properties required of the system are specified by temporal logics. Both BDD- and SAT-based model checking algorithms are supported in Beagle. Custom algorithms for verifying labeled transition systems papers [1-4] are also implemented.

The goal of Beagle is to become the back-end model checker for various languages. Support for additional languages can be added by means of plugins.

Beagle is under GPLv2 license.


News

  • 2015-06-30, Beagle Online Editor is released! [TRY IT!]
    • Supports ELTS editing
    • Pure HTML5
    • Supports C programs verification
    • Added a tool to count verification task elements' numbers
    • Added abstraction and refinement framework
    • Added a tool to convert LLVM IR files into ELTS models
  • 2014-04-21, Beagle 1.0 released! [README] [Downloads]
    • Enhancement for ELTS
    • Better performance
    • More clear output
    • Bug fix
  • 2014-01-23, Beagle 0.9 released! [README] [Downloads]

Documentation


Downloads


Publications

  1. VCS: A Verifier for Component-Based Systems

    Fei He, Liangze Yin, Bow-Yao Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2013.

  2. Macro-Step BMC for Compositional Systems

    Liangze Yin, Fei He, Min Zhou, Ming Gu and Jiaguang Sun. Technique report. 2013.09.

  3. Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information

    Liangze Yin, Fei He, Ming Gu. In Theoretical Aspects of Software Engineering (TASE), 2013 Seventh International Symposium on. IEEE, 2013, pp. 23-27.

  4. Reusing Search Tree for Incremental SAT Solving of Temporal Induction

    Liangze Yin, Fei He, Min Zhou, Ming Gu. In International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 85-92.

  5. Clause Replication and Reuse in Incremental Temporal Induction

    Liangze Yin, Fei He, Ming Gu, Jiaguang Sun. Technique report. 2013.06.


Team

  • Fei He, Associate Professor
  • Dexi Wang, PhD Candidate
  • Chao Zhang, PhD Candidate
  • Guang Chen, PhD Candidate
  • You Peng, Bachelor

Many people have contributed to Beagle, they are listed below.

  • Bow-Yaw Wang, Professor
  • Liangze Yin, PhD
  • Lianyi Zhang, Phd Candidate
  • Guanyu Mu, Master
  • Wenrui Meng, Master
  • Wei He, Master
  • Yiyun Miao, Master

Related Projects