Mikoláš Janota

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Mikoláš Janota

Mikoláš Janota

Welcome to my homepage. Currently I am doing my PhD at the UCD Dublin under the supervision of Dr. Joseph Kiniry. I am part of the research group Kind Software. In my research I am focusing on software verification; especially on techniques that exploit mathematical logic.

For current work, please visit the homepage of our research group.

More information follows:

Various documents
Research Examples
Contact
Links

That's me

My Master's Thesis (defended August 2005) .tex, .pdf.gz, .pdf
My Scientific CV myCV.pdf
My Statement of Research Interest aboutme.pdf
My Grades at Charles University M. Sc. program grades.pdf
References used in my Master's Thesis mybib.bib
Slides for my presentation of my Master Thesis (in English) .ps .pdf .tex
Slight extension of slides for my presentation of my Master Thesis (in English) .ps .pdf .tex
Slides for my presentation of my Master Thesis (in Czech) .ps .pdf .tex

Some of my JML examples

JML is an annotation language for java.

Small example, a function that returns maximum of three integers: .html, .java
Two versions of bubble sort extensions, both are verified by ESCJava/2 automatically (run with the "loopSafe" option). html version, .java
Heap, i.e. a binary tree where parent is not greater than its children, stored as an array(children of i: 2i+1, 2i+2). The example contains two methods, one for adding an element, second for popping the root node (minimal value). What we lack here is an invariant that would state that the structure is really a heap. The problem is that different constructs are used in pop and add to express the heap property (children gteq parent vs. parent lteq children). html version, .java

Some of my PVS examples

PVS is a powerful proof assistant, aimed on applications in software verification. Here are some of mine experiments with this tool.
The first example shows soundness of a definition of strongest postcondition for a toy language; the soundness is shown via operational semantics. The other two examples are verifications of bubble-sort and merge-sort; the algorithms are defined as recursive functions inside PVS.
Note: The .ps files do not contain comments

Operational semantics and strongest postcondition propagation for a toy programming language.
Semantics, strongest postcondition and lemmata: prg.pvs,
Definition of program:
State.pvs,
expression.pvs,
expression.pvs,
program.pvs,
eprogram.pvs,
Proof file: prg.prf,
Bubble sort. bubble.tgz, bubble.ps
Merge sort. merge.tgz, merge.ps

Access Counter : 3810 (started on Nov 27 2005)
Local Time: Saturday, February 09, 2008 - 18:24:27 EST