Automated Analysis and Verification Research Group - VeriFIT

Publications

2017ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt and REZINE Ahmed. An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer. 2017, vol. 5, no. 19, pp. 549-563. ISSN 1433-2779.
 CALINESCU Radu, ČEŠKA Milan, GERASIMOU Simos, KWIATKOWSKA Marta and PAOLETTI Nicola. Designing Robust Software Systems through Parametric Markov Chain Synthesis. In: Proceedings of 14th IEEE International Conference On Software Architecture. To appear in IEEE: IEEE Computer Society, 2017, pp. 131-140. ISBN 978-1-5090-5729-0.
 CARDELLI Luca, ČEŠKA Milan, FRANZLE Martin, KWIATKOWSKA Marta, LAURENTI Luca, PAOLETTI Nicola and WHITBY Max. Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. In: Proceedings of the 29th International Conference on Computer Aided Verification. To appear in LNCS, 2017, pp. 1-20.
 CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony and WU Zhilin. Register Automata with Linear Arithmetic. arXiv:1704.03972, 2017.
 CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony and WU Zhilin. Register Automata with Linear Arithmetic. In: Proceedings of LICS'17. XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX, 2017, pp. 1-12.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design. Berlin: Springer Verlag, 2017, vol. 2017, no. 1, pp. 1-33. ISSN 0925-9856.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Heidelberg: Springer Verlag, 2017, pp. 302-309. ISSN 0302-9743.
 FIEDOR Jan, LOURENCO Joao, SMRČKA Aleš and VOJNAR Tomáš. Verifying Concurrent Programs Using Contracts. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). Tokyo: Institute of Electrical and Electronics Engineers, 2017, pp. 196-206. ISBN 978-1-5090-6032-0.
 FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 2017.
 FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, pp. 407-425. ISBN 978-3-662-54576-8.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0.
 HONG Chih-Duo, CHEN Yu-Fang, LENGÁL Ondřej, MU Shin-Cheng, SINHA Nishant and WANG Bow-Yaw. An Executable Sequential Specification for Spark Aggregation. In: Proceedings of NETYS'17. Heidelberg: Springer Verlag, 2017, pp. 1-15. ISSN 0302-9743.
 LAURENTI Luca, ABATE Alessandro, BORTOLUSSI Luca, CARDELLI Luca, ČEŠKA Milan and KWIATKOWSKA Marta. Reachability Computation for Switching Diffusions:Finite Abstractions with Certifiable and Tuneable Precision. In: Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control. New York: Association for Computing Machinery, 2017, pp. 55-64. ISBN 978-1-4503-4590-3.
 LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak and RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, pp. 499-517. ISBN 978-3-662-46680-3.
 ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch, SEKANINA Lukáš, VAŠÍČEK Zdeněk and VOJNAR Tomáš. Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In: Proceedings of 36th IEEE/ACM International Conference On Computer Aided Design (ICCAD). Irvine, CA: Institute of Electrical and Electronics Engineers, 2017, pp. 416-423. ISBN 978-1-5386-3093-8.
 ČEŠKA Milan, ČEŠKA Milan and PAOLETTI Nicola. Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters. Processing of Sixteenth International Conference on Computer Aided Systems Theory (Extended Abstract). Las Palmas de Gran Canaria, 2017.
