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) |