Our journal-sized extension of the ICTAC’23 paper on “Modular Soundness Checking of Feature Model Evolution Plans” is finally out!

In this version, we included all the nitty-gritty details, and Charaf and I ported an older Maude-based approach to Haskell and added some performance evaluation. Runtime performance in a TCS paper?!, you’re asking? Well, why not (and Reviewer #2 asked for it, and Reviewer #4 looked as confused as you’re doing probably right now 😉). Found a great Haskell library (Criterion) to do just that along the way!

Here’s Elsevier’s direct link to our Open Access paper: https://authors.elsevier.com/sd/article/S0304-3975(25)00389-5. The HTML is fun to look at, gigantic maths symbols all over the place. Oh, and tons of tracking links…

In case this goes belly-up, we Norwegians archive everything in Cristin (which will soon get the axe in favour for a new national archive), so you can also go there for another year or so: https://app.cristin.no/results/show.jsf?id=2392980

This way to the artefact: https://zenodo.org/records/14841339

Fun collaboration, and shows that you often need to pull in people with different skills to get an idea to shine!

This also brings my personal number of failed industrial-sized Coq/Rocq proof attempts to three, I think…Ulises did the heavy lifting in the beginning, and we did some of the easier proofs. From there we did an extrapolation: we had 9 semantic rules, and were hence looking at 81 distinc top-level cases. At the pace of the initial proofs, our lack of experience with LTAC and no other good ideas about proof automation, we estimated we’d be finished with the mechanization sometime around … 2027 (we also have other things to do, who’d have thought)!

Can’t wait to find out what my failed-industrial-sized-Rocq-project #4, undoubtedly with LTAC2, will be!¡!

Elsevier also reminded us to go onto social media and share our news, so I’ll do that now — and I’ll have to find out what this “Google+” and “Twitter” is that Elsevier talked about in their email.