2016ABATE Alessandro, ČEŠKA Milan and KWIATKOWSKA Marta. Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. In: Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis. Heidelberg: Springer Verlag, 2016, pp. 1-16. ISBN 978-3-319-46519-7.
 ALDEGHERI Stefano, BARNAT Jiří, BOMBIERI Nicola, BUSATO Federico and ČEŠKA Milan. Parametric Multi-Step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. In: Proceedings of 2nd Workshop on Performance Engineering for Large Scale Graph Analytics. Cham: Springer Verlag, 2016, pp. 519-531. ISBN 978-3-319-58942-8.
 ALMEIDA Ricardo, HOLÍK Lukáš and MAYR Richard. Reduction of Nondeterministic Tree Automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin Heidelberg: Springer Verlag, 2016, pp. 717-735. ISBN 978-3-662-49673-2.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016). Sydney: School of Computer Science and Engineering, University of New South Wales, 2016, pp. 87-93. ISSN 2075-2180.
 CHEN Yu-Fang, HSIEH Chiao, LENGÁL Ondřej, LII Tsung-Ju, TSAI Ming-Hsien, WANG Bow-Yaw and WANG Farn. PAC Learning-Based Verification and Model Synthesis. In: Proceedings of the 38th International Conference on Software Engineering. Austin, TX: Association for Computing Machinery, 2016, pp. 714-724. ISBN 978-1-4503-3900-1.
 DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03. Brno, 2016.
 DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin Heidelberg: Springer Verlag, 2016, pp. 431-452. ISBN 978-3-662-49121-8.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Run Forester, Run Backwards! (Competition Contribution). In: Proceedings of TACAS'16. Heidelberg: Springer Verlag, 2016, pp. 923-926. ISBN 978-3-662-49673-2.
 HOLÍK Lukáš, KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika, TRTÍK Marek and VOJNAR Tomáš. Predator Shape Analysis Tool Suite. In: Proceedings of HVC 2016. Zurich: Springer Verlag, 2016, pp. 202-209. ISBN 978-3-319-49052-6.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, SEKANINA Lukáš, VAŠÍČEK Zdeněk and VOJNAR Tomáš. Towards Formal Relaxed Equivalence Checking in Approximate Computing Methodology. In: 2nd Workshop on Approximate Computing (WAPCO 2016). Prague, 2016, pp. 1-6.
 HOLÍK Lukáš, MEYER Roland and MUSKALLA Sebastian. An Anti Chain-based Approach to Recursive Program Verification. In: Proceedings of International Conference on Networked Systems. Cham: Springer International Publishing, 2016, pp. 322-336. ISBN 978-3-319-26849-1.
 HOLÍK Lukáš, MEYER Roland and MUSKALLA Sebastian. Summaries for Context-Free Games. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, pp. 41-57. ISBN 978-3-95977-027-9.
 IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2016, pp. 71-89. ISBN 978-3-662-49673-2.
 KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika and VOJNAR Tomáš. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In: Proceedings of TACAS 2016. Heidelberg: Springer Verlag, 2016, pp. 942-945. ISBN 978-3-662-49673-2.
 ČEŠKA Milan, PILAŘ Petr, PAOLETTI Nicola, BRIM Luboš and KWIATKOWSKA Marta. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer International Publishing, 2016, pp. 367-384. ISBN 978-3-662-49673-2. ISSN 0302-9743.
2015ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed, RUMMER Philipp and STENMAN Jari. Norn: An SMT Solver for String Constraints. In: Computer Aided Verification. Cham: Springer International Publishing, 2015, pp. 462-469. ISBN 978-3-319-21689-8.
 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. Acta Informatica. 2015, vol. 53, no. 4, pp. 357-385. ISSN 0001-5903.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2015, pp. 193-194. ISBN 978-84-606-5438-4.
 FIEDOR Jan, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. Advances in Noise-based Testing of Concurrent Programs. Software Testing, Verification and Reliability. 2015, vol. 25, no. 3, pp. 272-309. ISSN 1099-1689.
 FIEDOR Jan, LETKO Zdeněk, LOURENCO Joao and VOJNAR Tomáš. Dynamic Validation of Contracts in Concurrent Code. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: The Universidad de Las Palmas de Gran Canaria, 2015, pp. 177-178. ISBN 978-84-606-5438-4.
 FIEDOR Jan, LETKO Zdeněk, LOURENCO Joao and VOJNAR Tomáš. Dynamic Validation of Contracts in Concurrent Code. In: Proceedings of EUROCAST'15. Heidelberg: Springer Verlag, 2015, pp. 555-564. ISBN 978-3-319-27339-6.
 FIEDOR Jan, LETKO Zdeněk, LOURENCO Joao and VOJNAR Tomáš. On Monitoring C/C++ Transactional Memory Programs. In: Proceedings of MEMICS'14. Heidelberg: Springer Verlag, 2015, pp. 73-87. ISBN 978-3-319-14895-3.
 FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 658-674. ISBN 978-3-662-46680-3.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 431-434. ISBN 978-3-662-46680-3.
 MÜLLER Petr, PERINGER Petr and VOJNAR Tomáš. Predator Hunting Party (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 443-446. ISBN 978-3-662-46680-3.

Show all publications

Your IPv4 address: 54.161.3.96
Switch to IPv6 connection

DNSSEC [dnssec]