Contribute to AProVE
AProVE is open source! The source code is available on GitHub under the LGPL-2.1 license. Whether you want to add support for a new input language, implement a new analysis technique, or improve an existing part of the system: Contributions are very welcome! If you have questions about contributing, feel free to contact us.
Ways to Contribute
You do not have to implement a whole new analysis to help the project. The following ideas are a good way to get started.
Report Bugs & Request Features
If AProVE crashes, produces a wrong proof, or cannot handle an input that it should, please open an issue on GitHub. A small example input that triggers the problem helps us a lot.
Join the Discussion
For questions, ideas, and general exchange with the developers and other users, please use the GitHub discussions. This is the best place to propose larger changes before you start implementing them.
Contribute Code
The architecture of AProVE is particularly well suited for adding new input languages to analyze, integrating new proof techniques and new proof strategies, as well as new backend solver integrations. Please read the contributing guide and the code of conduct before opening a pull request.
Contributors
Since its conception in April 2001, many people have contributed to the success of the AProVE system.
Current Contributors
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)
- Cynthia Kop (author of the system WANDA)