Springer anti-typesetters, part 1

This post describes (only some) of my frustrations with Springer’s typesetting of one paper (Saan et al., 2024) in December 2023 and was also written around that time, but not published. It compares our submitted camera-ready version (which is very similar to the nicely-formatted arXiv version) with the proofs from Springer typesetters.

Discrediting other authors

In our paper the citation “Beyer and Strejček [23]” was edited by Springer to simply “Strejček [23]”, discrediting Dirk Beyer. We used \citet{Beyer2022} in LaTeX and both authors are still listed in the corresponding References entry. The cited paper is published via Springer, so they should have no doubt about the authorship. What reason would Springer have to replace \citet with a reduced authors list which is no longer consistent with References? Or how would one do that accidentally?

Reformatting tables entirely

We use the booktabs LaTeX package to typeset beautiful professional tables. For whatever reason Springer entirely reformats tables:

Vertical column-separating rules are added between all columns.
All columns are left-aligned. That is especially bad for numeric data spanning multiple orders of magnitude. Our tables with siunitx columns that properly align digits and decimal points were ruined. Columns of centered checkmarks and crosses became awkward. Centered \multicolumn spans became odd.
The font for tables was changed to something not matching the rest of the paper.

Nothing in the Springer guidelines requires any of such changes to tables, instead requiring:

It is essential that all illustrations are clear and legible.

By unnecessarily reformatting all tables, Springer editors have done the complete opposite of their own guidelines.

Comparisons

The following image comparisons illustrate the pessimization from our camera-ready version to Springer’s proof (it’s very easy to tell which side is which version). Hover/swipe across the images to fully appreciate the horror.

Table 1

Extra ugly is how the vertical rules have gaps in them and some cells are not completely colored.

Table 2

History

Apparently, this behavior is far from new: Dmytro Mishkin already complained about it in 2018. Meanwhile in the first half of 2023, booktabs tables were fine again, as evidenced by some of our papers. Clearly, Springer lacks any kind of policy on this and their typesetters are rulers of a wild west, each making up their own rules.

Making references inconsistent

Abbreviating partially

We explicitly edited our BibTeX bibliography to be consistent across all entries, in particular about booktitles/journals. As provided by Springer Link, we used unabbreviated names like “Static Analysis” and “Tools and Algorithms for the Construction and Analysis of Systems”. Springer says:

References are also modified to make them compatible with CrossRef, which will permit cross referencing within SpringerLink […]

Fair enough, they abbreviated such names to, e.g., SAS and TACAS. However, their editing is completely inconsistent: some entries use abbreviations, while others still have full names for the very same proceedings/journals.

Editing titles

We cite two papers which have the tool name Goblint set in small caps in their title. As provided by Springer Link, we did not have small caps in our bibliography. Springer edited one to use small caps, but left the other (right after the first) in normal font. If there were any policy, then it should be enforced consistently by Springer Link and Springer editors, or at minimum be consistent within a single References section.

Furthermore, Springer typesetters like to remove all crucial capitalization from cited titles:

replacing “C programs” with “c programs”,
replacing “Frama-C” with “frama-c”,
replacing “CommuHash” with “commuhash”.

Adding random dots

We reference items in a prior enumerate like “Items 2 and 4 illustrate”, which was edited by Springer to “Items 2 and 4. illustrate”. The additional dot was consistently (!) throughout the paper added after item number 4 (multiple instances of “Item 4 from Example 4” were changed to “Item 4. from Example 4”). But all other item references into the same list did not get a dot — Springer randomly did it to Item 4.

Conclusion

After listing every occurrence of all of these issues explicitly in the response to typesetting proofs, Springer did manage to fix (i.e., undo) most, but not all, of these issues. In the publisher’s version the tables still aren’t as nice as our original version.

~~Stay tuned for~~ Check out part 2!

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.