In the field of speech preprocessing several new methods of robust feature extraction were developed that assure high recognition accuracy in adverse environments. A new speech enhancement algorithm was defined based on spectral subtraction using minimum statistics principles that was further upgraded with the special time-domain additive noise reduction procedure. Further, higher order cumulants properties of the noisy speech signal were inspected. It was shown that LDA classes corresponding to emitting states of the monophone Hidden Markov Models (HMMs) achieve the best automatic speech recognition performance at the lowest feature vector dimensionality. A wavelet transform and the properties of the multiresolutional analysis of the speech signals were inspected. The concept of the noise robust feature extraction algorithm based on joint wavelet packet decomposition and autoregressive modeling was developed and tested. To improve large vocabulary speech recognition, multipass search strategies were applied. We used the three-pass search strategy and a newly developed method for choosing the best hypothesis in the last pass, which was integrated in ROVER algorithm. In the field of continuous speech recognition a new type of subword language model (stem-ending) was defined. The models in great extend solve the problem of out of vocabulary words, typically encountered in Slavic languages. Such models also allow for modelling of words that are not in the vocabulary, but may appear during the speech recognition process. Based on this, a new extended search algorithm was developed and was optimized for sub-word models (stems and endings). We have also developed a new algorithm for splitting words into sub-word units based on lemmas, which can be used in the newly developed search algorithm. The research work in the area of multilingual speech recognition was focused on development of new aglomerative procedure for acoustic model clustering and definition of multilingual acoustic models as well as definition of effective, computation and memory efficient multilingual speech recognition system. Furthermore, we developed a procedure for generation of phonetic broad classes that are needed during the development of acoustic models. A new data driven method is based on similarity measure defined on multilingual phoneme confusion matrix. A new method for transfer of source acoustic models to a new target language was proposed. The similarity between source acoustic models and target language is estimated on the basis of multilingual subphonetic confusion matrix. The main results in the area of formal methods are as follows. EST, an efficient and flexible software package for automatic formal verification of finite-state systems described with a simple process algebra was developed. The package is based on system representation using binary decision diagrams. It allows verification by checking equivalence relations between processes and by model-checking ACTL formulae as well as system fault diagnostics generation. Methods for formal specification of contemporary reactive systems, such as featured telecommunications systems and mobile systems, with SDL and TLA languages were proposed. Algorithms for conversion of SDL system descriptions into the Promela language were developed. Applicability of the EST package and the methods was tested on practical examples. Due to its modular design and flexibility, the EST package is very appropriate to be used for implementation and experimenting with new procedures for automatic formal verification and test sequence generation for hardware and software. Based on the proposed specification methods, special-purpose verification tools, which would be more efficient than the general-purpose ones, could be developed. The SDL to Promela conversion algorithms will enable progress in the development of methods and tools for automated formal verification of telecommunications systems.