Our paper about Symbolic Model Checking Quantum Circuits in Maude has been accepted for publication in PeerJ Computer Science and selected for a JAIST press release (link). :tada: