|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Study of the properties of hyperpolarized xenon-129 for magnetic resonance imaging
Rychnovský, Jan ; Nováková,, Sabina (oponent) ; Kohout,, jJaroslav (oponent) ; Bartušek, Karel (vedoucí práce)
The production of hyperpolarized gases (HpG), predominantly helium (3He) or xenon (129Xe), have found a steadily increasing range of applications in magnetic resonance imaging (MRI). Neither helium nor xenon are normally present in the body, thus the magnetic resonance experiments do not suffer from unwanted background signals. It has been demonstrated by several techniques of hyperpolarization that the magnetic polarization (magnetization) of the noble gas nuclei can be increased to levels that make practical application feasible. Hence, hyperpolarized gases may become a useful tool for non-invasive investigation of human lung ventilation, permitting static imaging during breathhold or probing the dynamics of inhalation/exhalation, or functional imaging. In inanimate nature, hyperpolarized gas can be used as a contrast medium for microporous materials, such zeolites, constructive materials in civil engineering, etc. This thesis describes the development and construction of a xenon (129Xe) hyperpolarization (Hp) device. Buying hyperpolarized xenon from other research centres abroad is inefficient mainly because of a need of a fast transport of HpXe under specific conditions. That was the main motivation for developing of our own technology for production of HpXe. Well-handled technology could allow a medical cooperation or cooperation with teams dealing with in/animate nature (microporous material, gels, agriculture, animals, etc.). The aim of this work is to study the hyperpolarized noble gases theory with concern to 129Xe and to experimentally prove and measure xenon relaxation times by the NMR. Since it is possible to store hyperpolarized noble gases for later use, this doctoral thesis also explores the potentials of hyperpolarized noble gas storage system and its theoretical and experimental solution. Mainly two types of experiments are described in the thesis. In both experiments, sealed cylindrical Simax sample filled with xenon and supplement gas – nitrogen, helium were used. The first type of experiment is based on thermally polarized xenon and the second on hyperpolarized xenon. For hyperpolarization of 129Xe a high-power laser was used. In this experiment, the relation between power spectral density of optical pumping beam and efficiency of HpXe production process was investigated. The optimal duration of optical pumping and relaxation times of HpXe were investigated too.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Study of the properties of hyperpolarized xenon-129 for magnetic resonance imaging
Rychnovský, Jan ; Nováková,, Sabina (oponent) ; Kohout,, jJaroslav (oponent) ; Bartušek, Karel (vedoucí práce)
The production of hyperpolarized gases (HpG), predominantly helium (3He) or xenon (129Xe), have found a steadily increasing range of applications in magnetic resonance imaging (MRI). Neither helium nor xenon are normally present in the body, thus the magnetic resonance experiments do not suffer from unwanted background signals. It has been demonstrated by several techniques of hyperpolarization that the magnetic polarization (magnetization) of the noble gas nuclei can be increased to levels that make practical application feasible. Hence, hyperpolarized gases may become a useful tool for non-invasive investigation of human lung ventilation, permitting static imaging during breathhold or probing the dynamics of inhalation/exhalation, or functional imaging. In inanimate nature, hyperpolarized gas can be used as a contrast medium for microporous materials, such zeolites, constructive materials in civil engineering, etc. This thesis describes the development and construction of a xenon (129Xe) hyperpolarization (Hp) device. Buying hyperpolarized xenon from other research centres abroad is inefficient mainly because of a need of a fast transport of HpXe under specific conditions. That was the main motivation for developing of our own technology for production of HpXe. Well-handled technology could allow a medical cooperation or cooperation with teams dealing with in/animate nature (microporous material, gels, agriculture, animals, etc.). The aim of this work is to study the hyperpolarized noble gases theory with concern to 129Xe and to experimentally prove and measure xenon relaxation times by the NMR. Since it is possible to store hyperpolarized noble gases for later use, this doctoral thesis also explores the potentials of hyperpolarized noble gas storage system and its theoretical and experimental solution. Mainly two types of experiments are described in the thesis. In both experiments, sealed cylindrical Simax sample filled with xenon and supplement gas – nitrogen, helium were used. The first type of experiment is based on thermally polarized xenon and the second on hyperpolarized xenon. For hyperpolarization of 129Xe a high-power laser was used. In this experiment, the relation between power spectral density of optical pumping beam and efficiency of HpXe production process was investigated. The optimal duration of optical pumping and relaxation times of HpXe were investigated too.
|
|
|
SMV-2013-07: Vypracování a ověření metodiky zobrazení a analýzy animálního modelu schizofrenie prostředky magnetické rezonance v poli 9,4 Tesla a proměření dodaného vzorku
Starčuk jr., Zenon ; Dražanová, Eva ; Jiřík, Radovan ; Rychnovský, Jan ; Starčuková, Jana ; Kořínek, Radim
Na základě smlouvy bylo provedeno posouzení zadaného myšího modelu schizofrenie z hlediska možností zobrazení relevantních parametrů struktury a funkce zadavatelem určených orgánů, byly vyhodnoceny možnosti z hlediska požadavků zadavatele, byla navržena a vypracována metodika zobrazení, byly připraveny a validovány projekty pokusů a navržená metodika byla aplikována na sérii 60 zvířat v souladu s platnými projekty pokusů. Původní i statisticky vyhodnocená data byla předána zadavateli.
|
|
| |
|
| |
|
| |
|
|
Generace a detekce hyperpolarizovaného xenonu
Rychnovský, Jan ; Buchta, Zdeněk
Uvádíme experimentální výsledky výroby a detekce hyperpolarizovaného xenonu získané 4,7 T 200 MHz systémem magnetické rezonance (MR). Xenon 129 byl hyperpolarizován pomocí spinové výměny s rubidiem čerpaným ECL laserem jeho základem je výkonová laserová dioda. ECL laser je optimalizovaný pro dosažení maximální účinnosti procesu optického čerpání atomů rubidia. Užití laserového sytému je orientované k činnosti v experimentální sestavě pro produkci hyperpolarizovaných plynů (HpG), především xenonu. Je navržen pro funkčnost v medicínských a průmyslových aplikacích.
|
|
|
Aparatura pro polarizaci 129Xe - pracovní režimy
Rychnovský, Jan
Hlavním cílem tohoto článku je poskytnout bližší pohled na polarizaci 129Xe, která může být použita v NMR analýze. Nukleární magnetická rezonance - NMR vytváří základ pro elementární spektroskopickou analýzu neznámých látek. Hlavní experiment je stále ve stadiu teoretických příprav. Princip popisovaného systému bude však použit v praxi. Dosáhli jsme výsledků v teoretické přípravě výzkumu a jsou vyřešeny jisté detaily. V neposlední řadě se zmiňuji o operačních modech, které se objevují během polarizace 129Xe.
|
host ::
RSS.