|
|
A Bit-Vector Compiler for Data-Flow Graphs
Sušovský, Tomáš ; Lengál, Ondřej (referee) ; Smrčka, Aleš (advisor)
The principal goal of this bachelor thesis is to design and implement a tool for compiling data-flow graph models to SMT-LIB format. This thesis builds on the research project HADES developed by VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The solution uses compiler for generating object model from original graph. Object model can be converted to a SMT-LIB format description including assertions of the desired system properties. Loop unrolling method (with user defined boundary for unrollment) is used for verification of system properties depending on changes in state of model. Capabilities of the developed tool are demonstrated on set of data-flow graphs models. Models cover usage of all elements defined in VAM language (input format) and their combinations. Result of this thesis presents new ways of processing data-flow graphs in VAM format and their verification.
|
|
|
Convolutional Networks for Handwriting Recognition
Sladký, Jan ; Kišš, Martin (referee) ; Hradiš, Michal (advisor)
This thesis deals with handwriting recognition using convolutional neural networks. From the current methods, a network model was chosen to consist of convolutional and recurrent neural networks with the Connectist Temporal Classification. The Vertical Attention Module, which selects the relevant information in each column corresponding to the text in the figure was subsequently implemented in such a model. Then, this module was compared with other possibilities of vertical aggregation between convolutional and recurrent networks. The experiments took place on a data set containing over 80,000 lines of text from Czech letters from the 20th century. The results show that the Vertical Attention Module almost always achieves the best results on all used types of convolution networks. The resulting network achieved the best result with 8,9% of the character error rate. The contribution of this work is a neural network with a newly introduced element that can recognize lines of text.
|
|
|
Convolutional Networks for Handwriting Recognition
Sladký, Jan ; Kišš, Martin (referee) ; Hradiš, Michal (advisor)
This thesis deals with handwriting recognition using convolutional neural networks. From the current methods, a network model was chosen to consist of convolutional and recurrent neural networks with the Connectist Temporal Classification. The Vertical Attention Module, which selects the relevant information in each column corresponding to the text in the figure was subsequently implemented in such a model. Then, this module was compared with other possibilities of vertical aggregation between convolutional and recurrent networks. The experiments took place on a data set containing over 80,000 lines of text from Czech letters from the 20th century. The results show that the Vertical Attention Module almost always achieves the best results on all used types of convolution networks. The resulting network achieved the best result with 8,9% of the character error rate. The contribution of this work is a neural network with a newly introduced element that can recognize lines of text.
|
|
|
A Bit-Vector Compiler for Data-Flow Graphs
Sušovský, Tomáš ; Lengál, Ondřej (referee) ; Smrčka, Aleš (advisor)
The principal goal of this bachelor thesis is to design and implement a tool for compiling data-flow graph models to SMT-LIB format. This thesis builds on the research project HADES developed by VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The solution uses compiler for generating object model from original graph. Object model can be converted to a SMT-LIB format description including assertions of the desired system properties. Loop unrolling method (with user defined boundary for unrollment) is used for verification of system properties depending on changes in state of model. Capabilities of the developed tool are demonstrated on set of data-flow graphs models. Models cover usage of all elements defined in VAM language (input format) and their combinations. Result of this thesis presents new ways of processing data-flow graphs in VAM format and their verification.
|
|
|
The Comparison of Efficiency of Approximate Methods for Solving Transportation Problem
Zárubová, Radka ; Jablonský, Josef (advisor) ; Skočdopolová, Veronika (referee)
The goal of my work is to analyze difference between optimal solution and solution we get when using approximate methods (i.e. NWCM, LCM, VAM). To get necessary data, I have created an application in VBA (both for generating and solving). The application interacts with LINGO. However, its most important parts are procedures for these approximation methods which can be run separately. Therefore, after explaining necessary theory, I focus on approximation methods and explain every single code for them. The last part of my work is the mentioned comparison. In this part, I analyze difference between optimum and approximate solution for five chosen dimensions of transportation tableau. Last but not least, I study whether there is any dependence of difference on number of constrains.
|
guest ::
