|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Study of the properties of hyperpolarized xenon-129 for magnetic resonance imaging
Rychnovský, Jan ; Nováková,, Sabina (referee) ; Kohout,, jJaroslav (referee) ; Bartušek, Karel (advisor)
Produkce hyperpolarizovaných plynů, především helia (3He) nebo xenonu (129Xe), nachází stále rostoucí rozsah aplikací v zobrazování magnetickou rezonancí (MRI). Helium ani xenon nejsou obyčejně obsaženy v těle a experimenty tedy nejsou ovlivněny nechtěným signálem z okolních tkání. Ukázalo se, že několika hyperpolarizačními technikami může být magnetická polarizace (magnetizace) jader vzácných plynů zvýšena na hladinu, se kterou jsou praktické aplikace proveditelné. Hyperpolarizované plyny mohou tedy být užitečným nástrojem pro neinvazivní zkoumání lidského dýchání, dovolující statické zobrazování během zadržení dechu nebo zkoumání dynamiky výdechu nebo nádechu, nebo funkčního zobrazování. V neživé přírodě, mohou být hyperpolarizovaný plyny využity jako kontrastní látka při studiu mikroporézních materiálů, jako jsou zeolity, stavební látky a hmoty, atd. V této doktorské práci je popsán vývoj a konstrukce aparatury pro hyperpolarizaci xenonu (izotopu 129Xe). Nákup hyperpolarizovaného xenonu od jiných výzkumných center v zahraničí a jeho dovážení by ovšem nebylo efektivní a to zejména z důvodu náročnosti zajištění potřebných fyzikálních podmínek pro přepravu hyperpolarizovaného plynu. Toto bylo hlavní motivací k vývoji vlastní technologie pro přípravu hyperpolarizovaného xenonu. Se zvládnutou technologií by bylo možné navázat spolupráci s medicínskými zařízeními, nebo s týmy zabývající se živou nebo neživou přírodou (např. při studiu mikroporézních materiálů, gelů, v zemědělských aplikacích nebo při výzkumu využívajících zvířat, atd.). Cílem této práce je studium teorie hyperpolarizovaných vzácných plynů se zaměřením na 129Xe a experimentální ověření a změření relaxačních časů pomocí jaderné magnetické rezonance. Vzhledem k tomu, že je možné hyperpolarizované vzácné plyny skladovat pro pozdější využití, se tato práce také zabývá možnostmi zásobníku hyperpolarizovaného vzácného plynu a jeho teoretickým a experimentálním řešením. V této práci jsou popsány především dva základní typy experimentů přípravy hyperpolarizovaného xenonu. V obou jsou využity zatavené válcové skleněné vzorky naplněné xenonem a doplňujícím plynem – dusíkem, heliem. První z experimentů se zabývá měřením vlastností termálně polarizovaného xenonu a druhý měřením vlastností hyperpolarizovaného xenonu. Pro hyperpolarizaci 129Xe bylo použito výkonového laseru a experimentálně byla zkoumána jednak míra polarizace na základě změny spektrální hustoty čerpacího laserového svazku a dále pak optimální doba optického čerpání 129Xe a relaxační časy xenonu.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Study of the properties of hyperpolarized xenon-129 for magnetic resonance imaging
Rychnovský, Jan ; Nováková,, Sabina (referee) ; Kohout,, jJaroslav (referee) ; Bartušek, Karel (advisor)
Produkce hyperpolarizovaných plynů, především helia (3He) nebo xenonu (129Xe), nachází stále rostoucí rozsah aplikací v zobrazování magnetickou rezonancí (MRI). Helium ani xenon nejsou obyčejně obsaženy v těle a experimenty tedy nejsou ovlivněny nechtěným signálem z okolních tkání. Ukázalo se, že několika hyperpolarizačními technikami může být magnetická polarizace (magnetizace) jader vzácných plynů zvýšena na hladinu, se kterou jsou praktické aplikace proveditelné. Hyperpolarizované plyny mohou tedy být užitečným nástrojem pro neinvazivní zkoumání lidského dýchání, dovolující statické zobrazování během zadržení dechu nebo zkoumání dynamiky výdechu nebo nádechu, nebo funkčního zobrazování. V neživé přírodě, mohou být hyperpolarizovaný plyny využity jako kontrastní látka při studiu mikroporézních materiálů, jako jsou zeolity, stavební látky a hmoty, atd. V této doktorské práci je popsán vývoj a konstrukce aparatury pro hyperpolarizaci xenonu (izotopu 129Xe). Nákup hyperpolarizovaného xenonu od jiných výzkumných center v zahraničí a jeho dovážení by ovšem nebylo efektivní a to zejména z důvodu náročnosti zajištění potřebných fyzikálních podmínek pro přepravu hyperpolarizovaného plynu. Toto bylo hlavní motivací k vývoji vlastní technologie pro přípravu hyperpolarizovaného xenonu. Se zvládnutou technologií by bylo možné navázat spolupráci s medicínskými zařízeními, nebo s týmy zabývající se živou nebo neživou přírodou (např. při studiu mikroporézních materiálů, gelů, v zemědělských aplikacích nebo při výzkumu využívajících zvířat, atd.). Cílem této práce je studium teorie hyperpolarizovaných vzácných plynů se zaměřením na 129Xe a experimentální ověření a změření relaxačních časů pomocí jaderné magnetické rezonance. Vzhledem k tomu, že je možné hyperpolarizované vzácné plyny skladovat pro pozdější využití, se tato práce také zabývá možnostmi zásobníku hyperpolarizovaného vzácného plynu a jeho teoretickým a experimentálním řešením. V této práci jsou popsány především dva základní typy experimentů přípravy hyperpolarizovaného xenonu. V obou jsou využity zatavené válcové skleněné vzorky naplněné xenonem a doplňujícím plynem – dusíkem, heliem. První z experimentů se zabývá měřením vlastností termálně polarizovaného xenonu a druhý měřením vlastností hyperpolarizovaného xenonu. Pro hyperpolarizaci 129Xe bylo použito výkonového laseru a experimentálně byla zkoumána jednak míra polarizace na základě změny spektrální hustoty čerpacího laserového svazku a dále pak optimální doba optického čerpání 129Xe a relaxační časy xenonu.
|
|
|
SMV-2013-07: Development and validation of a body of methods for imaging and analysis of an animal model of schizophrenia by 9.4-Tesla magnetic resonance, and analysis of a sample provided
Starčuk jr., Zenon ; Dražanová, Eva ; Jiřík, Radovan ; Rychnovský, Jan ; Starčuková, Jana ; Kořínek, Radim
A contract-based research with a specified mouse model of schizophrenia was carried out, examining the possibility of imaging relevant parameters of the structure and function of organs specified by the client. The options were assessed with respect to client's needs, suitable imaging methodology was identified and developed, animal experiment protocols were prepared and validated, and the proposed methodology was applied to a series of 60 animals according to valid animal use protocols. Original and statistically evaluated data were provided to the client.
|
|
| |
|
| |
|
|
Vliv magnetické susceptibility na T1 relaxace 129Xe.
Bartušek, Karel ; Rychnovský, Jan
Every substance has its own susceptibility, which can affect homogenous magnetic field in magnetic resonance measuring. Local homogenous magnetic field deformation reduces T1 and T2 relaxation times of measured materials. By the laboratory glasses magnetic susceptibilities measurement, we obtained theirs walls influence to thermally polarized 129Xe T1 relaxation times.
|
|
|
Generace a detekce hyperpolarizovaného xenonu
Rychnovský, Jan ; Buchta, Zdeněk
We present the experimental results of generation and detection of hyperpolarized Xenon obtained by 4.7 T, 200 MHz magnetic resonance (MR) system. Xenon 129 was hyperpolarized by the spin-exchange with Rubidium pumped by extended cavity laser system based on a tunable high-power laser diode optimized for maximum efficiency of the optical pumping process. The application of the laser system is oriented to employment in an experimental arrangement for production of hyperpolarized gasses (HpG), namely Xenon. It is designed to operate in medical and industrial applications to come.
|
|
|
The system for 129Xe polarization - the operating modes
Rychnovský, Jan
The main tendency of this paper is to bring a close view of polarization 129Xe that can be used in NMR analyses. Nuclear Magnetic Resonance - NMR, creates a base for an elementary spectroscopic analysis of unknown substances. The main experiment is still in theoretical preparations. But principle of the described system will be used in practice. We have a theoretical attainments about the research and small details are solved. Above all I write about operating modes which will occur during the polarization of 129 Xe.
|
guest ::
