Detail projektu

Verifikace a optimalizace počítačových systémů

Období řešení: 1. 1. 2012 - 31. 12. 2014

Typ projektu: grant

Kód: FIT-S-12-1

Agentura: Vysoké učení technické v Brně

Program: Vnitřní projekty VUT

Název anglicky
Verification and Optimization of Computer Systems
Typ
grant
Klíčová slova

formální verifikace, testování a dynamická verifikace, optimalizace, počítačové systémy

Abstrakt

Projekt je zaměřen na rozvoj technik automatizované verifikace a optimalizace počítačových systémů, včetně kombinací technik používaných v těchto oblastech. Projekt integruje výzkumné skupiny ze dvou ústavů FIT VUT v Brně. Do projektu jsou významným způsobem zapojeni vybraní doktorandi působící v oblasti verifikace i optimalizace. Významným aspektem projektu je akcentace mezinárodní spolupráce se špičkovými zahraničními pracovišti, vedoucí na společné publikace, projekty a vedení doktorandů.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , spoluřešitel
Dudka Kamil, Ing. (UITS FIT VUT) , spoluřešitel
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Fučík Otto, doc. Dr. Ing. (UPSY FIT VUT) , spoluřešitel
Korček Pavol, Ing., Ph.D. (UPSY FIT VUT) , spoluřešitel
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Letko Zdeněk, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Minárik Michal, Ing. (UITS FIT VUT) , spoluřešitel
Peringer Petr, Dr. Ing. (UITS FIT VUT) , spoluřešitel
Petrlík Jiří, Ing. (UPSY FIT VUT) , spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , spoluřešitel
Sekanina Lukáš, prof. Ing., Ph.D. (UPSY FIT VUT) , spoluřešitel
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Vašíček Zdeněk, doc. Ing., Ph.D. (UPSY FIT VUT) , spoluřešitel
Publikace

2015

  • VALENTA Václav, NEČASOVÁ Gabriela, KUNOVSKÝ Jiří, ŠÁTEK Václav a KOCINA Filip. Adaptive Solution of the Wave Equation. In: Proceedings of the 5th International Conference on Simulation and Modeling Methodologies, Technologies and Applications. Colmar: SciTePress - Science and Technology Publications, 2015, s. 154-162. ISBN 978-989-758-120-5. Detail
  • KUNOVSKÝ Jiří, ŠÁTEK Václav, VALDMAN Jan a VALENTA Václav. Construction of P1 Gradient from P0 Gradient by Averaging. In: 12th International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, s. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • VEIGEND Petr, KUNOVSKÝ Jiří, KOCINA Filip, NEČASOVÁ Gabriela, ŠÁTEK Václav a VALENTA Václav. Electronic Representation of Wave Equation. In: 13rd International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, s. 1-4. ISBN 978-0-7354-1392-4. ISSN 0094-243X. Detail
  • CHALOUPKA Jan, KUNOVSKÝ Jiří, MARTINKOVIČOVÁ Alžbeta, ŠÁTEK Václav a THONHOFER Elvira. Multiple Integral Computations Using Taylor Series. In: 12th International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, s. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • KOCINA Filip, ŠÁTEK Václav, VEIGEND Petr, NEČASOVÁ Gabriela, VALENTA Václav a KUNOVSKÝ Jiří. New Trends in Taylor Series Based Applications. In: 13rd International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, s. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • KOCINA Filip, KUNOVSKÝ Jiří, MAREK Martin, NEČASOVÁ Gabriela, SCHIRRER Alexander a ŠÁTEK Václav. New Trends in Taylor Series Based Computations. In: 12th International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, s. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • CHALOUPKA Jan, KUNOVSKÝ Jiří, ŠÁTEK Václav, VEIGEND Petr a MARTINKOVIČOVÁ Alžbeta. Numerical Integration of Multiple Integrals Using Taylor's Polynomial. In: Proceedings of the 5th International Conference on Simulation and Modeling Methodologies, Technologies and Applications. Colmar: SciTePress - Science and Technology Publications, 2015, s. 163-171. ISBN 978-989-758-120-5. Detail
  • LUŽA Radim, ROZMAN Jaroslav a ZBOŘIL František V. ROS-based Remote Controlled Robotic Arm Workcell. In: International Conference on Intelligent Systems Design and Applications, ISDA. Okinawa: Institute of Electrical and Electronics Engineers, 2015, s. 101-106. ISBN 978-1-4799-7938-7. Detail
  • NEČASOVÁ Gabriela, KUNOVSKÝ Jiří, ŠÁTEK Václav, CHALOUPKA Jan a VEIGEND Petr. Taylor Series Based Differential Formulas. In: MATHMOD VIENNA 2015 - 8th Vienna Conference on Mathematical Modelling. ARGESIM REPORT No. 44. Vienna: ARGE Simulation News, 2015, s. 705-706. ISBN 978-3-901608-46-9. Detail
  • ŠÁTEK Václav, KOCINA Filip, KUNOVSKÝ Jiří a SCHIRRER Alexander. Taylor Series Based Solution of Linear ODE Systems and MATLAB Solvers Comparison. In: MATHMOD VIENNA 2015 - 8th Vienna Conference on Mathematical Modelling. ARGESIM REPORT No. 44. Vienna: ARGE Simulation News, 2015, s. 693-694. ISBN 978-3-901608-46-9. Detail

