Fold/Unfold Transformations for Fixpoint Logic . . . . . . . . . . . . . . . . . . . . . 195
Naoki Kobayashi, Grigory Fedyukovich, and Aarti Gupta
Tools and Case Studies
Verifying OpenJDK’s LinkedList using KeY . . . . . . . . . . . . . . . . . . . . 217
Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer,
Marko van Eekelen, and Stijn de Gouw
Analysing installation scenarios of Debian packages . . . . . . . . . . . . . . . . . . 235
Benedikt Becker, Nicolas Jeannerod, Claude Marché,
Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen
Endicheck: Dynamic Analysis for Detecting Endianness Bugs . . . . . . . . . . . 254
Roman Kápl and Pavel Parízek
Describing and Simulating Concurrent Quantum Systems. . . . . . . . . . . . . . . 271
Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly,
and Rajagopal Nagarajan
EMTST: Engineering the Meta-theory of Session Types . . . . . . . . . . . . . . . 278
David Castro, Francisco Ferreira, and Nobuko Yoshida
Games and Automata
Solving Mean-Payoff Games via Quasi Dominions . . . . . . . . . . . . . . . . . . . 289
Massimo Benerecetti, Daniele Dell’Erba, and Fabio Mogavero
Partial-Order Reduction for Parity Games with an Application
on Parameterised Boolean Equation Systems . . . . . . . . . . . . . . . . . . . . . . . 307
Thomas Neele, Tim A. C. Willemse, and Wieger Wesselink
Polynomial Identification of x-Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 325
Dana Angluin, Dana Fisman, and Yaara Shoval
SV-COMP 2020
Advances in Automatic Software Verification: SV-COMP 2020 . . . . . . . . . . 347
Dirk Beyer
2LS: Heap Analysis and Memory Safety (Competition Contribution) . . . . . . . 368
Viktor Malík, Peter Schrammel, and Tomáš Vojnar
COASTAL: Combining Concolic and Fuzzing
for Java (Competition Contribution) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 373
Willem Visser and Jaco Geldenhuys
xxii
Contents – Part II