embedded software engineers

Abstract: Bounded model checking unrolls a program into a single formula, so a function holding a loop costs the solver a fresh copy of that loop at every call site. Function contracts break that coupling. Verify the body once against its contract, then replace each call by a stub derived from it. CBMC supports this through dynamic frame condition checking, applied at industrial scale, but with no formal account of why the replacement is sound and no characterisation of what the frame check costs. We present the function-contract framework for ESBMC. The clause syntax, both phases, and the first assigns enforcement the tool has had are all introduced here. Its technical core is an observational frame rule: snapshot the locations the contract does not permit the function to write, then compare them at exit. The encoding emits a number of verification conditions set by how many globals the program has, not by how many writes the body performs, while dynamic frame condition checking grows with the write count. That is a property of the encoding rather than a timing, so it moves with neither the machine nor the solver. The rule itself is the classical one; what we add is its bounded form inside a BMC encoding, with the pipeline's algebraic skeleton machine-checked in Lean 4 and the limits of that model stated. We evaluate on synthetic sweeps, SV-COMP tasks, an ANSSI X.509 parser, the FreeRTOS heap_1 allocator, and the ML-KEM reference implementation whose CBMC contracts we reuse unchanged. At the coefficient count FIPS-203 mandates, neither tool finishes on the monolithic route inside ten minutes, and both finish on the modular one. The framework is merged into ESBMC master. Contracts are what is left when unrolling runs out of room.

Abstract: The theoretical foundation for model checking timed systems against Metric Interval Temporal Logic (MITL) was established in the early 1990s, yet the first practical tool supporting future MITL (MightyL) did not emerge until 2017. Recently, there has been growing interest in extending this toolchain to support more expressive logical operators, including past modalities, Pnueli modalities, and limited use of singular intervals. MightyPPL is one such toolchain. We introduce an upgraded version of MIghtyPPL that enables for the first time, the model checking of Metric Temporal Logic (MTL) properties of the form (whenever an event p occurs, it is eventually followed by some event q after exactly some k time units) in addition to Pnueli and Past modalities. We discuss the tool's underlying architecture and implementation, and present a performance evaluation against the Tempora tool across diverse satisfiability and model checking benchmarks, demonstrating that MightyPPL delivers significantly better performance.

Abstract: Resource constrained single-board computers including Raspberry Pi, NVIDIA Jetson Nano, Arduino UNO Q, Orange Pi, and LattePanda motivate on-device small language model (SLM) agents that reduce cloud dependence, improve data locality, and tolerate intermittent connectivity. Model Context Protocol (MCP)-style tool invocation demands more than fluent generation: an agent must emit machine-readable JSON, select the correct tool, supply all required arguments, and avoid unintended actions. We establish a platform-agnostic CPU baseline by evaluating five open-weight models below two billion parameters Phi-1.5, Pythia-1.4B, TinyLlama-1.1B-Chat, Qwen2.5-0.5B, and Qwen2.5-1.5B on 100 prompts spanning weather retrieval, web search, calculation, email composition, and task creation, under greedy decoding and nucleus sampling. A recovery parser strips Markdown fences, extracts brace-delimited substrings, and scores parseability, tool-name correctness, argument completeness, and value agreement. Under this criterion, Qwen2.5-1.5B achieves 75% (greedy) and 79% (sampling); Qwen2.5-0.5B achieves 72% (greedy) but drops to 32% under sampling. Phi-1.5 scores 0%; Pythia and TinyLlama reach at most 7%. A strict post-hoc audit finds only 5 of 1,000 raw responses directly parseable as JSON, exposing near-total dependence on output recovery. A CPU resource probe shows Qwen2.5-1.5B requires 7,960 MiB and 30.782 s mean latency; Qwen2.5-0.5B uses 3,637 MiB and 10.627 s, revealing a reliability-resource trade-off for edge deployment. These results do not cover the named boards directly or a full MCP implementation. Safe deployment requires schema validation, constrained generation, least-privilege execution, and human escalation for consequential actions.