Tomas Vojnar -- Publications
2021
-
V. Malik and
T. Vojnar.
Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects.
In Proc. of the IEEE International Conference on Software Testing, Verification and Validation 2021---ICST'21,
Ipojuca, Brazil, virtual due to COVID-19.
To be published by IEEE, 2021.
A preliminary version is available here.
The DiffKemp tool is available here.
-
V. Havlena,
L. Holik,
O. Lengal, and
T. Vojnar.
Automata Terms in a Lazy WSkS Decision Procedure.
Journal of Automated Reasoning, 65(7):971--999, 2021.
The first version appeared in the the Proc. of CADE-27.
- L. Charvat,
A. Smrcka, and
T. Vojnar.
Utilizing Parametric Systems for Detection of Pipeline Hazards.
International Journal on Software Tools for Technology Transfer (STTT), XX(XX):XXX--XXX, Springer, XXXX. A preliminary version is available here.
2020
-
L. Turonova,
L. Holik,
O. Lengal,
O. Saarikivi,
M. Veanes, and
T. Vojnar.
Regex Matching with Counting-Set Automata.
In Proc. of the OOPSLA'20 conference, Chicago, USA,
virtual due to COVID-19.
Proceedings of the ACM on Programming Languages, 4(OOPSLA):218:1--218:30, ACM, 2020.
A video presentation is available here.
An extended version is available as the MSR-TR-2020-31 technical report, Microsoft Research, 2020.
-
M. Ceska,
J. Matyas,
V. Mrazek,
L. Sekanina,
Z. Vasicek, and
T. Vojnar.
Adaptive Verifiability-driven Strategy for Evolutionary Approximation of Arithmetic Circuits.
Applied Soft Computing,
95(106466), Elsevier, 2020.
-
V. Havlena,
L. Holik,
O. Lengal,
O. Vales, and
T. Vojnar.
Antiprenexing
for WSkS: A Little Goes a Long Way.
In Proc. of 23rd International Conference on Logic for Programming,
Artificial Intelligence and
Reasoning---LPAR-23,
Alicante, Spain (cancelled due to COVID-19),
volume 73 of EPiC Series in Computing,
pages 298--316, 2020.
-
M. Ceska,
J. Matyas,
V. Mrazek, and
T. Vojnar.
Satisfiability
Solving Meets Evolutionary Optimisation in Designing Approximate Circuits.
In Proc. of 23rd International Conference on Theory and Applications of
Satisfiability Testing---SAT'20,
virtual due to COVID-19,
volume 12178 of LNCS,
pages 481--491, 2020. Springer-Verlag.
-
P. Peringer,
V. Sokova, and
T. Vojnar.
PredatorHP Revamped
(Not Only) for Interval-Sized Memory Regions and Memory Reallocation.
In Proc. of 26th International Conference on Tools and Algorithms for the
Construction and Analysis of
Systems---
as a competition contribution within the
9th International Competition on Software
Verification---SV-COMP'20,
Dublin, Ireland (cancelled due to COVID-19),
volume 12079 of LNCS, pages 408--412, 2020. Springer-Verlag.
The Predator tool is available
here.
-
V. Malik,
P. Schrammel, and
T. Vojnar.
2LS: Heap Analysis and
Memory Safety.
In Proc. of 26th International Conference on Tools and Algorithms for the
Construction and Analysis of
Systems---
as a competition contribution within the
9th International Competition on Software
Verification---SV-COMP'20,
Dublin, Ireland (cancelled due to COVID-19),
volume 12079 of LNCS, pages 368--372, 2020. Springer-Verlag.
The 2LS tool is available here.
-
M. Chalupa,
T. Jasek,
L. Tomovic,
M. Hruska,
V. Sokova,
P. Ayaziova,
J. Strejcek, and
T. Vojnar.
Symbiotic 7: Integration
of Predator and More.
In Proc. of 26th International Conference on Tools and Algorithms for the
Construction and Analysis of
Systems---
as a competition contribution within the
9th International Competition on Software
Verification---SV-COMP'20,
Dublin, Ireland (cancelled due to COVID-19),
volume 12079 of LNCS, pages 413--417, 2020. Springer-Verlag.
The Symbiotic tool is available here.
-
L. Holik,
R. Iosif,
A. Rogalewicz, and
T. Vojnar.
Abstraction Refinement
for Trace Inclusion of Infinite State Systems.
Formal Methods in System Design,
55(3):137--170, Springer, 2020.
An extended abstract appeared in the the Proc. of TACAS'16.
A preliminary version is available at arXiv with the id
1410.5056.
A prototype implementation is available in the tool called
INCLUDER (tracer).
- M. Ceska,
V. Havlena,
L. Holik,
O. Lengal, and
T. Vojnar.
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection.
International Journal on Software Tools for Technology Transfer (STTT), 22(5):523--539, Springer, 2020. An extended abstract appeared in the the Proc. of TACAS'18. A preliminary version is available here.
2019
-
L. Holik,
O. Lengal,
O. Saarikivi,
L. Turonova,
M. Veanes, and
T. Vojnar.
Succinct Determinisation of Counting Automata via Sphere Construction.
In Proc. of 17th Asian Symposium on Programming Languages and
Systems---APLAS'19,
Bali, Indonesia, volume 11893 of LNCS, pages 468--489, 2019. Springer-Verlag.
A preliminary version is available
here.
-
Y.-F. Chen,
C.-Y. Chiang,
L. Holik,
W.-T. Kao,
H.-H. Lin,
T. Vojnar,
Y.-F. Wen, and
W.-C. Wu.
J-ReCoVer: Java Reducer Commutativity Verifier.
In Proc. of 17th Asian Symposium on Programming Languages and
Systems---APLAS'19,
Bali, Indonesia, volume 11893 of LNCS, pages 357--366, 2019. Springer-Verlag.
A preliminary version is available
here.
The J-ReCoVer tool is available here.
-
V. Havlena, L. Holik, O. Lengal, and T. Vojnar.
Automata Terms in a Lazy WSkS Decision
Procedure.
In Proc. of the 27th International Conference on Automated
Deduction---CADE-27,
Natal, Brazil, volume 11716 of LNCS, pages 300--318, 2019. Springer-Verlag.
The best paper award of CADE-27.
An extended version appeared as the technical report
CoRR abs/1905.08697, 2019.
-
M. Ceska, V. Havlena, L. Holik, J. Korenek, O. Lengal, D. Matousek, J. Matousek, J. Semric, and
T. Vojnar.
Deep Packet Inspection in FPGAs via Approximate
Nondeterministic Automata.
In Proc. of 27th IEEE International Symposium On Field-Programmable Custom Computing
Machines---FCCM'19, San
Diego, USA, pages 109--117, 2019.
IEEE.
An extended version appeared as the technical report
CoRR abs/1904.10786, 2019.
-
M. Ceska jr., M. Ceska, J. Matyas, A. Pankuch, and T. Vojnar.
Approximating Complex Arithmetic Circuits with Guaranteed Worst-Case Relative Error.
In Proc. of the 17th International Conference on Computer Aided Systems
Theory---EUROCAST'19,
Las Palmas, Spain, volume 12013 of LNCS, pages 482--490, 2019. Springer-Verlag.
A preliminary version is available
here.
-
V. Malik,
M. Hruska,
P. Schrammel, and
T. Vojnar.
2LS: Heap Analysis and Memory Safety (Competition
Contribution).
Technical report CoRR abs/1903.00712 related to
the SV-COMP'19 competition, 2019.
The 2LS tool is available here.
-
T. Fiedor,
L. Holik,
O. Lengal, and
T. Vojnar.
Nested Antichains for WS1S.
Acta Informatica, 56(3):205--228, Springer, 2019.
An extended abstract appeared in the the Proc. of TACAS'15. A preliminary version is available
here.
The concerned tool called dWiNA is available
here.
2018
-
V. Malik,
M. Hruska,
P. Schrammel, and
T. Vojnar.
Template-Based Verification of Heap-Manipulating
Programs.
In Proc. of 18th International Conference on Formal Methods in Computer-Aided
Design---FMCAD'18,
Austin, USA, 2018.
IEEE.
A preliminary version is available
here.
The 2LS tool is available
here.
-
L. Holik,
O. Lengal,
J. Sic,
M. Veanes, and
T. Vojnar.
Simulation Algorithms for Symbolic
Automata.
In Proc. of 16th International Symposium on Automated Technology for
Verification and Analysis---ATVA'18,
Los Angeles, USA, volume 11138 of LNCS, pages 109--125, 2018. Springer-Verlag.
An extended version appeared as the technical report
CoRR abs/1807.08487, 2018.
-
J. Fiedor,
M. Muzikovska,
A. Smrcka,
O. Vasicek, and
T. Vojnar.
Advances in the ANaConDA Framework for Dynamic Analysis and Testing of
Concurrent C/C++ Programs.
In Proc. of 27th International Symposium on Software Testing and
Analysis---ISSTA'18,
Amsterdam, Netherlands, pages 356--359, 2018. ACM.
The best tool demo award of ISSTA'18.
A preliminary version is available
here.
The ANaConDA tool is available
here.
-
M. Ceska,
J. Matyas,
V. Mrazek,
L. Sekanina,
Z. Vasicek, and
T. Vojnar.
ADAC: Automated Design of Approximate Circuits.
In Proc. of 30th International Conference on Computer Aided
Verification---CAV'18,
Oxford, UK, volume 10981 of LNCS, pages 612--620, 2018. Springer-Verlag.
The ADAC tool is available
here.
-
M. Ceska,
V. Havlena,
L. Holik,
O. Lengal, and
T. Vojnar.
Approximate
Reduction of Finite Automata for High-Speed Network Intrusion Detection.
In Proc. of 24th International Conference on Tools and Algorithms for the
Construction and Analysis of
Systems---TACAS'18,
Thessaloniki, Greece, volume 10806 of LNCS, pages 155--175, 2018. Springer-Verlag.
An extended version appeared as the technical report
CoRR abs/1710.08647, 2018.
-
V. Malik,
S. Marticek,
P. Schrammel,
M.K. Srivas,
T. Vojnar, and
J. Wahlang.
2LS: Memory
Safety and Non-termination (Competition Contribution).
In Proc. of 24th International Conference on Tools and Algorithms
for the Construction and Analysis of
Systems---TACAS'18,
Thessaloniki, Greece, volume 10806 of LNCS, pages 417--421, 2018. Springer-Verlag.
The 2LS tool is available
here.
-
T. Fiedor,
L. Holik,
A. Rogalewicz,
M. Sinn,
T. Vojnar, and
F. Zuleger.
From Shapes to Amortized Complexity.
In Proc. of 19th International Conference on Verification, Model Checking, and Abstract
Interpretation---VMCAI'18,
Los Angeles, CA, USA, volume 10747 of LNCS, pages 205--225, 2018. Springer-Verlag.
A preliminary version is available
here.
-
L. Holik,
A.W. Lin,
P. Janku,
P. Ruemmer, and
T. Vojnar.
String Constraints with
Concatenation and Transducers Solved Efficiently.
In Proc. of 45th ACM SIGPLAN Symposium on Principles of Programming
Languages---POPL'18,
Los Angeles, CA, USA, 2018.
Proceedings of the ACM on Programming Languages, Vol. 2, Article 4.
ACM.
A preliminary version is available
here.
The SLOTH string solver implemented within the paper is available
here.
-
J.M. Lourenco,
J. Fiedor,
B. Krena, and
T. Vojnar.
Discovering
Concurrency Errors.
A chapter of
Lectures on
Runtime Verification, volume 10457 of LNCS, pages 34--60, 2018. Springer-Verlag.
A preliminary version is available
here.
2017
-
M. Ceska,
J. Matyas,
V. Mrazek,
L. Sekanina,
Z. Vasicek, and
T. Vojnar.
Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit
Multipliers Accomplished.
In Proc. of 36th International Conference On Computer Aided
Design---ICCAD'17,
Irvine, CA, USA, pages 416--423, 2017. IEEE CS.
A bronze medal in the 2018 Human-Competitive Awards:
"Humies".
A preliminary version is available
here.
-
L. Holik,
R. Meyer,
T. Vojnar, and
S. Wolff.
Effect Summaries for Thread-Modular Analysis
(Sound Analysis Despite an Unsound Heuristic).
In Proc. of 24th Static Analysis
Symposium---SAS'17,
New York City, NY, USA, volume 10422 of LNCS, pages 169--191, 2017.
Springer-Verlag.
An extended version appeared as the technical report
CoRR abs/1705.03701, 2017.
The implementation is available
here.
-
R. Avros,
V. Dudka,
B. Krena,
Z. Letko,
H. Pluhackova,
S. Ur,
T. Vojnar, and
Z. Volkovitch.
Boosted Decision Trees for
Behaviour Mining of Concurrent Programmes.
Concurrency and Computation: Practice and Experience, 29(21), pp. 21, Wiley, 2017.
An extended abstract appeared in the the Proc. of MEMICS'14. A preliminary version is available
here.
-
R.J. Dias,
C. Ferreira,
J. Fiedor,
J.M. Lourenco,
A. Smrcka,
D.G. Sousa, and
T. Vojnar.
Verifying Concurrent Programs Using Contracts.
In Proc. of 10th IEEE International Conference on Software Testing, Verification and
Validation---ICST'17,
Waseda University, Tokyo, Japan, pages 196--206, 2017. IEEE.
A preliminary version is available
here.
An extended version appeared as the technical report
FIT-TR-2016-02,
FIT BUT, 2016.
The slides from the presentation are available
here.
The concerned ANaConDA framework is available
here.
-
B. Krena,
H. Pluhackova,
S. Ur, and
T. Vojnar.
Prediction of
Coverage of Expensive Concurrency Metrics Using Cheaper Metrics.
In Proc. of 16th International Conference on Computer Aided Systems
Theory---EUROCAST'17,
Las Palmas, Spain, volume 10672 of LNCS, pages 99--108, 2018. Springer-Verlag.
A preliminary version is available
here.
-
C. Enea,
O. Lengal,
M. Sighireanu, and
T. Vojnar.
Compositional Entailment Checking
for a Fragment of Separation Logic.
Formal Methods in System Design, 51(3):575--607, Springer-Verlag, 2017.
An extended abstract appeared in the the Proc. of APLAS'14. A preliminary version is available
here.
The concerned tool called SPEN is available
here.
-
C. Enea,
O. Lengal,
M. Sighireanu, and
T. Vojnar.
SPEN: A Solver for Separation Logic.
In Proc. of 9th NASA Formal Methods
Symposium---NFM'17,
NASA Ames Research Center, Moffett Field, CA, USA, volume 10227 of LNCS, pages 302--309, 2017.
Springer-Verlag.
A preliminary version is available
here.
The SPEN tool is available
here.
-
T. Fiedor,
L. Holik,
P. Janku,
O. Lengal, and
T. Vojnar.
Lazy Automata Techniques for WS1S.
In Proc. of 23rd International Conference on Tools and Algorithms for the Construction
and Analysis of Systems---TACAS'17,
Uppsala, Sweden, volume 10205 of LNCS, pages 407--425, 2017. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
CoRR abs/1701.06282, 2017.
The slides from the presentation are available
here.
The concerned tool Gaston is available
here.
-
L. Holik,
M. Hruska,
O. Lengal,
A. Rogalewicz,
J. Simacek, and
T. Vojnar.
Forester: From Heap Shapes to Automata
Predicates (Competition Contribution).
In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and
Analysis of Systems---TACAS'17,
Uppsala, Sweden, volume 10206 of LNCS, pages 365--369, 2017. Springer-Verlag.
A preliminary version is available
here.
The Forester tool is available
here.
-
L. Holik,
M. Hruska,
O. Lengal,
A. Rogalewicz, and
T. Vojnar.
Counterexample Validation
and Interpolation-Based Refinement for Forest Automata.
In Proc. of 18th International Conference on Verification, Model Checking, and
Abstract Interpretation---VMCAI'17,
Paris, France, volume 10145 of LNCS, pages 288--309, 2017. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
FIT-TR-2016-03,
FIT BUT, Brno, Czech Republic, 2016.
The Forester tool is available
here.
2016
-
R. Iosif,
A. Rogalewicz, and
T. Vojnar.
Abstraction Refinement for Trace Inclusion of Infinite State Systems
.
In Proc of 22nd International Conference on Tools and Algorithms for the Construction and
Analysis of Systems---TACAS'16,
Eindhoven, Netherlands, volume of LNCS 9636, pages 71--89, 2016. Springer-Verlag.
A preliminary version is available at arXiv with the id
1410.5056.
A prototype implementation is available in the tool called
INCLUDER (tracer).
-
L. Holik,
M. Kotoun,
P. Peringer,
V. Sokova,
M. Trtik, and
T. Vojnar.
Predator Shape Analysis Tool Suite
.
In Proc. of 12th Haifa Verification
Conference---HVC'16,
Haifa, Israel,
volume 10028 of LNCS, pages 202--209, 2016. Springer-Verlag.
A preliminary version is available
here.
The Predator tool suite is available
here.
-
L. Charvat,
A. Smrcka, and
T. Vojnar.
Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
.
In Proc. of 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer
Science---MEMICS'16,
Telc, Czech republic,
volume 233 of EPTCS, pages 87--93, 2016.
The Hades tool is available
here.
-
M. Kotoun,
P. Peringer,
V. Sokova, and
T. Vojnar.
Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution).
In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'16 as a competition contribution
within the 5th International Competition on Software
Verification---SV-COMP'16,
London, UK, volume 9636 of LNCS, pages 942--945, 2016. Springer-Verlag.
A preliminary version is available
here.
-
L. Holik,
M. Hruska,
O. Lengal,
A. Rogalewicz,
J. Simacek, and
T. Vojnar.
Run Forester, Run Backwards! (Competition Contribution).
In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'16 as a competition contribution
within the 5th International Competition on Software
Verification---SV-COMP'16,
London, UK, volume 9636 of LNCS, pages 923--926, 2016. Springer-Verlag.
A preliminary version is available
here.
-
K. Dudka,
L. Holik,
P. Peringer,
M. Trtik, and
T. Vojnar.
From Low-Level Pointers to High-Level Containers
.
In Proc of 17th International Conference on Verification, Model Checking, and Abstract
Interpretation---VMCAI'16,
St. Petersburg, Florida, USA, volume of LNCS 9583, pages 431--452,2016. Springer-Verlag.
A preliminary version is available at arXiv with the id
1510.07995.
The prototype implementation Predator-adt is available
here.
-
P.A. Abdulla,
L. Holik,
B. Jonsson,
O. Lengal,
C.Q. Trinh, and
T. Vojnar.
Verification of Heap Manipulating Programs with Ordered Data by
Extended Forest Automata.
Acta Informatica, 53(4):357--385, Springer-Verlag, 2016.
An extended abstract appeared in the the Proc. of ATVA'13.
A preliminary version is available
here.
2015
-
T. Fiedor,
L. Holik,
O. Lengal, and
T. Vojnar.
Nested Antichains for WS1S.
In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'15,
London, UK, volume 9035 of LNCS, pages 658--674, 2015. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
FIT-TR-2014-01,
FIT BUT, Brno, Czech Republic, 2014.
The concerned tool called dWiNA is available
here.
-
P. Muller,
P. Peringer, and
T. Vojnar.
Predator Hunting Party (Competition Contribution).
In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'15 as a competition contribution
within the 4th International Competition on Software
Verification---SV-COMP'15,
London, UK, volume 9035 of LNCS, pages 443--446, 2015. Springer-Verlag.
A preliminary version is available
here.
-
L. Holik,
M. Hruska,
O. Lengal,
A. Rogalewicz,
J. Simacek, and
T. Vojnar.
Forester: Shape Analysis Using Tree Automata (Competition Contribution).
In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'15 as a competition contribution
within the 4th International Competition on Software
Verification---SV-COMP'15,
London, UK, volume 9035 of LNCS, pages 432--435, 2015. Springer-Verlag.
A preliminary version is available
here.
-
J. Fiedor,
Z. Letko,
J. Lourenco, and
T. Vojnar.
Dynamic Validation of Contracts in Concurrent Code.
In Proc. of 15th International Conference on Computer Aided Systems
Theory---EUROCAST'15,
Las Palmas, Spain,
volume 9520 of LNCS, pages 555-564, 2015. Springer-Verlag.
A preliminary version is available
here.
-
L. Charvat,
A. Smrcka, and
T. Vojnar.
Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems.
In Proc. of 15th International Conference on Computer Aided Systems
Theory---EUROCAST'15,
Las Palmas, Spain,
volume 9520 of LNCS, pages 605--614, 2015. Springer-Verlag.
A preliminary version is available
here.
-
J. Fiedor,
V. Hruba,
B. Krena,
Z. Letko,
S. Ur, and
T. Vojnar.
Advances in Noise-based Testing of Concurrent Software.
In Software Testing, Verification and Reliability,
25(3):272--309, Elsevier, 2015.
A preliminary version is available
here.
2014
-
L. Charvat,
A. Smrcka, and
T. Vojnar.
Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors.
In Proc. of 15th International Workshop on Microprocessor Test and
Verification---MTV'14, Austin, USA, IEEE
CS, pages 83--89, 2014.
A preliminary version is available
here.
-
C. Enea,
O. Lengal,
M. Sighireanu, and
T. Vojnar.
Compositional Entailment Checking for a Fragment of Separation Logic.
In Proc. of 12th Asian Symposium on Programming Languages and
Systems---APLAS'14,
Singapore, 2014, volume 8858 of LNCS, pages 314--333, 2014. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
FIT-TR-2014-01,
FIT BUT, Brno, Czech Republic, 2014.
The concerned tool called SPEN is available
here.
Results of SPEN participating in the separation logic competition within SMT-COMP 2014 can be
found here.
-
R. Iosif,
A. Rogalewicz, and
T. Vojnar.
Deciding Entailments in Inductive Separation Logic with Tree Automata.
In Proc. of 12th International Symposium on Automated Technology for Verification
and Analysis---ATVA'14, Sydney, Australia, 2014,
volume 8837 of LNCS, pages 201--218, 2014. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
CoRR abs/1402.2127,
arxiv.org, 2014.
The concerned tool called SLIDE is available
here.
Results of SLIDE participating in the separation logic competition within SMT-COMP 2014 can be
found here.
-
V. Hruba,
B. Krena,
Z. Letko,
H. Pluhackova, and
T. Vojnar.
Multi-objective Genetic Optimization for Noise-Based Testing of Concurrent Software.
In Proc. of 6th Symposium on Search Based Software
Engineering---SSBSE'14, Fortaleza, Brazil,
volume 8636 of LNCS, pages 107--122, 2014. Springer-Verlag.
A preliminary version is available
here.
-
J. Fiedor,
Z. Letko,
J. Lourenco, and
T. Vojnar.
On Monitoring C/C++ Transactional Memory Programs.
In Proc. of 9th International Doctoral Workshop on Mathematical and Engineering Methods in
Computer Science---MEMICS'14, Telc, Czech Republic,
volume 8934 of LNCS, pages 73--87, 2014. Springer-Verlag.
A preliminary version is available
here.
The concerned tool called ANaConDA is available
here.
-
R. Avros,
V. Hruba,
B. Krena,
Z. Letko,
H. Pluhackova,
S. Ur,
T. Vojnar, and
Z. Volkovitch.
Boosted Decision
Trees for Behaviour Mining of Concurrent Programs.
In Proc. of 9th International Doctoral Workshop on Mathematical and Engineering Methods in
Computer Science---MEMICS'14,
Telc, Czech Republic, pages 15--27, 2014. Novpress.
-
K. Dudka,
P. Peringer, and
T. Vojnar.
Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution).
In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'14 as a competition contribution
within the 3rd International Competition on Software
Verification---SV-COMP'14,
Grenoble, France, volume 8413 of LNCS, pages 412--414, 2014. Springer-Verlag.
A preliminary version is available
here.
-
P. Muller and
T. Vojnar.
CPAlien: Shape Analyzer for CPAChecker (Competition Contribution).
In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'14 as a competition contribution
within the 3rd International Competition on Software
Verification---SV-COMP'14,
Grenoble, France, volume 8413 of LNCS, pages 395--397, 2014. Springer-Verlag.
A preliminary version is available
here.
-
P.A. Abdulla,
Y.-F. Chen,
L. Holik, and
T. Vojnar.
Mediating for Reduction (On Minimizing Alternating Büchi Automata).
In Theoretical Computer Science,
552:26--43, Elsevier, 2014.
A preliminary version is available
here.
An extended abstract appeared in the proceedings of FSTTCS'09.
2013
-
L. Holik,
O. Lengal,
J. Simacek,
A. Rogalewicz, and
T. Vojnar.
Fully Automated Shape Analysis Based on Forest Automata.
In Proc. of 25th International Conference on Computer Aided
Verification---CAV'13,
Saint Petersburg, Russia, volume 8044 of LNCS, pages 740--755, 2013. Springer-Verlag.
A preliminary version is available
here.
The concerned tool called Forester is available
here.
-
P.A. Abdulla,
L. Holik,
B. Jonsson,
O. Lengal,
C.Q. Trinh, and
T. Vojnar.
Verification of Heap Manipulating Programs with Ordered Data by
Extended Forest Automata.
In Proc. of 11th International Symposium on Automated Technology for
Verification and Analysis---ATVA'13,
Hanoi, Vietnam, volume 8172 of LNCS, pages 224--239, 2013. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2013-02,
FIT BUT, Brno, Czech Republic, 2013.
-
K. Dudka,
P. Peringer, and
T. Vojnar.
Byte-Precise Verification of Low-Level List Manipulation.
In Proc. of 20th Static Analysis
Symposium---SAS'13,
Seattle, USA, volume 7935 of LNCS, pages 215--237, 2013. Springer-Verlag.
A preliminary version is available
here.
An extended version appeared as the technical report
FIT-TR-2012-04,
FIT BUT, Brno, Czech Republic, 2012.
The concerned tool called Predator is available
here.
-
K. Dudka,
P. Muller,
P. Peringer, and
T. Vojnar.
Predator: A Tool for Verification of Low-level List Manipulation (Competition Contribution).
In Proc. of 19th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'13 as a competition contribution
within the 2nd International Competition on Software
Verification---SV-COMP'13,
Rome, Italy, volume 7795 of LNCS, pages 627--629, 2013. Springer-Verlag.
A preliminary version is available
here.
-
L. Charvat,
A. Smrcka, and
T. Vojnar.
An Abstraction of Multi-port Memories with Arbitrary Addressable Units.
In 14th International Conference on Computer Aided Systems
Theory---EUROCAST'13,
Las Palmas, Spain, volume 8111 of LNCS, pages 460--468, 2013. Springer-Verlag.
A preliminary version is available
here.
-
P.A. Abdulla,
J. Cederberg, and
T. Vojnar.
Monotonic
Abstraction for Programs with Multiply-Linked Structures.
In International Journal of Foundations of Computer Science,
24(2):187--210, World Scientific, 2013. A preliminary version appeared
in the proceedings of RP'11.
-
B. Krena and
T. Vojnar.
Automated Formal Analysis
and Verification: An Overview.
International Journal of General Systems, 42(4):335--365, Taylor and Francis, 2013.
A preliminary version is available
here.
2012
-
P. Habermehl,
L. Holik,
J. Simacek,
A. Rogalewicz, and
T. Vojnar.
Forest Automata for Verification
of Heap Manipulation.
Formal Methods in System Design, 41(1):83--106, Springer-Verlag, 2012. An extended abstract
appeared in the the Proc. of CAV'11. A preliminary version is available
here.
-
V. Hruba,
B. Krena,
Z. Letko,
S. Ur, and
T. Vojnar.
Testing of Concurrent
Programs Using Genetic Algorithms.
In Proc. of 4th Symposium on Search Based Software
Engineering---SSBSE'12, Riva del Garda, Trento,
volume 7515 of LNCS, pages 152--167, 2012. Springer-Verlag.
A preliminary version is available
here.
-
J. Fiedor and
T. Vojnar.
ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs
on the Binary Level.
In Proc. of 3rd International Conference on Runtime
Verification---RV'12, Istanbul, Turkey, 2012.
volume 7687 of LNCS, pages 35--41, 2012. Springer-Verlag.
A preliminary version is available
here.
The ANaConDA framework is available
here.
The best tool paper award of RV'12.
-
J. Fiedor and
T. Vojnar.
Noise-based Testing and Analysis of
Multi-threaded C/C++ Programs on the Binary Level.
In Proc. of 10th Workshop on Parallel and Distributed Systems: Testing, Analysis, and
Debugging---PADTAD'12, Minneapolis, USA,
pages 36--46, 2012. ACM Press.
A preliminary version is available
here.
-
L. Charvat,
A. Smrcka, and
T. Vojnar.
Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description.
In Proc. of 13th International Workshop on Microprocessor Test and
Verification---MTV'12, Austin, USA, IEEE CS, 2012.
A preliminary version is available
here.
-
O. Lengal,
J. Simacek, and
T. Vojnar.
VATA: A Library for Efficient
Manipulation of Non-Deterministic Tree Automata.
In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'12, Talinn, Estonia,
volume 7214 of LNCS, pages 79--94, 2012. Springer-Verlag.
A preliminary version is available
here.
-
K. Dudka,
P. Muller,
P. Peringer, and
T. Vojnar.
Predator: A Verification Tool for
Programs with Dynamic Linked Data Structures (Competition Contribution).
In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'12 as a competition contribution
within the 1st International Competition on Software
Verification---SV-COMP'12, Talinn, Estonia,
volume 7214 of LNCS, pages 545--548, 2012. Springer-Verlag.
A preliminary version is available
here.
-
A. Bouajjani,
P. Habermehl,
A. Rogalewicz, and
T. Vojnar.
Abstract Regular (Tree) Model Checking.
International Journal on Software Tools for Technology Transfer (STTT),
14(2):167--191, Springer-Verlag, 2012.
A preliminary version is available
here.
2011
-
P. Habermehl,
L. Holik,
J. Simacek,
A. Rogalewicz, and
T. Vojnar.
Forest Automata for Verification
of Heap Manipulation.
In Proc. of 23rd International Conference on Computer Aided
Verification---CAV'11,
Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 424--440, 2011. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2011-01,
FIT BUT, Brno, Czech Republic, 2011.
The concerned tool called Forester is available
here.
-
K. Dudka,
P. Peringer, and
T. Vojnar.
Predator: A Practical Tool for
Checking Manipulation of Dynamic Data Structures Using Separation Logic.
In Proc. of 23rd International Conference on Computer Aided
Verification---CAV'11,
Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 372--378, 2011. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2011-02,
FIT BUT, Brno, Czech Republic, 2011.
The Predator tool is available
here.
A few slides presenting Predator are available
here.
-
L. Holik,
O. Lengal,
J. Simacek, and
T. Vojnar.
Efficient
Inclusion Checking on Explicit and Semi-Symbolic Tree Automata.
In Proc. of 9th International Symposium on Automated Technology for Verification and
Analysis---ATVA'11,
Taipei, Taiwan, volume 6996 of LNCS, pages 243--258, 2011. Springer-Verlag.
More details and some post-ATVA extension of the approach can be found in the technical report
FIT-TR-2011-04,
FIT BUT, Brno, Czech Republic, 2011.
-
B. Krena,
Z. Letko, and
T. Vojnar.
Noise Injection Heuristics for
Concurrency Testing.
In Proc. of 7th International Doctoral Workshop on Mathematical and Engineering Methods in Computer
Science---MEMICS'11, Lednice, Czech Republic,
volume 7119 of LNCS, pages 123--135, 2012. Springer-Verlag.
-
B. Krena,
Z. Letko, and
T. Vojnar.
Coverage Metrics for
Saturation-based and Search-based Testing of Concurrent Software.
In Proc. of 2nd International Conference on Runtime
Verification---RV'11,
San Francisco, CA, USA, volume 7186 of LNCS, pages 177--192, 2012. Springer-Verlag.
A preliminary version is available
here.
-
J. Fiedor,
V. Hruba,
B. Krena, and
T. Vojnar.
DA-BMC: A Tool
Chain Combining Dynamic Analysis and Bounded Model Checking.
In Proc. of 2nd International Conference on Runtime
Verification---RV'11,
San Francisco, CA, USA, volume 7186 of LNCS, pages 375--380, 2012. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2011-06,
FIT BUT, Brno, Czech Republic, 2011.
The DA-BMC tool is available
here.
-
P.A. Abdulla,
Y.-F. Chen,
L. Clemente,
L. Holik,
C.-D. Hong,
R. Mayr, and
T. Vojnar.
Advanced
Ramsey-based Büchi Automata Inclusion Testing.
In Proc. of 22nd International Conference on Concurrency
Theory---CONCUR'11,
Aachen, Germany, volume 6901 of LNCS, pages 187--202, 2011. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2011-03,
FIT BUT, Brno, Czech Republic, 2011.
-
P.A. Abdulla,
J. Cederberg, and
T. Vojnar.
Monotonic
Abstraction for Programs with Multiply-Linked Structures.
In Proc. of 5th Workshop on Reachability
Problems---RP'11,
Genova, Italy, volume 6945 of LNCS, pages 125--138, 2011. Springer-Verlag.
-
K. Dudka,
P. Peringer, and
T. Vojnar.
An Easy to Use Infrastructure for
Building Static Analysis Tools.
In Proc. of 13th International Conference on Computer Aided Systems
Theory---EUROCAST'11,
Las Palmas, Spain, volume 6927 of LNCS, pages 527--534, 2012. Springer-Verlag.
A preliminary version is available
here.
The described infrastructre is available
here.
-
J. Fiedor,
Z. Letko,
B. Krena, and
T. Vojnar.
A Uniform
Classification of Common Concurrency Errors.
In Proc. of 13th International Conference on Computer Aided Systems
Theory---EUROCAST'11,
Las Palmas, Spain, volume 6927 of LNCS, pages 519--526, 2012. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2010-03,
FIT BUT, Brno, Czech Republic, 2010.
-
A. Bouajjani,
M. Bozga,
P. Habermehl,
R. Iosif,
P. Moro, and
T. Vojnar.
Programs with Lists are Counter Automata.
Formal Methods in System Design, 38(2):158--192, Springer-Verlag, 2011. An extended
abstract appeared in the Proc. of CAV'06.
2010
-
P.A. Abdulla,
Y.-F. Chen,
L. Holik,
R. Mayr, and
T. Vojnar.
When
Simulation Meets Antichains (on Checking Language Inclusion of NFAs).
In Proc. of 16th International Conference on Tools and Algorithms for the Construction and Analysis
of Systems---TACAS'10,
Paphos, Cyprus, volume 6015 of LNCS (the ARCoSS subline), pages 158--174, 2010. Springer-Verlag.
The EATCS best theory paper
of ETAPS'10.
An extended version appeared as the technical report
FIT-TR-2010-01,
FIT BUT, Brno, Czech Republic, 2010.
-
P.A. Abdulla,
Y.-F. Chen,
L. Clemente,
L. Holik,
C.-D. Hong,
R. Mayr, and
T. Vojnar.
Simulation Subsumption in Ramsey-based
Büchi Automata Universality and Inclusion Testing.
In Proc. of 22nd International Conference on Computer Aided
Verification---CAV'10,
Edinburgh, Scotland, volume 6174 of LNCS, pages 132--147, 2010. Springer-Verlag.
An extended version appeared as the technical report
FIT-TR-2010-02,
FIT BUT, Brno, Czech Republic, 2010.
-
B. Krena,
Z. Letko,
S. Ur, and
T. Vojnar.
A Platform for Search-Based Testing of Concurrent Software.
In Proc. of 8th International Workshop on Parallel and Distributed Systems: Testing and
Debugging---PADTAD'10,
Trento, Italy, pages 48--58, 2010. ACM Press.
-
P. Habermehl,
R. Iosif, and
T. Vojnar.
Automata-based Verification of Programs with Tree Updates.
Acta Informatica, 47(1):1--31, 2010. Springer-Verlag.
An extended version of a paper published originally at
TACAS'06.
2009
-
P.A. Abdulla,
Y.-F. Chen,
L. Holik, and
T. Vojnar.
Mediating for Reduction (On Minimizing Alternating Büchi Automata).
In Proc. of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science---FSTTCS'09,
Kanpur, India, volume 4 of LIPIcs, pages 1--12, 2009.
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik.
Also appeared as the technical report FIT-TR-2009-02, FIT BUT, Brno, Czech Republic, 2009.
-
M. Bozga,
P. Habermehl,
R. Iosif,
F. Konecny, and
T. Vojnar.
Automatic Verification of Integer Array Programs.
In Proc. of 21st International Conference on Computer Aided Verification---CAV'09,
Grenoble, France, volume 5643 of LNCS, pages 157--172, 2009. Springer-Verlag.
An extended version appeared as the technical report TR-2009-2,
Verimag,
Grenoble, France, 2009.
-
B. Krena,
Z. Letko,
Y. Nir-Buchbinder,
R. Tzoref-Brill,
S. Ur, and
T. Vojnar.
A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and
Runtime Healing.
In Proc. of 9th International Workshop on Runtime Verification---RV'09,
Grenoble, France, volume 5779 of LNCS, pages 101--114, 2009. Springer-Verlag.
Also appeared as the technical report FIT-TR-2009-01, FIT BUT, Brno, Czech Republic, 2009.
-
V. Hruba,
B. Krena, and
T. Vojnar.
Self-Healing Assurance Using Bounded Model Checking.
In Proc. of 12th International Conference on Computer Aided Systems
Theory---EUROCAST'09,
Las Palmas, Spain, volume 5717 of LNCS, pages 295--303, 2009. Springer-Verlag.
-
P.A. Abdulla,
L. Holik,
L. Kaati, and
T. Vojnar.
A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata.
Electronic Notes in Theoretical Computer Science,
251:27--48, 2009. An extended version of a paper published originally at
MEMICS'08.
-
P.A. Abdulla,
A. Bouajjani,
L. Holik,
L. Kaati, and
T. Vojnar.
Composed Bisimulation for Tree Automata.
International Journal of Foundations of Computer Science,
20(4):685--700, 2009. An extended version of a paper published originally at
CIAA'08.
2008
-
P. Habermehl,
R. Iosif, and
T. Vojnar.
A Logic of Singly Indexed Arrays.
In Proc. of 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning---LPAR'08, Doha, Qatar, volume 5330 of LNAI, pages 558--573, 2008. Springer-Verlag.
An extended version appeared as the technical report TR-2008-9,
Verimag,
Grenoble, France, 2008.
-
P.A. Abdulla,
L. Holik,
L. Kaati, and
T. Vojnar.
A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata.
In Proc. of 4th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'08, Znojmo, Czech Republic, pages 3--11, 2008.
An extended version appeared as the technical report FIT-TR-2008-005, FIT BUT, Brno, Czech Republic, 2008.
-
B. Krena,
Z. Letko, and
T. Vojnar.
AtomRace: Data Race and Atomicity Violation Detector and Healer.
In Proc. of 6th International Workshop on Parallel and Distributed Systems: Testing and
Debugging---PADTAD'08,
Seattle, WA, USA, pages 1--10, 2008. ACM Press.
-
A. Bouajjani,
P. Habermehl,
L. Holik,
T. Touili, and
T. Vojnar.
Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata.
In Proc. of 13th International Conference on Implementation and Application of Automata---CIAA'08, San Francisco, CA, USA, volume 5148 of LNCS, pages 57--67, 2008. Springer-Verlag.
An extended version appeared as the technical report FIT-TR-2008-001,
FIT BUT, Brno, Czech Republic, 2008.
-
P.A. Abdulla,
A. Bouajjani,
L. Holik,
L. Kaati, and
T. Vojnar.
Composed Bisimulation for Tree Automata.
In Proc. of 13th International Conference on Implementation and Application of Automata---CIAA'08, San Francisco, CA, USA, volume 5148 of LNCS, pages 212--222, 2008. Springer-Verlag.
The best paper award of CIAA'08.
An extended version appeared as the technical report FIT-TR-2008-004,
FIT BUT, Brno, Czech Republic, 2008.
-
P. Habermehl,
R. Iosif, and
T. Vojnar.
What else is decidable about integer arrays?
In Proc. of 11th International Conference on Foundations of Software Science and Computation Structures---FoSSaCS'08, Budapest, Hungary, volume 4962 of LNCS, pages 475--490, 2008. Springer-Verlag.
An extended version appeared as the technical report TR-2007-8, Verimag,
Grenoble, France, 2007.
-
P.A. Abdulla,
A. Bouajjani,
L. Holik,
L. Kaati, and
T. Vojnar.
Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata.
In Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'08, Budapest, Hungary, volume 4963 of LNCS, pages 93--108, 2008. Springer-Verlag.
An extended version appeared as the technical report FIT-TR-2007-001, FIT BUT,
Brno, Czech Republic, 2007.
-
A. Bouajjani,
P. Habermehl, and
T. Vojnar.
Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management.
Formal Methods in System Design, Springer-Verlag, 32(2):129--172, 2008. An extended abstract appeared in the
Proc. of CONCUR'03.
2007
-
P. Habermehl,
R. Iosif,
A. Rogalewicz, and
T. Vojnar.
Proving Termination of Tree Manipulating Programs.
In Proc. of 5th International Symposium on Automated Technology for Verification and
Analysis---ATVA'07, Tokyo, Japan,
volume 4762 of LNCS, pages 145--161, 2007. Springer-Verlag.
An extended version appeared as the Verimag Technical Report TR-2007-1, Verimag,
Grenoble, France, 2007.
-
A. Smrcka and
T. Vojnar.
Verifying Parameterised Hardware Designs via Counter Automata.
In Proc. of Haifa Verification Conference 2007---HVC'07, Haifa, Israel, 2007. Appeared in volume 4899 of LNCS, pages 51--68, 2008. Springer-Verlag.
-
M. Ceska,
P. Erlebach, and
T. Vojnar.
Generalized Multi-Pattern-Based Verification of Programs with Linear Linked Structures.
Formal Aspects of Computing, Springer-Verlag, 19(3):363--374, 2007.
-
B. Krena,
Z. Letko,
R. Tzoref,
S. Ur, and
T. Vojnar.
Healing Data Races On-The-Fly.
In Proc. of 5th International Workshop on Parallel and Distributed Systems: Testing and
Debugging---PADTAD'07,
London, UK, 2007. ACM Press.
-
M. Ceska,
P. Erlebach, and
T. Vojnar.
Pattern-based Verification for Trees.
In Proc. of 11th International Conference on Computer Aided Systems
Theory---EUROCAST'07, Las Palmas, Spain,
volume 4739 of LNCS, pages 488--496, 2007. Springer-Verlag.
-
T. Vojnar.
Cut-offs and Automata in Formal Verification of Infinite-State Systems.
Habilitation thesis, Faculty of Information Technology, Brno University of Technology,
Brno, Czech Republic, 2007.
189 p.
2006
-
A. Bouajjani,
P. Habermehl,
A. Rogalewicz, and
T. Vojnar.
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures.
In Proc. of 13th International Static Analysis Symposium---SAS'06,
Seoul, Korea, volume 4134 of LNCS, pages 52--70, 2006. Springer-Verlag.
-
A. Bouajjani,
M. Bozga,
P. Habermehl,
R. Iosif,
P. Moro, and
T. Vojnar.
Programs with Lists are Counter Automata.
In Proc of 18th
International Conference on Computer Aided Verification---CAV'06,
Seattle, WA, USA, volume 4144 of LNCS, pages 517--531, 2006. Springer-Verlag.
An extended version appeared as the technical report TR-2006-3 of Verimag,
Grenoble, France, 2006.
-
P. Habermehl,
R. Iosif, and
T. Vojnar.
Automata-based Verification of Programs with Tree Updates.
In Proc. of 12th International Conference on Tools and Algorithms for the Construction and Analysis of
Systems---TACAS'06,
Vienna, Austria, volume 3920 of LNCS, pages 350--364, 2006. Springer-Verlag.
An extended version appeared as the technical report TR-2005-16 of
Verimag, Grenoble, France, 2005.
-
A. Smrcka,
V. Rehak,
T. Vojnar,
D. Safranek,
P. Matousek, and
Z. Rehak.
Verifying VHDL Designs with Multiple Clocks in SMV.
In Proc. of 11th International Workshop on Formal Methods for Industrial Critical
Systems---FMICS'06,
Bonn, Germany, volume 4346 of LNCS, pages 148--164, 2007. Springer-Verlag.
-
M. Ceska,
P. Erlebach, and
T. Vojnar.
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures.
Electronic Notes in Theoretical Computer Science,
145:113--130, 2006.
Proc. of 5th International Workshop on Automated Verification
of Critical Systems---AVOCS'05,
Warwick, UK, pages 101--117, 2005.
-
A. Bouajjani,
P. Habermehl,
A. Rogalewicz, and
T. Vojnar.
Abstract Regular Tree Model Checking.
Electronic Notes in Theoretical Computer Science,
149(1):37--48, 2006.
Proc. of 7th International Workshop on Verification of Infinite-State
Systems---Infinity'05, San Francisco, CA, USA,
pages 15--24, 2005.
2005
-
A. Bouajjani,
P. Habermehl,
P. Moro, and
T. Vojnar.
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking.
In Proc. of 11th International Conference on Tools and Algorithms for the Construction and Analysis of
Systems---TACAS'05,
Edinburgh, UK, volume 3440 of LNCS, pages 13--29, 2005. Springer-Verlag.
-
A. Smrcka,
P. Matousek, and
T. Vojnar.
High-Level Modelling, Analysis, and Verification on FPGA-based Hardware
Design.
In Proc. of 13th International Conference on Correct Hardware Design
and Verification Methods---Charme'05,
Saarbrücken, Germany, volume 3725 of LNCS, pages 371--375, 2005. Springer-Verlag.
An extended version appeared as the technical report
8/2005 of
CESNET within the
Liberouter project, Czech Republic, 2005.
-
P. Erlebach and
T. Vojnar.
Automated Formal Verification of Programs with Dynamic Data
Structures Using State-of-the-Art Tools.
In Proc. of 8th International Conference on
Information Systems Implementation and
Modelling---ISIM'05,
Hradec nad Moravici, Czech Republic, pages 219--226, 2005.
MARQ Ostrava.
-
M. Ceska,
B. Krena, and
T. Vojnar.
Parallel State Space Generation and Exploration on Shared-Memory Architectures.
In Proc. of 10th International Conference on Computer Aided
Systems Theory---EUROCAST'05,
Las Palmas, Canary Islands, Spain, volume 3643 of LNCS, pages 275--280, 2005. Springer-Verlag.
-
P. Hlavka,
T. Kratochvila,
V. Rehak,
D. Safranek,
P. Simecek, and
T. Vojnar.
CRC64 Algorithm Analysis and Verification.
Technical report 27/2005 of
CESNET within the
Liberouter project, Czech Republic, 2005.
-
P. Habermehl and
T. Vojnar.
Regular Model Checking Using Inference of Regular Languages.
Electronic Notes in Theoretical Computer Science,
138(3):21--36, 2005.
Proc. of 6th International Workshop on Verification of Infinite-State
Systems---Infinity'04, London, UK, 2004.
2004
-
A. Bouajjani,
P. Habermehl, and
T. Vojnar.
Abstract Regular Model Checking.
In Proc. of 16th International Conference on Computer Aided
Verification---CAV'04,
Boston, Massachusetts, USA, volume 3114 of LNCS, pages 372--386, 2004. Springer-Verlag.
-
A. Rogalewicz and
T. Vojnar.
Tree Automata In Modelling and Verification Of Concurrent Programs.
In Proc. of ASIS'04, MARQ Ostrava, Czech Republic,
pages 197--202, 2004.
2003
-
A. Bouajjani,
P. Habermehl, and
T. Vojnar.
Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management.
In Proc. of 14th International Conference on Concurrency
Theory---CONCUR'03, Marseille, France,
volume 2761 of LNCS, pages 174--190, 2003. Springer-Verlag.
-
M. Ceska,
L. Hasa, and
T. Vojnar.
Partial Order Reduction in Model Checking of Object-Oriented Petri Nets.
In Proc. of 9th International Workshop on Computer Aided Systems Theory--EUROCAST'03,
volume 2809 of LNCS, pages 265--278, 2003. Springer-Verlag.
2002
-
A. Bouajjani and
T. Vojnar.
Automata with Parameterized Arrays and Parameterized Networks of Automata.
Research report D11 of the
ADVANCE project
(EU's 5th Framework IST FET project No. IST-1999-29082). LIAFA, University Paris 7, France, 2002.
-
A. Bouajjani,
P. Habermehl, and
T. Vojnar.
Verification of Parameterized Concurrent Systems with Resource Sharing.
Research report D12.2 of the
ADVANCE project
EU's 5th Framework IST FET project No. IST-1999-29082). LIAFA, University Paris 7, France, 2002.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Modelling, Prototyping, and Verifying Concurrent and Distributed Applications Using
Object-Oriented Petri Nets.
Kybernetes: The International Journal of Systems & Cybernetics,
2002(9):1289--1299, 2002.
2001
-
T. Vojnar.
Towards Formal Analysis and Verification over State Spaces of Object-Oriented Petri Nets.
PhD thesis, Department of Computer Science and Engineering, FEECS, Brno University of Technology,
Brno, Czech Republic, 2001.
148 p.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Generating and Using State Spaces of Object-Oriented Petri Nets.
International Journal of Computer Systems Science and Engineering,
16(3):183--193, 2001.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Analysis and Verification Queries over Object-Oriented Petri Nets.
In Proc. of 8th International Workshop on Computer Aided Systems Theory---EUROCAST'01,
volume 2178 of LNCS, pages 365--384, 2001. Springer-Verlag.
-
R. Koci and
T. Vojnar.
A PNtalk-based Model of a Cooperative Editor.
In Proc. of MOSIS'01, Hradec nad Moravici, Czech Republic, pages 165--172, 2001.
MARQ Ostrava.
-
B. Krena and
T. Vojnar.
Type Analysis in Object-Oriented Petri Nets.
In Proc. of ISM'01, Hradec nad Moravici, Czech Republic, pages 173--180, 2001. MARQ Ostrava.
2000
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Towards Verifying Distributed Systems Using Object-Oriented Petri Nets.
In Proc. of 7th International Workshop on Computer Aided Systems Theory---EUROCAST'99,
volume 1798 of LNCS, pages 90--104, 2000. Springer-Verlag.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Generating and Exploiting State Spaces of Object-Oriented Petri Nets.
In Proc. of Workshop on Software Engineering and Petri Nets---SEPN'00, Aarhus, Denmark,
DAIMI PB-548, pages 35--54, 2000. Department of Computer Science, University of Aarhus.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
PNtalk Modelling Experience.
In Proc. of 26th ASU Conference, La Valetta, Malta, pages 65--73, 2000. ASU
and University of Malta, Faculty of Science, Department of Statistics and
Operations Research.
1998
-
M. Ceska,
V. Janousek, and
T. Vojnar.
Object-Oriented Petri Nets, Their Simulation, and Analysis.
In Proc. of IEEE System, Man, and Cybernetics Conference---SMC'98,
San Diego, California, USA, IEEE Catalog Number 98CH36218, pages 256--261, 1998.
Omnipress.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
PNtalk--An Experimental System Based on Object-Oriented Petri Nets.
In Tool Demonstrations within 19th International Conference
on Application and Theory of Petri Nets---ICATPN'98, Lisbon, Portugal, 1998.
-
V. Janousek and
T. Vojnar.
State Spaces of Object-Oriented Petri Nets.
In Proc. of MFCS'98 Workshop on Concurrency, Brno, Czech Republic, Technical Report
FIMU-RS-98-06, pages 87--96, 1998. Faculty of
Informatics, Masaryk University, Brno, Czech Republic.
1997
-
M. Ceska,
V. Janousek, and
T. Vojnar.
PNtalk--A Computerized Tool for Object Oriented Petri Nets Modelling.
In Proc. of 6th International Workshop on Computer Aided Systems Theory---EUROCAST'97,
volume 1333 of LNCS, pages 591--610, 1997. Springer-Verlag.
-
M. Ceska,
V. Janousek, and
T. Vojnar.
PNtalk--A Language and System Based on Object Oriented Petri Nets.
In Tool Demonstrations within 18th International Conference
on Application and Theory of Petri Nets---ICATPN'97, Toulouse, France, 1997.
-
T. Vojnar.
Various Kinds of Petri Nets in Simulation and Modelling.
In Proc. of MOSIS'97, Hradec nad Moravici, Czech Republic, pages 227--232, 1997.
MARQ Ostrava.