Contributors

Since its conception in April 2001, many people have contributed to the success of the AProVE system.

Acknowledgements

Unfortunately, any sufficiently complex software system contains bugs. Our most sincere thanks go to those people that have discovered critical bugs in AProVE, most notably:

• Nao Hirokawa and Aart Middeldorp (authors of the system TTT)
• Hans Zantema and Adam Koprowski (authors of the systems TORPA and TPA)
• Ian Wehrman (member of the Computational Logic group at Washington University)
• Salvador Lucas (author of the system MuTerm)
• Naomi Lindenstrauss (author of the system TermiLog)

3rd party software

AProVE uses the following 3rd party libraries and development tools:

• Albireo:
  The integration of ZGRViewer and the Eclipse GUI is done with the help of the Albireo project. You can find the source code here.
• ANTLR:
  We use this tool to generate parsers for some of the input languages accepted by AProVE.
• Apache ANT:
  ANT is our builder of choice.
• Apache Commons:
  The Codec and IO subprojects are used for Base64 de/encoding and file operations.
• ASM:
  ASM is used as part of of the Bytecode Outline plugin, described below.
• Bytecode Outline:
  Inside the GUI, parts of this project are used to find the correct .class file and method signature.
• CeTA:
  This tool is used in the GUI to certify the automatically generated proofs.
• Clang:
  The Clang compiler is used to compile C programs to the LLVM intermediate representation.
• Eclipse:
  We use this powerful IDE for the development of AProVE.
• FindBugs:
  During development of AProVE, we use FindBugs to find bugs.
• git:
  Our SCM of choice is git.
• GNU getopt:
  We use this Java port of GNU Getopt to parse command line arguments.
• Graphviz:
  We use these tools to view graphs.
• Java:
  AProVE is developed in the Java programming language.
• JDOM:
  JDOM helps AProVE to generate XML files, which are needed for certified termination proofs.
• Jenkins:
  During development, we continuously check for compile errors and bugs using Jenkins.
• KoAT:
  AProVE uses the tool KoAT to analyze the complexity of integer transition systems.
• MiniSAT 2:
  The award-winning SAT solver is used as a backend for various encodings of search problems to SAT.
• OpenJDK:
  We use the basic .class files (e.g. java.lang.Object) from the OpenJDK project as part of our Java Bytecode analysis.
• SableCC:
  The compiler compiler developed by the Sable Group is used to generate parsers for some of the input languages accepted by AProVE.
• Sat4j:
  We use this Java satisfiability library both as a backend for SAT-encoded search problems and to convert Boolean circuits into CNF using Tseitin's algorithm. You can download our modified version here.
• Saxon-HE:
  Saxon is used to convert XML files as part of certified termination proving.
• Timing Framework:
  This framework is used as part of ZGRViewer, described below.
• Yices:
  We use this efficient SMT solver as a backend for several intermediate problems in the handling of integer problems and to search for well-founded orders.
• ZVTM and ZGRViewer:
  We use ZGRViewer (from the ZVTM toolkit) to display graphs in the GUI. You can download our modified version of ZGRViewer here (the remaining parts of ZVTM are left unchanged).
• Z3:
  We use this efficient SMT solver as a backend for non-termination analysis of Java Bytecode.

Current Contributors

• Jürgen Giesl
• Marc Brockschmidt
• Daniel Cloerkes
• Stefan Dollase
• Frank Emrich
• Florian Frohn
• Carsten Fuhs
• Marcel Hark
• Jera Hensel
• David Keller
• Nils Lommen
• Fabian Meyer
• Matthias Naaf
• Peter Schneider-Kamp
• René Thiemann

Past Contributors

• Clemens Adolphs
• Cornelius Aschermann
• Arndt Baars
• Nina Beckmann
• Ralf Behle
• Karsten Behrmann
• Max Berrendorf
• Felix Bier
• Eric Bodden
• Fabian Böller
• Jan Böker
• Andreas Capellmann
• Andrea Crotti
• Thomas Dickmeis
• Darius Dlugosz
• Andrej Dyck
• Burak Emir
• Fabian Emmes
• Tim Enger
• Stephan Falke
• Felix Frei
• Barbara Friemann
• Marina Gluzberg
• Thomas Henn
• Igor Gonopolskiy
• Heike Haegert
• Christian Hang
• Christian Haselbach
• Albert Helligrath
• Matthias Hölzel
• Besnik Ilazi
• Patrick Kabasci
• Christian Käunicke
• Andreas Kelle-Emden
• Sabrina Kielmann
• Marcel Klinzing
• Christian Kuknat
• Fabian Kürten
• Tom Küspert
• Achim Lücking
• Martin Mertens
• Richard Musiol
• Lars Noschinski
• Carsten Otto
• Benedikt Pago
• Michael Parting
• Carsten Pelikan
• Martin Plücker
• Tobias Polock
• Matthias Raffelsieper
• Janine Repke
• Tim Rohlfs
• Ulrich Schmidt-Goertz
• Kristian Scholz
• Matthias Sondermann
• Christian Stein
• Thomas Ströder
• Thies Strothmann
• Stephan Swiderski
• Christian von Essen
• Hermann Walth
• Christoph Weidmann
• Sebastian Weise
• Alexander Weinert
• Patrick Wiehe
• Eugen Yu