arxiv: 2604.16153 · v1 · submitted 2026-04-17 · 💻 cs.LO

Recognition: unknown

The QBF Gallery 2023

Simone Heisinger , Luca Pulina , Martina Seidl

Authors on Pith no claims yet

Pith reviewed 2026-05-10 07:20 UTC · model grok-4.3

classification 💻 cs.LO

keywords QBFQuantified Boolean FormulasBenchmarkingSolver EvaluationQBF GalleryPerformance AnalysisAutomated Reasoning

0 comments

The pith

The QBF Gallery 2023 releases a consolidated public benchmark set for comparing QBF solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper surveys the state of the art in solving quantified Boolean formulas by collecting solvers and formulas submitted to the QBF Gallery 2023. It constructs a new consolidated benchmark set that combines previously well-evaluated formulas with the new submissions and makes this set available to the public. Using this set, the authors perform a comparative analysis of the submitted solvers as well as other publicly available ones to assess their performance. This work documents current capabilities in the field and outlines ideas for future editions of the gallery to support ongoing research and benchmarking.

Core claim

By merging well-evaluated formulas with submitted instances into a publicly available benchmark set, the QBF Gallery 2023 enables a detailed comparative analysis of QBF solvers, revealing their current performance levels and informing directions for future development in quantified Boolean formula solving.

What carries the argument

The consolidated benchmark set combining well-evaluated formulas with submitted QBF instances, used to evaluate solver performance.

If this is right

The public availability of the benchmark set allows independent verification and further testing by the community.
Comparative analysis highlights strengths and weaknesses of different solving approaches.
Discussion of the gallery's status suggests ways to enhance future events for better community support.
Researchers gain a standardized resource to track advancements in QBF technology.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This approach of consolidation could be extended to other domains of automated reasoning to create more robust evaluation standards.
Over time, repeated use of this set might help identify specific problem classes where solvers still struggle.
The analysis might encourage development of new solvers targeting weaknesses uncovered in the comparisons.

Load-bearing premise

The collection of submitted solvers and formulas, together with the chosen well-evaluated ones, accurately reflects the broader landscape of QBF solving challenges and capabilities.

What would settle it

Observing that solver performance rankings change substantially when evaluated on the consolidated set versus the well-evaluated formulas alone would question the representativeness of the new benchmark.

read the original abstract

The QBF Gallery 2023, the last QBF evaluation event, continues the tradition to survey and document the state of the art in solving quantified Boolean formulas (QBFs). It provides a detailed overview by collecting newly developed solvers and formulas as benchmarks. This report documents the solvers and formulas submitted by the community and introduces a new, consolidated benchmark set that combines well-evaluated formulas with the submitted instances. The resulting formula set is made publicly available. With this benchmark set, we conduct a comparative analysis of the submitted solvers and publicly available solvers, assessing their performance and current capabilities. In addition, we report on the present status of the QBF Gallery and discuss ideas and directions for future editions to further support research and benchmarking within the QBF community.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

A routine but useful community report that ships a new public QBF benchmark set and solver comparison from the 2023 gallery.

read the letter

This paper is the final report from the QBF Gallery series. The authors collected solver and formula submissions for 2023, merged the new instances with a set of previously well-evaluated formulas, released the combined benchmark publicly, and ran a head-to-head comparison of the submitted solvers plus some existing ones. That is the core of the work. The public data release and the performance numbers are the parts that actually matter to people working on QBF solvers. The report also notes that this was the last gallery and sketches a few ideas for future community benchmarking. Those elements are straightforward and match what these events have done in prior years. The facts line up with the stress-test note: the paper does not claim the benchmark is representative or unbiased; it simply records what arrived and what the runs showed. No load-bearing assumptions or derivations are present, so the descriptive nature does not create circularity problems. The main limitation is obvious and expected: this is infrastructure documentation rather than a technical advance. The solver comparison uses standard metrics and does not introduce new analysis techniques or statistical depth. The future-directions section stays high-level. For anyone outside the narrow QBF evaluation community the paper adds little. Inside that community the consolidated benchmark and the 2023 numbers are worth having on record. I would bring the benchmark data itself to a reading group if the goal was to pick new test instances, but not the paper. It is not something I would cite in my own technical work. Still, the activity of running these galleries and releasing the data supports the subfield, so a serious editor should send it to peer review rather than desk-reject it. The review would mainly check that the data release is complete and that the reported runs are reproducible.