2014

  • MRÁČEK Štěpán, DRAHANSKÝ Martin, DVOŘÁK Radim, PROVAZNÍK Valentine a VÁŇA Jan. 3D Face Recognition on Low-Cost Depth Sensors. In: Proceedings of the International Conference of Biometrics Special Interest Group (BIOSIG 2014). Darmstadt: GI - Gesellschaft für Informatik e.V., 2014, s. 195-202. ISBN 978-3-88579-624-4. ISSN 1617-5468. Detail
  • FIEDOR Tomáš. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. ISBN 978-3-659-63583-0. Detail
  • ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Lecture Notes in Computer Science, roč. 2014. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743. Detail
  • AVROS Renata, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana, UR Shmuel, VOJNAR Tomáš a VOLKOVICH Zeev. Boosted Decision Trees for Behaviour Mining of Concurrent Programs. In: Proceedings of MEMICS'14. Brno: NOVPRESS s.r.o., 2014, s. 15-27. ISBN 978-80-214-5022-6. Detail
  • ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Fakulta informačních technologií VUT v Brně, 2014. Detail
  • MÜLLER Petr a VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 8413. Heidelberg: Springer Verlag, 2014, s. 395-397. ISBN 978-3-642-54861-1. Detail
  • LUŽA Radim a ZBOŘIL František V. Detection of mechanical play of revolute robot joint. In: ICINCO 2014 Proceedings of the 11th International Conference on Informatics in Control, Automation and Robotics Volume 2. Vídeň: Ústav inteligentních systémů FIT VUT v Brně, 2014, s. 327-332. ISBN 978-989-758-040-6. Detail
  • MARHEFKA Matúš a MÜLLER Petr. Dfuzzer: A D-Bus Service Fuzzing Tool. In: Proceedings of IEEE Seventh International Conference on Software Testing, Verification and Validation Workshopsn. Cleveland: IEEE Computer Society, 2014, s. 383-389. ISBN 978-0-7695-5194-4. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. Formal Models in Software Development and Deployment: A Case Study. International Journal on Advances in Software, roč. 7, č. 1, 2014, s. 266-276. ISSN 1942-2628. Detail
  • KRÁL Jiří, ZBOŘIL František a ZBOŘIL František V. Handling Multiple Intentions Using Action Heuristics. In: Proceedings of the 2014 International Conference on Intelligent Systems Design and Applications. Okinawa: Institute of Electrical and Electronics Engineers, 2014, s. 56-61. ISBN 978-1-4799-7938-7. Detail
  • HOMOLIAK Ivan, OVŠONKA Daniel, KORANDA Karel a HANÁČEK Petr. Characteristics of Buffer Overflow Attacks Tunneled in HTTP Traffic. In: International Carnahan Conference on Security Technology. 48th Annual International Carnahan Conference on Security Technology. Řím: IEEE Computer Society, 2014, s. 188-193. ISBN 978-1-4799-3531-4. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana a VOJNAR Tomáš. Multi-objective Genetic Optimization for Noise-Based Testing of Concurrent Software. In: SSBSE'14. Lecture Notes in Computer Science, roč. 8636. Heidelberg: Springer Verlag, 2014, s. 107-122. ISBN 978-3-319-09939-2. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana a VOJNAR Tomáš. Multi-objective Genetic Optimization for Noise-Based Testing of Concurrent Software. Proceedings of MEMICS'14. Brno, 2014. Detail
  • HOMOLIAK Ivan, OVŠONKA Daniel, GRÉGR Matěj a HANÁČEK Petr. NBA of Obfuscated Network Vulnerabilities' Exploitation Hidden into HTTPS Traffic. In: Proceedings of International Conference for Internet Technology and Secured Transactions (ICITST-2014). London: IEEE Computer Society, 2014, s. 310-317. ISBN 978-1-908320-40-7. Detail
  • POLÁŠEK Petr, JANOUŠEK Vladimír a ČEŠKA Milan. Petri Net Simulation as a Service. In: CEUR Workshop Proceedings. Tunisia: CEUR-WS.org, 2014, s. 353-362. ISSN 1613-0073. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, RUMMER Philipp a STENMAN Jari. String Constraints for Verification. In: 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559, roč. 8559. Berlin: Springer Verlag, 2014, s. 150-166. ISBN 978-3-319-08866-2. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. System Composition Using Petri Nets and DEVS Formalisms. In: The Ninth International Conference on Software Engineering Advances. Nice: Xpert Publishing Services, 2014, s. 309-315. ISBN 978-1-61208-367-4. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014). Austin, TX: IEEE Computer Society, 2014, s. 83-89. ISBN 978-1-4673-6858-2. Detail

