| |
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 197--202, 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.
|
| |