Referee Report

0 major / 2 minor

Summary. The manuscript reports on the QBF Gallery 2023, documenting solvers and formulas submitted by the community, introducing a new consolidated benchmark set that combines well-evaluated formulas with the submitted instances, making the resulting set publicly available, conducting a comparative analysis of the submitted solvers and publicly available solvers, and discussing the current status of the QBF Gallery along with ideas for future editions.

Significance. If the claims hold, the work is significant because it consolidates and publicly releases a benchmark set for QBF solving, which directly supports reproducibility, standardized evaluations, and tracking of progress in the field. The comparative analysis provides a snapshot of current solver capabilities, and the discussion of future directions helps sustain community efforts in QBF research and benchmarking.

minor comments (2)

Abstract: the claim that the consolidated benchmark set 'combines well-evaluated formulas with the submitted instances' would benefit from a brief statement of the selection criteria or number of formulas involved to allow readers to assess the scale and construction process.
The section describing the comparative analysis: the report should explicitly state the hardware, time limits, and any data exclusion rules used in the solver runs to ensure the performance comparison is fully reproducible from the public benchmark set.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our manuscript on the QBF Gallery 2023. We appreciate the recognition that our work consolidates and publicly releases a benchmark set, supports reproducibility, and provides a useful snapshot of solver capabilities along with directions for future community efforts. The recommendation for minor revision is noted.

Circularity Check

0 steps flagged

No significant circularity in descriptive community report

full rationale

The paper is a purely descriptive report on the 2023 QBF Gallery. It collects and documents submitted solvers and formulas, consolidates them with prior well-evaluated instances into a public benchmark set, and reports comparative solver performance on that set. No derivations, predictions, fitted parameters, or mathematical claims are present that could reduce by construction to the paper's own inputs or self-citations. All central statements are factual accounts of external community submissions and executed runs, with no load-bearing self-referential steps.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is a community survey and benchmarking report with no mathematical derivations, fitted parameters, background axioms, or postulated entities.

pith-pipeline@v0.9.0 · 5420 in / 1101 out tokens · 41272 ms · 2026-05-10T07:20:16.852005+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

52 extracted references · 35 canonical work pages

[1]

Olaf Bayersdorﬀ, Mikolá Janota, Florian Lonsing, and Martina Seidl. 2021. Quan- tiﬁed Boolean Formulas. In Handbook of Satisﬁability Second Edition Part 2 , pp. 1177–1222. The QBF Gallery 2023 35

2021
[2]

Daniel Le Berre, Massimo Narizzano, Laurent Simon, and Armando Tacchella
[3]

The Second QBF Solvers Comparative Evaluation. In Theory and Applica- tions of Satisﬁability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers (Lecture Notes in Com- puter Science , volume 3542). Springer, pp. 376–392. doi: 10.1007/11527695_28

work page doi:10.1007/11527695_28 2004
[4]

Daniel Le Berre, Laurent Simon, and Armando Tacchella. 2003. Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers. In Theory and Applications of Satisﬁability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers (Lecture Notes in Computer Science, volume 2919). Springer, pp. 46...

work page doi:10.1007/978-3-540-24605-3_35 2003
[5]

Armin Biere, Florian Lonsing, and Martina Seidl. 2011. bloqqer. https://fmv.jku .at/bloqqer/. Accessed: 2025-11-25. (2011)

2011
[6]

Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lons- ing, and Martina Seidl. 2018. Expansion-Based QBF Solving Without Recursion. CoRR, abs/1807.08964. arXiv: 1807.08964. http://arxiv.org/abs/1807.08964

work page arXiv 2018
[7]

Bryant and Marijn J

Randal E. Bryant and Marijn J. H. Heule. 2021. Dual Proof Generation for Quanti- ﬁed Boolean Formulas with a BDD-based Solver. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings (Lecture Notes in Computer Science , volume 12699). Springer, pp. 433–449. doi: 10.1007/978-3-03...

work page doi:10.1007/978-3-030-79876-5_25 2021
[8]