2013

  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Proceedings of the 14th Computer Aided Systems Theory. Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2013, s. 254-255. ISBN 978-84-695-6971-9. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Computer Aided Systems Theory - EUROCAST 2013. Lecture Notes in Computer Science, roč. 8111. Berlin Heidelberg: Springer Verlag, 2013, s. 460-468. ISBN 978-3-642-53855-1. Detail
  • LETKO Zdeněk. Analysis and Testing of Concurrent Programs. Information Sciences and Technologies Bulletin of the ACM Slovakia, roč. 5, č. 3, 2013, s. 1-8. ISSN 1338-1237. Detail
  • IOSIF Radu a ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics, roč. 2013, č. 4, s. 739-775. ISSN 1335-9150. Detail
  • KŘENA Bohuslav a VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems, roč. 2013, č. 42, s. 335-365. ISSN 0308-1079. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, roč. 20. Berlin: Springer Verlag, 2013, s. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Fakulta informačních technologií VUT v Brně, 2013. Detail
  • MINAŘÍK Miloš a SEKANINA Lukáš. Concurrent Evolution of Hardware and Software for Application-Specific Microprogrammed Systems. In: 2013 IEEE International Conference on Evolvable Systems (ICES). Proceedings of the 2013 IEEE Symposium Series on Computational Intelligence (SSCI). Singapur: IEEE Computational Intelligence Society, 2013, s. 43-50. ISBN 978-1-4673-5869-9. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, s. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Fakulta informačních technologií VUT v Brně, 2013. Detail
  • ABDULLA Parosh A., CEDERBERG Jonathan a VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science, roč. 24, č. 2, 2013, s. 187-210. ISSN 0129-0541. Detail
  • DUDKA Kamil, MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science Volume 7795, roč. 2013. Berlin: Springer Verlag, 2013, s. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, s. 224-239. ISBN 978-3-319-02443-1. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Fakulta informačních technologií VUT v Brně, 2013. Detail

