Verification of sequential imperative programs in Isabelle-HOL [Elektronische Ressource] / Norbert Schirmer

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2006
• Nombre de lectures: 18
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

f
f f f
f f f f
f f
f f f
f f f f
f f f
Verification of Sequential Imperative
Programs in Isabelle/HOL
Norbert Schirmer
Lehrstuhl fur¨ Software & Systems Engineering
Institut fur¨ Informatik
Technische Universitat¨ Munchen¨Lehrstuhl fur¨ Software & Systems Engineering
Institut fur¨ Informatik
Technische Universitat¨ Munchen¨
Verification of Sequential Imperative Programs in
Isabelle/HOL
Norbert Schirmer
Vollstandiger¨ Abdruck der von der Fakultat¨ fur¨ Informatik der Technischen
Universitat¨ Munchen¨ zurErlangungdesakademischenGradeseines
DoktorsderNaturwissenschaften(Dr.rer.nat.)
genehmigtenDissertation.
Vorsitzender: Univ. Prof.Dr.HelmutSeidl
Prufer¨ derDissertation: 1.Univ. Prof.TobiasNipkow,Ph.D.
2.Univ. Prof.Dr.WolfgangJ.Paul
UniversitatdesSaarlandes¨
DieDissertationwurdeam31.10.2005beiderTechnischenUniversitatMunchen¨ ¨
eingereichtunddurchdieFakultat¨ fur¨ Informatikam21.04.2006angenommen.i
Kurzfassung
ZielderDissertationistes,eineVerifikationsumgebungfur¨ sequentielleimperative
Programmezuschaffen.Zunachst¨ wirdunabhangig¨ voneinerkonkretenProgram
miersprache ein allgemeines Sprachmodell entwickelt, das ausdrucksstark genug
ist um alle gangigen¨ Programmiersprachkonzepte abzudecken: Gegenseitig rekur-
sive Prozeduren, abrupte Terminierung und Ausnahmebehandlung, Laufzeitfeh
ler, lokale und globale Variablen, Zeiger und Halde, Ausdrucke¨ mit Seiteneffekten,
Zeiger auf Prozeduren, partielle Applikation, dynamischer Methoden Aufruf und
unbeschrankter¨ Indeterminismus.
Fur¨ diesesSprachmodellwirdeineHoareLogiksowohlfur¨ partiellealsauchfur¨
totaleKorrektheitentwickelt.DaraufaufbauendwirdeinVerifikations Bedingungs
Generator implementiert. Die Hoare Logik erlaubt die Integration von statischer
ProgrammanalyseundSoftwareModelCheckernindieVerifikation.
DesweiterenwirdeineTeilsprachevonCindieVerifikationsumgebungeingebet
tet,umdieDurchgangigkeit¨ zueinerrealenProgrammiersprachezudemonstrieren.
Die gesamte Entwicklung wurde im Theorembeweiser Isabelle durchgefuhrt.¨
DadurchwirdzumeinendieKorrektheitmaschinellsichergestelltundzumanderen
stehtnunfur¨ dieVerifikationvonProgrammendiereichhaltigeInfrastruktureiner
vollwertigenunduniversellenBeweisumgebungzurVerfugung.¨iiiii
Abstract
Thepurposeofthisthesisistocreateaverificationenvironmentforsequentialimper-
ativeprograms. Firstagenerallanguagemodelisproposed,whichisindependent
of a concrete programming language but expressive enough to cover all common
language features: mutually recursive procedures, abrupt termination and excep
tions, runtime faults, local and global variables, pointers and heap, expressions
with side effects, pointers to procedures, partial application and closures, dynamic
methodinvocationandalsounboundednondeterminism.
ForthislanguageaHoarelogicforbothpartialandtotalcorrectnessisdeveloped
andontopofitaverificationconditiongeneratorisimplemented. TheHoarelogic
isdesignedtoallowtheintegrationofprogramanalysisorsoftwaremodelchecking
intotheverification.
To demonstrate the continuity to a real programming language a subset of C is
embeddedintotheverificationenvironment.
The whole work is developed in the theorem prover Isabelle. Therefore the
correctnessismachine checkedandinadditiontherichinfrastructureofthegeneral
purposetheoremproverIsabellecanbeemployedfortheverificationofimperative
programs.ivv
Funk is, what you don’t play.
— Maceo Parker
Acknowledgements
I thank Tobias Nipkow for supervising this thesis and giving me the opportunity
to work in his research group. I thank Wolfgang J. Paul for acting as referee and
initiatingtheVerisoftproject.
I am indebted to Amine Chaieb, Gerwin Klein, Martin Strecker and Martin
Wildmoserforreadingandcommentingondraftsofthisthesis.
IalsothankalltheformerandcurrentmembersoftheIsabelleteaminMunich
for the friendly and relaxed working atmosphere, where there is always time for a
coffeebreakanddiscussions: ClemensBallarin(forhiswiseadvise),GertrudBauer,
Stefan Berghofer (for all his support with Isabelle), Amine Chaieb, Florian Haft
mann, Gerwin Klein (for collaboration and friendship even across the continents),
AlexanderKrauss,FarhadMehta,StevenObua(forhispower),DavidvonOheimb,
Leonor Prensa Nieto, Sebastian Skalberg, Martin Strecker (for introducing me to
theorem proving and answering all my questions), Tjark Weber, Markus Wenzel
(forhisidealquestforpropersolutions),andMartinWildmoser.
I thank my parents Anneliese and Jorg, and my girlfriend Sarah Erath for their¨
loveandsupport.vi