Luis Cereceda, Jan van den Heuvel, and Matthew Johnson. 2008. Connectedness of the graph of vertex-colourings. Discret. Math. , 308, 5-6, 913–919. doi: 10.1016 /J.DISC.2007.07.028

2008
[9]

Günther Charwat and Stefan Woltran. 2016. BDD-based dynamic programming on tree decompositions. Database and Artiﬁcial Intelligence Group, TU Wien, Tech. Rep. DBAI-TR-2016-95

2016
[10]

Uwe Egly, Martina Seidl, Hans Tompits, Stefan Woltran, and Michael Zolda. 2003. Comparing Diﬀerent Prenexing Strategies for Quantiﬁed Boolean Formulas. In The- ory and Applications of Satisﬁability Testing, 6th International Conference, SAT

2003
[11]

Springer, pp

Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers (Lec- ture Notes in Computer Science , volume 2919). Springer, pp. 214–228. doi: 10.10 07/978-3-540-24605-3_17

2003
[12]

Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. 2021. SAT Competition 2020. Artif. Intell. , 301, 103572. doi: 10.1016/J.ARTINT.2021 .103572

work page doi:10.1016/j.artint.2021 2021
[13]

Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, and Bernd Becker. 2015. Solving DQBF through quantiﬁer elimination. In Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE The QBF Gallery 2023 36 2015, Grenoble, France, March 9-13, 2015 . ACM, pp. 1617–1622. http://dl.acm.o rg/citation.cfm?id=2757188

2015
[14]

Jesko Hecking-Harbusch and Leander Tentrup. 2018. Solving QBF by Abstraction. In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Veriﬁcation, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018 (EPTCS, volume 277), pp. 88–102. doi: 10.4204/EPTCS.277.7

work page doi:10.4204/eptcs.277.7 2018
[15]

Maximilian Heisinger. 2024. Encoding, Solving, and Benchmarking for SAT and Extensions. eng. (2024). https://resolver.obvsg.at/urn:nbn:at:at-ubl:1-81292

2024
[16]

Maximilian Heisinger, Simone Heisinger, and Martina Seidl. 2024. Booleguru, the Propositional Polyglot (Short Paper). In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I (Lecture Notes in Computer Science , volume 14739). Springer, pp. 315–324. doi: 10.1007/978-3-031-63498-7_19

work page doi:10.1007/978-3-031-63498-7_19 2024
[17]

Simone Heisinger, Maximilian Heisinger, Adrian Rebola-Pardo, and Martina Seidl
[18]

In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I (Lecture Notes in Computer Science , volume 14739)

Quantiﬁer Shifting for Quantiﬁed Boolean Formulas Revisited. In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I (Lecture Notes in Computer Science , volume 14739). Springer, pp. 325–343. doi: 10.1007/978-3-031-63498-7_20

work page doi:10.1007/978-3-031-63498-7_20 2024
[19]

Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez. 2021. HyperQube: A QBF-Based Bounded Model Checker for Hyperproperties. CoRR, abs/2109.12989. arXiv: 2109.12989. https://arxiv.org/abs/2109.12989

work page arXiv 2021
[20]

Mikolás Janota. 2018. Circuit-Based Search Space Pruning in QBF. In Theory and Applications of Satisﬁability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science , volume 10929). Springer, pp. 187–198. doi: 10.100...

work page doi:10.1007/978-3-319-94144-8_12 2018
[21]

Mikolás Janota. 2017. QFUN: Towards Machine Learning in QBF. CoRR, abs/1710.02198. arXiv: 1710.02198. http://arxiv.org/abs/1710.02198

work page arXiv 2017
[22]

Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, and Allen Van Gelder. 2014. The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. J. Satisf. Boolean Model. Comput. , 9, 1, 187–206. doi: 10.3233/S AT190108

work page doi:10.3233/s 2014
[23]

Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke
[24]

Solving QBF with counterexample guided reﬁnement. Artif. Intell. , 234, 1–
[25]

The QBF Gallery 2023 37

doi: 10.1016/J.ARTINT.2016.01.004. The QBF Gallery 2023 37

work page doi:10.1016/j.artint.2016.01.004 2016
[26]