2012

  • KOŘENEK Jan, KORČEK Pavol, KOŠAŘ Vlastimil, ŽÁDNÍK Martin a VIKTORIN Jan. A New Embedded Platform for Rapid Development of Networking Applications. In: Proceedings of the 2012 Seventh ACM/IEEE Symposium on Architectures for Networking and Communications Systems (ANCS 2012). Austin: IEEE Computer Society, 2012, s. 81-82. ISBN 978-1-4503-1684-2. Detail
  • KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp a GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, roč. 2012, č. 7436, s. 247-251. ISSN 0302-9743. Detail
  • IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor a RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, roč. 2012, č. 7561, s. 187-202. ISSN 0302-9743. Detail
  • LENGÁL Ondřej. An Efficient Finite Tree Automata Library: The Design of BDD-based Semi-symbolic Algorithms for Nondeterministic Finite Tree Automata. Saarbrücken: Lambert Academic Publishing, 2012. ISBN 978-3-659-27069-7. Detail
  • FIEDOR Jan a VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science, roč. 2012, č. 7687, s. 35-41. ISSN 0302-9743. Detail
  • KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. FIT Monograph. Brno: Fakulta informačních technologií VUT v Brně, 2012. ISBN 978-80-214-4464-5. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In: Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012, s. 6-12. ISBN 978-1-4673-4441-8. Detail
  • KORČEK Pavol, SEKANINA Lukáš a FUČÍK Otto. Calibration of Traffic Simulation Models Using Vehicle Travel Times. Lecture Notes in Computer Science, roč. 2012, č. 7495, s. 807-816. ISSN 0302-9743. Detail
  • PETRLÍK Jiří, KORČEK Pavol, FUČÍK Otto, BESZÉDEŠ Marián a SEKANINA Lukáš. Estimation of missing values in traffic density maps. In: Proceedings of the 15th International IEEE Conference on Intelligent Transportation Systems. Anchorage: IEEE Intelligent Transportation Systems Society, 2012, s. 632-637. ISBN 978-1-4673-3062-6. Detail
  • BIDLO Michal a VAŠÍČEK Zdeněk. Evolution of Cellular Automata Using Instruction-Based Approach. In: 2012 IEEE World Congress on Computational Intelligence. CA: Institute of Electrical and Electronics Engineers, 2012, s. 1060-1067. ISBN 978-1-4673-1508-1. Detail
  • KORČEK Pavol, SEKANINA Lukáš a FUČÍK Otto. Evolutionary approach to calibration of cellular automaton based traffic simulation model. In: Proceedings of the 15th International IEEE Conference on Intelligent Transportation Systems. Anchorage: IEEE Intelligent Transportation Systems Society, 2012, s. 122-129. ISBN 978-1-4673-3062-6. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design, roč. 2012, č. 41, s. 83-106. ISSN 0925-9856. Detail
  • KORČEK Pavol a ŽÁDNÍK Martin. Lightweight benchmarking of platforms for network traffic processing. In: Proceedings of the 2012 IEEE 15th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS). Tallin: IEEE Computer Society, 2012, s. 278-283. ISBN 978-1-4673-1185-4. Detail
  • FIEDOR Jan a VOJNAR Tomáš. Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In: PADTAD '12. Proceedings of the 10th Workshop on Parallel and Distributed Systems. New York: Association for Computing Machinery, 2012, s. 36-46. ISBN 978-1-4503-1456-5. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno, 2012. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel a VOJNAR Tomáš. Testování vícevláknových aplikací pomocí genetických algoritmů. Lecture Notes in Computer Science, roč. 2012, č. 7515, s. 152-167. ISSN 0302-9743. Detail
  • ZACHARIÁŠOVÁ Marcela a LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. FIT-TR-2012-03, Brno: Fakulta informačních technologií VUT v Brně, 2012. Detail
  • ZACHARIÁŠOVÁ Marcela a LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. Lecture Notes in Computer Science, roč. 2013, č. 7857, 2012, s. 266-273. ISSN 0302-9743. Detail
Produkty

2014

  • HADES (Hazard Detection System), software, 2014
    Autoři: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš Detail
  • SLIDE: Separační logika s induktivními definicemi, software, 2014
    Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš Detail
  • SPEN - Rozhodovací procedura pro separační logiku, software, 2014
    Autoři: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš Detail

2013

  • CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy, software, 2013
    Autoři: Müller Petr, Vojnar Tomáš Detail
  • Mikroskopický dopravní simulátor založen na celulárním automatu, software, 2013
    Autoři: Korček Pavol, Fülöp Tibor Detail
  • Systém pro výběr vstupů SVM, software, 2013
    Autoři: Petrlík Jiří Detail

2012

  • ANaConDA: Prostředí pro analýzu vícevláknových C/C++ programů na binární úrovni, software, 2012
    Autoři: Fiedor Jan, Vojnar Tomáš Detail
  • VATA: Knihovna pro efektivní práci s nedeterministickými stromovými automaty, software, 2012
    Autoři: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš Detail
Nahoru