Project Details

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

Project Period: 1. 1. 2012 - 31. 12. 2014

Project Type: grant

Code: FIT-S-12-1

Agency: Brno University of Technology

Program: Vnitřní projekty VUT

English title
Verification and Optimization of Computer Systems
Type
grant
Keywords

formal verification, testing and dynamic verification, optimization, computer systems

Abstract

The project targets verification and optimization of computer-based systems.

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

2015

  • VALENTA Václav, NEČASOVÁ Gabriela, KUNOVSKÝ Jiří, ŠÁTEK Václav and 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, pp. 154-162. ISBN 978-989-758-120-5. Detail
  • KUNOVSKÝ Jiří, ŠÁTEK Václav, VALDMAN Jan and 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, pp. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • VEIGEND Petr, KUNOVSKÝ Jiří, KOCINA Filip, NEČASOVÁ Gabriela, ŠÁTEK Václav and VALENTA Václav. Electronic Representation of Wave Equation. In: 13rd International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, pp. 1-4. ISBN 978-0-7354-1392-4. ISSN 0094-243X. Detail
  • CHALOUPKA Jan, KUNOVSKÝ Jiří, MARTINKOVIČOVÁ Alžbeta, ŠÁTEK Václav and THONHOFER Elvira. Multiple Integral Computations Using Taylor Series. In: 12th International Conference of Numerical Analysis and Applied Mathematics. Rhodes: American Institute of Physics, 2015, pp. 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 and 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, pp. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • KOCINA Filip, KUNOVSKÝ Jiří, MAREK Martin, NEČASOVÁ Gabriela, SCHIRRER Alexander and ŠÁ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, pp. 1-4. ISBN 978-0-7354-1287-3. ISSN 0094-243X. Detail
  • CHALOUPKA Jan, KUNOVSKÝ Jiří, ŠÁTEK Václav, VEIGEND Petr and 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, pp. 163-171. ISBN 978-989-758-120-5. Detail
  • LUŽA Radim, ROZMAN Jaroslav and 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, pp. 101-106. ISBN 978-1-4799-7938-7. Detail
  • NEČASOVÁ Gabriela, KUNOVSKÝ Jiří, ŠÁTEK Václav, CHALOUPKA Jan and 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, pp. 705-706. ISBN 978-3-901608-46-9. Detail
  • ŠÁTEK Václav, KOCINA Filip, KUNOVSKÝ Jiří and 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, pp. 693-694. ISBN 978-3-901608-46-9. Detail

2014

  • MRÁČEK Štěpán, DRAHANSKÝ Martin, DVOŘÁK Radim, PROVAZNÍK Valentine and 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 - Group for computer science, 2014, pp. 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 and HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 2014. Berlin: Springer Verlag, 2014, pp. 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áš and VOLKOVICH Zeev. Boosted Decision Trees for Behaviour Mining of Concurrent Programs. In: Proceedings of MEMICS'14. Brno: NOVPRESS s.r.o., 2014, pp. 15-27. ISBN 978-80-214-5022-6. Detail
  • ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Faculty of Information Technology BUT, 2014. Detail
  • MÜLLER Petr and VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413. Heidelberg: Springer Verlag, 2014, pp. 395-397. ISBN 978-3-642-54861-1. Detail
  • LUŽA Radim and 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ň: Department of Intelligent Systems FIT BUT, 2014, pp. 327-332. ISBN 978-989-758-040-6. Detail
  • MARHEFKA Matúš and 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, pp. 383-389. ISBN 978-0-7695-5194-4. Detail
  • KOČÍ Radek and JANOUŠEK Vladimír. Formal Models in Software Development and Deployment: A Case Study. International Journal on Advances in Software, vol. 7, no. 1, 2014, pp. 266-276. ISSN 1942-2628. Detail
  • KRÁL Jiří, ZBOŘIL František and 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, pp. 56-61. ISBN 978-1-4799-7938-7. Detail
  • HOMOLIAK Ivan, OVŠONKA Daniel, KORANDA Karel and 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, pp. 188-193. ISBN 978-1-4799-3531-4. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana and VOJNAR Tomáš. Multi-objective Genetic Optimization for Noise-Based Testing of Concurrent Software. In: SSBSE'14. Lecture Notes in Computer Science, vol. 8636. Heidelberg: Springer Verlag, 2014, pp. 107-122. ISBN 978-3-319-09939-2. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana and 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 and 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, pp. 310-317. ISBN 978-1-908320-40-7. Detail
  • POLÁŠEK Petr, JANOUŠEK Vladimír and ČEŠKA Milan. Petri Net Simulation as a Service. In: CEUR Workshop Proceedings. Tunisia: CEUR-WS.org, 2014, pp. 353-362. ISSN 1613-0073. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, RUMMER Philipp and STENMAN Jari. String Constraints for Verification. In: 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559, vol. 8559. Berlin: Springer Verlag, 2014, pp. 150-166. ISBN 978-3-319-08866-2. Detail
  • KOČÍ Radek and 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, pp. 309-315. ISBN 978-1-61208-367-4. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš and 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, pp. 83-89. ISBN 978-1-4673-6858-2. Detail

