BCVerifier -- A Backward Compatibility Verifier for Java Libraries
==================================================================

Code Repository
---------------

https://softech.cs.uni-kl.de/hg/public/bcverifier

Dependencies
------------

- Java 1.6+ runtime
- [Boogie](http://boogie.codeplex.com/) and its dependencies:
  - [Microsoft .NET](http://www.microsoft.com/net) or [Mono runtime](http://www.mono-project.com/)
  - [Z3](http://z3.codeplex.com/)

The command to run Boogie must be configured in the environment variable $BOOGIE_CMD.

Versions tested:

- Boogie, released on Oct 22, 2012 (version 2.2.30705.1126)
- Z3 version 4.1.2

To adapt the ISL syntax highlighting for the web frontend, the code is [here](http://boogietools.codeplex.com/).

Build System
------------

[Gradle](http://gradle.org/)

For Eclipse integration, use [STS with gradle support](http://static.springsource.org/sts/docs/latest/reference/html/gradle/installation.html)

Main gradle goals:

- jettyRunWar: Runs web frontend locally
- installApp: Installs the application into build/install subdirectory
- distZip: Creates a full distribution ZIP archive including runtime libraries and OS specific scripts in build/distributions subdirectory
- assemble: Assembles all the archives in the project (jar and war), like build but no tests
- test: Runs the test suite
- uploadWar1/2: Deploys web frontend to website

Developer note:

The code to adapt the ISL syntax highlighting for the web frontend is [here](http://boogietools.codeplex.com/).

Website
-------

https://softech.cs.uni-kl.de/bcverifier

Developers
----------

- Mathias Weber <m_weber@cs.uni-kl.de>
- [Yannick Welsch](https://softech.informatik.uni-kl.de/Homepage/YannickWelsch) <welsch@cs.uni-kl.de>
- Peter Zeller <p_zeller@cs.uni-kl.de>

[Software Technology Group, University of Kaiserslautern](http://softech.cs.uni-kl.de)