The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
[mc]square: A Model Checker for Microcontroller Code
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
The paper presents details of a model checker for microcontroller-based embedded systems, called [mc] square. The purpose of the tool is to make model checking technology applicable in an embedded systems industry context. Consequently, it does not implement new theory but combines existing techniques to achieve the necessary efficiency and usability in a novel application area. One of the pragmatic requirements has been that model checking must be possible without any kind of manual preprocessing of the code. In its core, [mc]square is an explicit state, CTL model checker which builds the state space from the hardware-specific assembly code. The paper describes the tool features in detail and illustrates its abilities using two realistic examples.
@misc{schlich2006mcsquare,
title = {[mc]square: A Model Checker for Microcontroller Code},
author = {Bastian Schlich and Stefan Kowalewski},
year = {2006},
pages = {466--473},
doi = {10.1109/isola.2006.62},
}