Contents – Part II
Bisimulation
An O(m log n) algorithm for branching bisimilarity on labelled
transition systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, and Anton Wijs
Verifying Quantum Communication Protocols with Ground Bisimulation . . . .
21
Xudong Qin, Yuxin Deng, and Wenjie Du
Deciding the Bisimilarity of Context-Free Session Types . . . . . . . . . . . . . . .
39
Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos
Sharp Congruences Adequate with Temporal Logics Combining Weak
and Strong Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
57
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
Verification and Efficiency
How Many Bits Does it Take to Quantize Your Neural Network?. . . . . . . . .
79
Mirco Giacobbe, Thomas A. Henzinger, and Mathias Lechner
Highly Automated Formal Proofs over Memory Usage of Assembly Code . . .
98
Freek Verbeek, Joshua A. Bockenek, and Binoy Ravindran
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. . . . . 118
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez,
and Albert Rubio
CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering . . . . . 126
Dirk Beyer and Philipp Wendler
Logic and Proof
Practical Machine-Checked Formalization of Change Impact Analysis . . . . . . 137
Karl Palmskog, Ahmet Celik, and Milos Gligoric
What’s Decidable About Program Verification Modulo Axioms? . . . . . . . . . 158
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
Formalized Proofs of the Infinity and Normal Form Predicates
in the First-Order Theory of Rewriting. . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
Alexander Lochmann and Aart Middeldorp