Search Results

Documents authored by Strejcek, Jan

Document
DOI: 10.4230/DagRep.15.4.92
Information Exchange in Software Verification (Dagstuhl Seminar 25172)

Authors: Dirk Beyer, Marieke Huisman, Jan Strejček, and Heike Wehrheim

Published in: Dagstuhl Reports, Volume 15, Issue 4 (2025)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 25172 Information Exchange in Software Verification. The term "software verification" refers to the procedure of deciding the correctness of software with respect to (user-supplied or predefined) specifications. In general, software verification is an undecidable problem. Despite this undecidability, software verification is a very active research field with contributions of researchers from several areas such as theorem proving, deductive verification, static analysis, and automatic verification. The analysis techniques developed in these subareas are often complementary with respect to the type of software and specifications they can efficiently handle. The objective of this Dagstuhl Seminar was to bring together people working in these different subareas to discuss and advance ways of having tools and techniques cooperate on the task of software verification.
Cite as

Dirk Beyer, Marieke Huisman, Jan Strejček, and Heike Wehrheim. Information Exchange in Software Verification (Dagstuhl Seminar 25172). In Dagstuhl Reports, Volume 15, Issue 4, pp. 92-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{beyer_et_al:DagRep.15.4.92,
  author =	{Beyer, Dirk and Huisman, Marieke and Strej\v{c}ek, Jan and Wehrheim, Heike},
  title =	{{Information Exchange in Software Verification (Dagstuhl Seminar 25172)}},
  pages =	{92--111},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{15},
  number =	{4},
  editor =	{Beyer, Dirk and Huisman, Marieke and Strej\v{c}ek, Jan and Wehrheim, Heike},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.4.92},
  URN =		{urn:nbn:de:0030-drops-252559},
  doi =		{10.4230/DagRep.15.4.92},
  annote =	{Keywords: Competitions and Benchmarks, Data-Flow Analysis, Deductive Verification, Formal Verification, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.23
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Authors: Tereza Schwarzová, Jan Strejček, and Juraj Major

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
This paper presents a novel application of QBF solving to automata reduction. We focus on Transition-based Emerson-Lei automata (TELA), which is a popular formalism that generalizes many traditional kinds of automata over infinite words including Büchi, co-Büchi, Rabin, Streett, and parity automata. Transitions in a TELA are labelled with acceptance marks and its accepting formula is a positive Boolean combination of atoms saying that a particular mark has to be visited infinitely or finitely often. Algorithms processing these automata are often very sensitive to the number of acceptance marks. We introduce a new technique for reducing the number of acceptance marks in TELA based on satisfiability of quantified Boolean formulas (QBF). We evaluated our reduction technique on TELA produced by state-of-the-art tools of the libraries Owl and Spot and by the tool ltl3tela. The technique reduced some acceptance marks in automata produced by all the tools. On automata with more than one acceptance mark obtained by translation of LTL formulas from literature with tools Delag and Rabinizer 4, our technique reduced 27.7% and 39.3% of acceptance marks, respectively. The reduction was even higher on automata from random formulas.
Cite as

Tereza Schwarzová, Jan Strejček, and Juraj Major. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{schwarzova_et_al:LIPIcs.SAT.2023.23,
  author =	{Schwarzov\'{a}, Tereza and Strej\v{c}ek, Jan and Major, Juraj},
  title =	{{Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23},
  URN =		{urn:nbn:de:0030-drops-184859},
  doi =		{10.4230/LIPIcs.SAT.2023.23},
  annote =	{Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko}
}
Document
DOI: 10.4230/DagSemProc.06081.6
Reachability analysis of multithreaded software with asynchronous communication

Authors: Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations. This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.
Cite as

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:DagSemProc.06081.6,
  author =	{Bouajjani, Ahmed and Esparza, Javier and Schwoon, Stefan and Strejcek, Jan},
  title =	{{Reachability analysis of multithreaded software with asynchronous communication}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.6},
  URN =		{urn:nbn:de:0030-drops-7263},
  doi =		{10.4230/DagSemProc.06081.6},
  annote =	{Keywords: Model checking, pushdown systems, concurrency}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact