ERC Consolidator Grant für Forschungsprojekt über höherstufiges Theorembeweisen

Prof. Dr. Jasmin Blanchette, Leiter der Lehr- und Forschungseinheit für Theoretische Informatik und Theorembeweisen an der LMU München, hat einen ERC Consolidator Grant für sein Projekt Nekoka: Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification erhalten. Der Grant ermöglicht ihm den Aufbau eines Teams, das die Automatisierung von Beweisen in interaktiven Beweisassistenten und anderen formalen Verifikationswerkzeugen vorantreiben wird.