Automated Reasoning About Recursive Programs

Syfte och mål

Syftet med projektet var att undersöka applikationer av automatisk teorembevisning till induktionsbevis, vilka behövs om man vill verifiera rekursiva program (skrivna t.ex. funktionella programmeringsspråk som Haskell). Fokus var på att automatiskt upptäcka extra lemman och generaliseringar vilket annars måste göras av en mänsklig expertanvändare. Vi kom att förbättra state-of-the-art inom induktiv teorembevisning genom att integrera en teknik som kallas theory exploration för att genererara en rikare bakgrundsteori för teorembevisaren.

Resultat och förväntade effekter

Projektets resultat har publicerats i flera artiklar och presenterats på internationella konferenser. Projektet har även lett till två mjukvarusystem, HipSpec och Hipster, som finns tillgänglinga online (open source). Vi har även sammanställt en större mängd benchmarks för att utvärdera och jämföra olika induktiva teorembevisare, som även dessa finns tillgängliga online för andra utvecklare och forskare. Projektet har även lett till nya internationella samarbeten och fortsatta forskningsmedel inom området.

Upplägg och genomförande

När jag började på Chalmers började jag samarbeta med forskare från funktionell-programmerings gruppen. De hade utvecklat ett verktyg för att generera specifikationer för Haskellprogram (QuickSpec), vilket vi kom att integrera med en induktiv teorembevisare i systemet HipSpec. Denna appraoch kallas theory exploration och vi kunde visa att vårt nya system kunde automatisera bevis som tidigare krävt mänsklig hjälp. Att använda theory exploration satte en ny standard för automatiserad induktion och har även inkluderats i andra system.