Concrete Semantics of Programs with Non-Deterministic and Random Inputs

TL;DR

This paper defines the semantics of C-like programs that interact with noisy, imprecise external environments, providing a formal foundation for reasoning about such programs.

Contribution

It introduces a formal semantics framework for programs with non-deterministic and random inputs, addressing the challenges of noisy environment interactions.

Findings

Formal semantics for noisy environment interactions

Framework for reasoning about non-deterministic inputs

Foundation for analyzing programs with imprecise data

Abstract

This document gives semantics to programs written in a C-like programming language, featuring interactions with an external environment with noisy and imprecise data.