Projects


Here you can find information on all projects completed as part of my Cand.Scient. All project reports are available as either .ps files and/or .pdf files. If you have problems viewing these formats I recommend Ghostscript and GSview for .ps files and Adobe Reader for .pdf files.

Thesis: Type Checking Versus Flow Logics – relations between static analysis methods for cryptographic protocols

Institute of Computer Science:
Dat1 – jSurveyor – et evalueringssystem
Dat2 – LagNa – a programming language for GamNa
Dat3 – The Morphy Project – Distributing a chess game
Dat4 – Symbolic Model Checking in Puzzle Games – Automated Reachability Analysis

Mathematical Institute:
Mat1 – On the Dynamics of a Simple Conservative System
Mat2 – Flow medieret vasodilation – en statistisk analyse

Intro year:
P0 – Usikkerhed i test
P1 – Matematiske modeller for trafik
P2 – Elektronisk afstemning

Project Thesis
Title Type Checking Versus Flow Logics – relations between static analysis methods for cryptographic protocols
Published 12. June 2006
Language English
Abstract In this project we examine the relationship between control flow analysis and type checking. We develop a typed version of the LySa calcu- lus using correspondence assertions, as well as an accompanying type system. We construct an encoding from processes with crypto-points in LySa to Typed LySa, and show that they have equiv- alent safety properties. Type inference is performed on the encoded process under a series of constraints. Lastly a new control flow analysis is created using correspondence assertions instead of crypto-points.
Download Thesis: (pdf) Exam Slides: (pdf)
Project dat4
Title Symbolic Model Checking in Puzzle Games – Automated Reachability Analysis
Published May 2005
Language English
Abstract In this article we apply the technique of model checking to puzzle games. We develop a tool, PUzzle checker for autoMAted reachability analysis (PUMA), to check if puzzles can be solved from some given initial state using reachability analysis. For this purpose we have developed a language to describe models of puzzles and an encoder to translate it into Binary Decision Diagrams representing the model. To combat the state space explosion problem, PUMA uses various heuristics.
Download Report: (pdf) Program: (zip)
Website PUMA
Project dat3
Title The Morphy Project – Distributing a chess game
Published 17. December 2004
Language English
Abstract This report covers the development of a distributed chess engine called Morphy Chess. The goal of the project is to take an existing chess program and modify it to be distributed. The more computing power and memory available, the better the chess program should perform. At the beginning of the report we analyse a number of algorithms for playing chess, including a distribution algorithm named APHID. This is used as the basis idea for the design of a distribution algorithm, and is implemented using the MPI framework. The implementation is in the end evaluated through performance testing.
Download Report: (ps) Source code: (rar)
Website Morphy
Project dat2
Title LagNa – a programming language for GamNa
Published 28. May 2004
Language English
Abstract In this project we develop a programming language for the game GamNa. This is done using Context Free Grammars and operational semantics. Furthermore we develop a verification system following an idea by C. A. R. Hoare and implement a compiler for the language using SableCC. An important aspect in the language design is easy read- and write-ability, we conclude that this has been achieved.
Download Report: (ps) Compiler source: (tar.gz) Engine source: (tar.gz)
Project dat1
Title jSurveyor – et evalueringssystem
Published 19. December 2003
Language Danish
Abstract Denne rapport dokumenterer udviklingen af det web-baserede evalueringssystem jSurveyor. I projektet tages der udgangspunkt i hvordan man kan understøtte håndtering af evalueringer i orskellige sammenhænge, samt at gøre systemet generelt med mulighed for specialisering.I projektet bliver objektorienteret analyse og design brugt i udviklingen af jSurveyor. I implementeringen anvendes Java,
JavaServer Pages, XHTML og MySQL. Derefter bliver jSurveyor underlagt tre brugertests. Til sidst i rapporten bliver reflektioner vedrørende valg og fravalg af teknologi taget op til diskussion./td>
Download Report: (ps) Program: (zip)
Project mat2
Title Flow medieret vasodilation – en statistisk analyse
Published 22. December 2006
Language Danish
Abstract Rapporten er en statistisk analyse af FMD som er rettet mod at bestemme observatørers målepræcision. Efter en introduktion til projektet beskrives, i andet kapitel, den bayesianske tankegang, samt den grundlæggende teori. Denne anvendes på normalfordelingen i det tredje kapitel. I fjerde kapitel indføres teorien om Markov kæder, som indirekte anvendes sidst i sjette kapitel ved konstruktionen af en model, der estimerer varianskomponenter. Femte kapitel er en præsentation af datasættet, samt den bagved liggende forsøgsopstilling, der ligger forud for, at der i sjette kapitel behandles målepræcision for observatørerne ved hjælp af generel lineær model og hypotese test. Syvende kapitel indeholder en undersøgelse af forklarende variables indflydelse på FMD, hvor der anvendes trinvis regression. Rapporten afsluttes med overvejelser angående forbedringer i forsøgsopstillingen.
Download Report: (pdf)
Project mat1
Title On the Dynamics of a Simple Conservative System
Published 12. December 2002
Language English
Abstract The report treats the dynamical system generated by a second-order differential equation arising from Newton’s equation of motion in one dimension. It is shown that the system admits an energy function; existence and uniqueness for general nth-order systems is treated and it is shown that the above system has a unique, globally defined solution. Explicit solutions are obtained, and using these together with the energy function, the fixed points are classified. Finally it is shown that solutions corresponding to negative energies are periodic
Download Report: (ps)
Project p2 – basis
Title Elektronisk afstemning
Published 27. May 2002
Language Danish
Abstract I denne rapport undersøges mulighederne for at indføre elektronisk afstemning via internettet i Danmark som supplement til traditionel afstemning. Dette gøres dels gennem en undersøgelse af de tekniske muligheder, dels ved en analyse af markedet for en sådan afstemningsløsning. I forbindelse med den tekniske redegørelse vil vi opstille en række matematisk-kryptografiske metoder baseret på beregninger i grupper og endelige legemer. Vi vil redegøre for, at en specialiseret kombination af disse metoder gør det muligt at konstruere en afstemningsprotokol. Denne protokol opfylder langt de fleste af de sikkerhedskrav, der er til afstemning og valg i Danmark i dag og på visse områder er mere sikker end traditionelle afstemningsmetoder. Ydermere vil vi argumentere for, at protokollen er et godt udgangspunkt for videre udvikling og kan anvendes direkte i forbindelse med afstemninger og mindre valg.
Igennem markedsanalysen belyses de yderligere forudsætninger for indførelse af elektronisk afstemning, herunder primært vælgerinteressen for løsningen. Vi vurderer, at Danmarks IT-situation og de politiske ambitioner gør elektronisk afstemning til en oplagt mulighed på længere sigt. Endelig vil vi præsentere en mindre spørgeskemaundersøgelse, hvor omtrent halvdelen af responden-terne viste interesse for at stemme via internettet til folketingsvalg. Vi vil udfra undersøgelsen argumentere for, at interessen for elektronisk afstemning bl.a. hænger sammen med erfaring og fortrolighed med computere og internet.
Download Report: (pdf) or (ps)
Project p1 – basis
Title Matematiske modeller for trafik
Published 18. December 2001
Language Danish
Abstract I denne rapport behandles spørgsmålet, hvorvidt det er muligt at opstille anvendelige matematiske modeller for trafik. Dette undersøges udfra en praktisk vinkel, idet en simpel model udvikles fra bunden og vurderes udfra dens forudsigelser i en række semipraktiske situationer. Desuden overvejes modelanvendelsen i Danmark med udgangspunkt i en undersøgelse af trafikplanlæggerens arbejde, og den sammenhæng han indgår i.
Gennem modeldannelsen og den efterfølgende undersøgelse viste vores teoretiske model sig utilstrækkelig i generelle trafiksituationer, men udfra resultaterne vurderede vi, at den som grundlag for mere omfattende modeller var brugbar. Desuden viste det sig, at modelanvendelse i dansk trafikplanlægningen overvejende er begrænset til empiriske og praktiske overvejelser, samt at rent teoretiske modeller i en praktisk situation kun sjældent anvendes.
Download Report: (ps) or (pdf)
Project p0 – basis
Title Usikkerhed i test
Published 21. September 2001
Language Danish
Abstract Denne rapport omhandler emnet: test. Der gives en kort introduktion til forskellige testtyper; dernæst vil vi fokusere særligt på multiple-choice testen og overveje usikkerheden, dels i forbindelse med konstruktionen, dels i forbindelse med analyse af resultaterne. Vi vil endvidere forsøge at opstille grundlaget for en simpel, diskret statistisk model, der kan anvendes i usikkerhedsanalysen både m.h.t. den statistiske usikkerhed og øvrige usikkerhedsaspekter
Download Report: (ps) or (pdf)