Ústav počítačových systémů

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

Hlavní řešitel:Vojnar Tomáš
Spoluřešitelé:Češka Milan, Dudka Kamil, Fiedor Jan, Fučík Otto, Korček Pavol, Křena Bohuslav, Lengál Ondřej, Letko Zdeněk, Minárik Michal, Peringer Petr, Petrlík Jiří, Rogalewicz Adam, Sekanina Lukáš, Šimáček Jiří, Vašíček Zdeněk
Agentura:VUT v Brně
Kód:FIT-S-12-1
Začátek:2012
Konec:2014
Klíčová slova:formální verifikace, testování a dynamická verifikace, optimalizace, počítačové systémy
Anotace:
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ů.

Produkty

2014HADES (Hazard Detection System), software, 2014
Autoři: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš
 SLIDE: Separační logika s induktivními definicemi, software, 2014
Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
 SPEN - Rozhodovací procedura pro separační logiku, software, 2014
Autoři: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš
2013CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy, software, 2013
Autoři: Müller Petr, Vojnar Tomáš
 Mikroskopický dopravní simulátor založen na celulárním automatu, software, 2013
Autoři: Korček Pavol, Fülöp Tibor
 Systém pro výběr vstupů SVM, software, 2013
Autoři: Petrlík Jiří
2012Prostředí pro analýzu vícevláknových C/C++ programů na binární úrovni, software, 2012
Autoři: Fiedor Jan, Vojnar Tomáš
 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áš

Publikace

2015NEČ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. Vienna: ARGE Simulation News, 2015, s. 389-390. ISBN 978-3-901608-46-9.
 ŠÁ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. Vienna: ARGE Simulation News, 2015, s. 377-378. ISBN 978-3-901608-46-9.
2014ABDULLA 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. Berlin: Springer Verlag, 2014, s. 150-166. ISBN 978-3-319-08866-2.
 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. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
 AVROS Renata, HRUBÁ 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.
 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, 2014, s. 1-4.
 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: Institute of Electrical and Electronics Engineers, 2014, s. 42-48.
 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.
 FIEDOR Tomáš. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. ISBN 978-3-659-63583-0.
 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. 311-318. ISBN 978-1-908320-40-7.
 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. Rím: IEEE Computer Society, 2014, s. 188-193. ISBN 978-1-4799-3531-4.
 HRUBÁ 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. Heidelberg: Springer Verlag, 2014, s. 107-122. ISBN 978-3-319-09939-2.
 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, 2014, s. 1-4.
 KOČÍ Radek a JANOUŠEK Vladimír. Formal Models in Software Development and Deployment: A Case Study. International Journal on Advances in Software. 2014, roč. 7, č. 1, s. 266-276. ISSN 1942-2628.
 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.
 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.
 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, 2014, s. 1-4.
 LUŽA Radim a ZBOŘIL František V. Detection of mechanical play of revolute 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.
 LUŽA Radim, ROZMAN Jaroslav a ZBOŘIL František V. ROS-based Remote Controlled Robotic Arm Workcell. In: Proceedings of ISDA 2014. Okinawa: Institute of Electrical and Electronics Engineers, 2014, s. 101-106. ISBN 978-1-4799-7938-7. ISSN 0000-0000.
 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.
 MRÁČEK Štěpán, DRAHANSKÝ Martin, DVOŘÁK Radim, PROVAZNÍK Ivo 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.
 MÜLLER Petr a VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, s. 395-397. ISBN 978-3-642-54861-1.
 POLÁŠEK Petr, JANOUŠEK Vladimír a ČEŠKA Milan. Petri Net Simulation as a Service. CEUR Workshop Proceedings. 2014, roč. 2014, č. 989, s. 353-362. ISSN 1613-0073.
2013ABDULLA Parosh A., CEDERBERG Jonathan a VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science. 2013, roč. 24, č. 2, s. 187-210. ISSN 0129-0541.
 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.
 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.
 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.
 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. Berlin Heidelberg: Springer Verlag, 2013, s. 460-468. ISBN 978-3-642-53855-1.
 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. Berlin: Springer Verlag, 2013, s. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 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.
 DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, s. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
 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.
 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.
 IOSIF Radu a ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics. Bratislava: Slovak Academic Press, 2013, roč. 2013, č. 4, s. 739-775. ISSN 1335-9150.
 KŘENA Bohuslav a VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems. Abingdon: Taylor & Francis Informa plc, 2013, roč. 2013, č. 42, s. 335-365. ISSN 0308-1079.
 LETKO Zdeněk. Analysis and Testing of Concurrent Programs. Information Sciences and Technologies Bulletin of the ACM Slovakia. Bratislava: Vydavateľstvo STU, 2013, roč. 5, č. 3, s. 1-8. ISSN 1338-1237.
 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). Singapur: IEEE Computational Intelligence Society, 2013, s. 43-50. ISBN 978-1-4673-5869-9.
2012BIDLO 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.
 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.
 FIEDOR Jan a VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science. 2012, roč. 2012, č. 7687, s. 35-41. ISSN 0302-9743.
 FIEDOR Jan a VOJNAR Tomáš. Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In: PADTAD '12. New York: Association for Computing Machinery, 2012, s. 36-46. ISBN 978-1-4503-1456-5.
 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. Berlin: Springer Verlag, 2012, roč. 2012, č. 41, s. 83-106. ISSN 0925-9856.
 HRUBÁ Vendula, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno, 2012.
 HRUBÁ 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. 2012, roč. 2012, č. 7515, s. 152-167. ISSN 0302-9743.
 IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor a RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science. 2012, roč. 2012, č. 7561, s. 187-202. ISSN 0302-9743.
 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. 2012, roč. 2012, č. 7436, s. 247-251. ISSN 0302-9743.
 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.
 KORČEK Pavol, SEKANINA Lukáš a FUČÍK Otto. Calibration of Traffic Simulation Models Using Vehicle Travel Times. Lecture Notes in Computer Science. 2012, roč. 2012, č. 7495, s. 807-816. ISSN 0302-9743.
 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.
 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.
 KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. Brno: Fakulta informačních technologií VUT v Brně, 2012. ISBN 978-80-214-4464-5.
 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.
 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.
 ŠIMKOVÁ 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.
 ŠIMKOVÁ Marcela a LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. Lecture Notes in Computer Science. 2012, roč. 2013, č. 7857, s. 266-273. ISSN 0302-9743.

Vaše IPv4 adresa: 54.166.104.226
Přepnout na IPv6 spojení

DNSSEC [dnssec]