Contributors

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

Current Contributors

• Florian Frohn
• Carsten Fuhs
• Jürgen Giesl
• Henri Nagel
• Jan-Christoph Kassing
• Moritz Leven Rosarius
• Nils Lommen
• Eleanore Meyer

Past Contributors

• Clemens Adolphs
• Cornelius Aschermann
• Arndt Baars
• Nina Beckmann
• Ralf Behle
• Karsten Behrmann
• Max Berrendorf
• Felix Bier
• Eric Bodden
• Marc Brockschmidt
• Andreas Capellmann
• Andrea Crotti
• Thomas Dickmeis
• Darius Dlugosz
• Stefan Dollase
• Andrej Dyck
• Fabian Emmes
• Burak Emir
• Frank Emrich
• Tim Enger
• Stephan Falke
• Felix Frei
• Barbara Friemann
• Marina Gluzberg
• Igor Gonopolskiy
• Thomas Henn
• Jera Hensel
• Heike Haegert
• Christian Hang
• Christian Haselbach
• Marcel Hark
• Albert Helligrath
• Matthias Hoelzel
• Besnik Ilazi
• Patrick Kabasci
• Christian Käunicke
• David Keller
• Andreas Kelle-Emden
• Sabrina Kielmann
• Marcel Klinzing
• Christian Kuknat
• Fabian Kürten
• Achim Lücking
• Martin Mertens
• Richard Musiol
• Matthias Naaf
• Lars Noschinski
• Carsten Otto
• Benedikt Pago
• Michael Parting
• Carsten Pelikan
• Martin Plücker
• Matthias Raffelsieper
• Janine Repke
• Tim Rohlfs
• Jonas Säuberlich
• Alexander Schlecht
• Ulrich Schmidt-Goertz
• Peter Schneider-Kamp
• Kristian Scholz
• Matthias Sondermann
• Leon Spitzer
• Christian Stein
• Thomas Ströder
• Thies Strothmann
• Stephan Swiderski
• René Thiemann
• Christian von Essen
• Grigory Vartanyan
• Hermann Walth
• Christoph Weidmann
• Alexander Weinert
• Sebastian Weise
• Patrick Wiehe
• Eugen Yu
• Ivan Zlatin

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 (former 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.