William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke. 2010. A Non- prenex, Non-clausal QBF Solver with Game-State Learning. In Theory and Appli- cations of Satisﬁability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science, volume 6175). Springer, pp. 128–142....

work page doi:10.1007/978-3-642-14186-7_12 2010
[27]

Florian Lonsing and Uwe Egly. 2017. DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. In Automated Deduction - CADE 26 - 26th Inter- national Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings (Lecture Notes in Computer Science , volume 10395). Springer, pp. 371–384. doi: 10.1007/978-3-319-63046-5_23

work page doi:10.1007/978-3-319-63046-5_23 2017
[28]

Florian Lonsing and Uwe Egly. 2019. QRATPre+: Eﬀective QBF Preprocessing via Strong Redundancy Properties. In Theory and Applications of Satisﬁability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings (Lecture Notes in Computer Science , volume 11628). Springer, pp. 203–210. doi: 10.1007/978-3-030...

work page doi:10.1007/978-3-030-24258-9_14 2019
[29]

Florian Lonsing, Martina Seidl, and Allen Van Gelder. 2016. The QBF Gallery: Behind the scenes. Artif. Intell. , 237, 92–114. doi: 10.1016/J.ARTINT.2016.04.00 2

work page doi:10.1016/j.artint.2016.04.00 2016
[30]

Massimo Narizzano, Luca Pulina, and Armando Tacchella. 2006. Report of the Third QBF Solvers Evaluation. J. Satisf. Boolean Model. Comput. , 2, 1-4, 145–

2006
[31]

doi: 10.3233/SAT190019

work page doi:10.3233/sat190019
[32]

Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. 2019. Dependency Learning for QBF. J. Artif. Intell. Res. , 65, 180–208. doi: 10.1613/JAIR.1.11529

work page doi:10.1613/jair.1.11529 2019
[33]

Claudia Peschiera, Luca Pulina, and Armando Tacchella. 2010. Designing a solver competition: the QBFEV AL’10 case study. In Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, EMSQMS 2010, Edinburgh, UK, July 20, 2010 (EPiC Series in Computing ). Aaron Stump, Geoﬀ Sutcliﬀe, and Cesare Tinelli, (Eds.) EasyChair, pp. 19–32. doi: 1...

work page doi:10.29007/cv3b 2010
[34]

Claudia Peschiera, Luca Pulina, Armando Tacchella, Uwe Bubeck, Oliver Kull- mann, and Inês Lynce. 2010. The Seventh QBF Solvers Evaluation (QBFEV AL’10). In Theory and Applications of Satisﬁability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science , volume 6175). Sp...

work page doi:10.1007/9 2010
[35]