2013

  • CHARVÁT Lukáš, SMRČKA Aleš and 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: The Universidad de Las Palmas de Gran Canaria, 2013, pp. 254-255. ISBN 978-84-695-6971-9. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Computer Aided Systems Theory - EUROCAST 2013. Lecture Notes in Computer Science, vol. 8111. Berlin Heidelberg: Springer Verlag, 2013, pp. 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, vol. 5, no. 3, 2013, pp. 1-8. ISSN 1338-1237. Detail
  • IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics, vol. 2013, no. 4, pp. 739-775. ISSN 1335-9150. Detail
  • KŘENA Bohuslav and VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems, vol. 2013, no. 42, pp. 335-365. ISSN 0308-1079. Detail
  • DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, vol. 20. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013. Detail
  • MINAŘÍK Miloš and 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, pp. 43-50. ISBN 978-1-4673-5869-9. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013. Detail
  • ABDULLA Parosh A., CEDERBERG Jonathan and VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science, vol. 24, no. 2, 2013, pp. 187-210. ISSN 0129-0541. Detail
  • DUDKA Kamil, MÜLLER Petr, PERINGER Petr and 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, vol. 2013. Berlin: Springer Verlag, 2013, pp. 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 and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013. Detail

2012

  • KOŘENEK Jan, KORČEK Pavol, KOŠAŘ Vlastimil, ŽÁDNÍK Martin and 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, pp. 81-82. ISBN 978-1-4503-1684-2. Detail
  • KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp and GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, vol. 2012, no. 7436, pp. 247-251. ISSN 0302-9743. Detail
  • IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor and RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, vol. 2012, no. 7561, pp. 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 and VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science, vol. 2012, no. 7687, pp. 35-41. ISSN 0302-9743. Detail
  • KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. FIT Monograph. Brno: Faculty of Information Technology BUT, 2012. ISBN 978-80-214-4464-5. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš and 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, pp. 6-12. ISBN 978-1-4673-4441-8. Detail
  • KORČEK Pavol, SEKANINA Lukáš and FUČÍK Otto. Calibrating Traffic Simulation Model using Vehicle Travel Times. Lecture Notes in Computer Science, vol. 2012, no. 7495, pp. 807-816. ISSN 0302-9743. Detail
  • PETRLÍK Jiří, KORČEK Pavol, FUČÍK Otto, BESZÉDEŠ Marián and SEKANINA Lukáš. Estimation of traffic density map using evolutionary algorithm. In: Proceedings of the 15th International IEEE Conference on Intelligent Transportation Systems. Anchorage: IEEE Intelligent Transportation Systems Society, 2012, pp. 632-637. ISBN 978-1-4673-3062-6. Detail
  • BIDLO Michal and 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, pp. 1060-1067. ISBN 978-1-4673-1508-1. Detail
  • KORČEK Pavol, SEKANINA Lukáš and 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, pp. 122-129. ISBN 978-1-4673-3062-6. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design, vol. 2012, no. 41, pp. 83-106. ISSN 0925-9856. Detail
  • KORČEK Pavol and ŽÁ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, pp. 278-283. ISBN 978-1-4673-1185-4. Detail
  • FIEDOR Jan and 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, pp. 36-46. ISBN 978-1-4503-1456-5. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk and 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 and VOJNAR Tomáš. Testing of Concurrent Programs with Genetic Algorithms. Lecture Notes in Computer Science, vol. 2012, no. 7515, pp. 152-167. ISSN 0302-9743. Detail
  • ZACHARIÁŠOVÁ Marcela and LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. FIT-TR-2012-03, Brno: Faculty of Information Technology BUT, 2012. Detail
  • ZACHARIÁŠOVÁ Marcela and LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. Lecture Notes in Computer Science, vol. 2013, no. 7857, 2012, pp. 266-273. ISSN 0302-9743. Detail
Products

2014

  • HADES (Hazard Detection System), software, 2014
    Authors: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš Detail
  • SLIDE: Separation Logic with Inductive Definitions, software, 2014
    Authors: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš Detail
  • SPEN - A Solver for Separation Logic Entailments, software, 2014
    Authors: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš Detail

2013

  • CPAlien: Configurable Program Analysis over Symbolic Memory Graphs, software, 2013
    Authors: Müller Petr, Vojnar Tomáš Detail
  • Microscopic CA-based traffic simulator, software, 2013
    Authors: Korček Pavol, Fülöp Tibor Detail
  • SVM Feature Selection System, software, 2013
    Authors: Petrlík Jiří Detail

2012

  • ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, software, 2012
    Authors: Fiedor Jan, Vojnar Tomáš Detail
  • VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, software, 2012
    Authors: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš Detail
Back to top