Ing. Ondřej Lengál, Ph.D.
| 2019 |
|
-
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 XXXXX of LNCS,
pages XXX--XXX,
2019.
Springer-Verlag.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1905.08697,
2019.
[incomplete reference]
-
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) 0(0),
pages 1--17,
2019.
Springer-Verlag.
A preliminary version is available here.
[incomplete reference]
-
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 XXX--XXX,
2019.
IEEE.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1904.10786.
[incomplete reference]
-
T. Fiedor,
L. Holik,
O. Lengal, and
T. Vojnar.
Nested Antichains for WS1S.
Acta Informatica 56(3),
pages 205--228,
2019.
Springer-Verlag.
A preliminary version is available here.
The associated tool dWiNA is available here.
| 2018 |
|
-
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.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1807.08487,
2018.
-
Y. Chen,
M. Heizmann,
O. Lengal,
Y. Li,
M. Tsai,
A. Turrini, and
L. Zhang.
Advanced Automata-based Algorithms for Program Termination Checking.
In Proc. of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
---
PLDI'18,
Philadelphia, PA,
USA,
pages 135--150,
2018.
ACM.
A preliminary version 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.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1710.08647,
2018.
| 2017 |
|
-
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),
pages 575--607,
2017.
Springer-Verlag.
-
Y. Chen,
O. Lengal,
T. Tan, and
Z. Wu.
Register Automata with Linear Arithmetic.
In Proc. of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
---
LICS'17,
Reykjavik, Iceland,
pages 1--12,
2017.
IEEE.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1704.03972,
2017.
-
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.
-
Y. Chen,
C. Hong,
O. Lengal,
S. Mu,
N. Sinha, and
B. Wang.
An Executable Sequential Specification for Spark Aggregation.
In Proc. of 5th International Conference of NETworked sYStems
---
NETYS'17,
Marrakech,
Morocco,
volume 10299 of LNCS,
pages 421--438,
2017.
Springer-Verlag.
A preliminary version is available here.
An extended version appeared as the technical report
CoRR abs/1702.02439,
2017.
-
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.
-
O. Lengal,
A.W. Lin,
R. Majumdar, and
P. Ruemmer.
Fair Termination for Parameterized Probabilistic Concurrent Systems.
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 499--517,
2017.
Springer-Verlag.
A preliminary version is available here.
The slides from the presentation are 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 associated tool Gaston 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.
|
| 2016 |
|
-
Y. Chen,
C. Hsieh,
O. Lengal,
T. Lii,
M. Tsai,
B. Wang, and
F. Wang.
PAC Learning-Based Verification and Model Synthesis.
In Proc. of 38th International Conference on Software Engineering
---
ICSE'16,
Austin,
Texas,
pages 714--724,
2016.
ACM.
A preliminary version is available here.
-
L. Holik,
M. Hruska,
O. Lengal,
A. Rogalewicz,
J. Simacek, and
T. Vojnar.
Run Forester! Run Backwads! (Competition Contribution).
In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
---
TACAS'16,
Eindhoven,
Netherlands,
volume 9636 of LNCS,
pages 923--926,
2016.
Springer-Verlag.
A preliminary version is available here.
|
| 2015 |
|
-
O. Lengal.
Automata in Infinite-State Formal Verification.
Ph.D. thesis
(an abridged version).
FIT BUT,
Brno,
Czech Republic,
2015.
-
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),
pages 357--385,
2016.
Springer-Verlag.
A preliminary version is available here.
-
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,
United Kingdom,
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-06,
FIT BUT,
Brno,
Czech Republic,
2014.
The associated tool dWiNA 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,
London,
United Kingdom,
volume 9035 of LNCS,
pages 431--434,
2015.
Springer-Verlag.
A preliminary version is available here.
|
| 2014 |
|
-
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,
Singapore,
volume 8858 of LNCS,
pages 314--333,
2014.
Springer-Verlag.
A preliminary version is available here.
The slides from the presentation are available here.
An extended version appeared as the technical report
FIT-TR-2014-01,
FIT BUT,
Brno,
Czech Republic,
2014.
|
| 2013 |
|
-
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.
A preliminary version is available here.
An extended version appeared as the technical report
FIT-TR-2013-02,
FIT BUT,
Brno,
Czech Republic,
2013.
-
L. Holik,
O. Lengal,
A. Rogalewicz,
J. Simacek, 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 slides from the presentation are available here.
|
| 2012 |
| |
| 2011 |
|
-
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.
A preliminary version is available here.
The slides from the presentation are available here.
An extended version appeared as the technical report
FIT-TR-2011-04,
FIT BUT,
Brno,
Czech Republic,
2011.
|
| 2010 |
| |
| 2009 |
| |
| 2008 |
|
-
M. Zadnik,
J. Korenek,
P. Kobiersky, and
O. Lengal.
Network Probe for Flexible Flow Monitoring.
In Proc. of 2008 IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems
---
DDECS'08,
Bratislava,
Slovakia,
pages 213--218,
2008.
IEEE.
|
| | Show all publications
|
Faculty of Information Technology