Luca Pulina. 2016. The Ninth QBF Solvers Evaluation - Preliminary Report. In Proceedings of the 4th International Workshop on Quantiﬁed Boolean Formulas (QBF 2016) co-located with 19th International Conference on Theory and Applica- tions of Satisﬁability Testing (SAT 2016), Bordeaux, France, July 4, 2016 (CEUR The QBF Gallery 2023 38 Workshop Proceedings...

2016
[36]

Luca Pulina and Martina Seidl. 2019. The 2016 and 2017 QBF solvers evaluations (QBFEV AL’16 and QBFEV AL’17). Artif. Intell. , 274, 224–248. doi: 10.1016/J.A RTINT.2019.04.002

work page doi:10.1016/j.a 2019
[37]

Rabe and Leander Tentrup

Markus N. Rabe and Leander Tentrup. 2015. CAQE: A Certifying QBF Solver. In Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015 . IEEE, pp. 136–143. doi: 10.1109/FMCAD.2015.7542263

work page doi:10.1109/fmcad.2015.7542263 2015
[38]

Franz-Xaver Reichl and Friedrich Slivovsky. 2022. Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisﬁa- bility Testing, SAT 2022, Haifa, Israel, August 2-5, 2022 (LIPIcs, volume 236). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 20:1–20:10. doi: 10.4230/LIPI CS.SAT.2022.20

work page doi:10.4230/lipi 2022
[39]

Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. 2023. Circuit Mini- mization with QBF-Based Exact Synthesis. In Thirty-Seventh AAAI Conference on Artiﬁcial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Appli- cations of Artiﬁcial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artiﬁcial Intelligence, ...

work page doi:10.1609/aaai.v37i4.25524 2023
[40]

Tereza Schwarzová, Jan Strejcek, and Juraj Major. 2023. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. In 26th International Confer- ence on Theory and Applications of Satisﬁability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy (LIPIcs, volume 271). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 23:1–23:20. doi: 10.4230/LIPICS.S...

work page doi:10.4230/lipics.sat.2023.23 2023
[41]

Irfansha Shaik, Valentin Mayer-Eichberger, Jaco van de Pol, and Abdallah Saf- ﬁdine. 2023. Implicit State and Goals in QBF Encodings for Positional Games (extended version). CoRR, abs/2301.07345. doi: 10 . 48550 / ARXIV . 2301 . 07345. arXiv: 2301.07345

work page arXiv 2023
[42]

Irfansha Shaik and Jaco van de Pol. 2022. Classical Planning as QBF without Grounding. In Proceedings of the Thirty-Second International Conference on Au- tomated Planning and Scheduling, ICAPS 2022, Singapore (virtual), June 13-24,

2022
[43]

AAAI Press, pp. 329–337
[44]

Irfansha Shaik and Jaco van de Pol. 2023. Concise QBF Encodings for Games on a Grid (extended version). CoRR, abs/2303.16949. doi: 10.48550/ARXIV.2303.16

work page doi:10.48550/arxiv.2303.16 2023
[45]

Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. 2019. A Survey on Ap- plications of Quantiﬁed Boolean Formulas. In Proc. of the 31st IEEE International The QBF Gallery 2023 39 Conference on Tools with Artiﬁcial Intelligence, (ICTAI 2019) . IEEE, pp. 78–84. doi: 10.1109/ICTAI.2019.00020

work page doi:10.1109/ictai.2019.00020 2019
[46]

Juraj Síc and Jan Strejcek. 2021. DQBDD: An Eﬃcient BDD-Based DQBF Solver. In Theory and Applications of Satisﬁability Testing - SAT 2021 - 24th Interna- tional Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Lecture Notes in Computer Science , volume 12831). Springer, pp. 535–544. doi: 10.1007/978-3-030 -80223-3_36

work page doi:10.1007/978-3-030 2021
[47]

Friedrich Slivovsky. 2024. miniQU. https://github.com/fslivovsky/miniQU . Ac- cessed: 2025-11-24. (2024)

2024
[48]

David Speck, Paul Höft, Daniel Gnad, and Jendrik Seipp. 2023. Finding Matrix Multiplication Algorithms with Classical Planning. In Proceedings of the Thirty- Third International Conference on Automated Planning and Scheduling, July 8-13, 2023, Prague, Czech Republic . AAAI Press, pp. 411–416. doi: 10.1609/ICAPS.V3 3I1.27220

work page doi:10.1609/icaps.v3 2023
[49]

and Meyer, Albert R

Larry J. Stockmeyer and Albert R. Meyer. 1973. Word Problems Requiring Expo- nential Time: Preliminary Report. In Proceedings of the 5th Annual ACM Sympo- sium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA . ACM, pp. 1–9. doi: 10.1145/800125.804029

work page doi:10.1145/800125.804029 1973
[50]

Leander Tentrup. 2016. Non-prenex QBF Solving Using Abstraction. In Theory and Applications of Satisﬁability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Lecture Notes in Computer Science , volume 9710). Springer, pp. 393–401. doi: 10.1007/978-3-319-40970-2_24

work page doi:10.1007/978-3-319-40970-2_24 2016
[51]

Leander Tentrup. 2017. On Expansion and Resolution in CEGAR Based QBF Solving. In Computer Aided Veriﬁcation - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science , volume 10427). Springer, pp. 475–494. doi: 10.1007/978-3-3 19-63390-9_25

work page doi:10.1007/978-3-3 2017
[52]

Ralf Wimmer, Sven Reimer, Paolo Marin, and Bernd Becker. 2017. HQSpre - An Eﬀective Preprocessor for QBF and DQBF. In Tools and Algorithms for the Con- struction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Soft- ware, ETAPS 2017, Uppsala, Sweden, April 22-29,...

work page doi:10.1007/978-3 2017