This paper studies an extension of O'Hearn's incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit We show this can be mitigated by extending with underspecification. The resulting combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) underapproximation (it focus on fewer than all the paths). prove soundness proof system, as well completeness for a defined subset...

This paper tackles the important, difficult problem of detecting program inputs that trigger large floating-point errors in numerical code. It introduces a novel, principled dynamic analysis leverages mathematically rigorously analyzed condition numbers for atomic operations, which we call conditions , to effectively guide search errors. Compared with existing approaches, our work based on has several distinctive benefits: (1) it does not rely high-precision implementations act as...

Data flow testing (DFT) focuses on the of data through a program. Despite its higher fault-detection ability over other structural techniques, practical DFT remains significant challenge. This paper tackles this challenge by introducing hybrid framework: (1) The core our framework is based dynamic symbolic execution (DSE), enhanced with novel guided path search to improve performance, and (2) we systematically cast problem as reach checking in software model complement DSE-based approach,...

Data flow testing (DFT) focuses on the of data through a program. Despite its higher fault-detection ability over other structural techniques, practical DFT remains significant challenge. This paper tackles this challenge by introducing hybrid framework: (1) The core our framework is based dynamic symbolic execution (DSE), enhanced with novel guided path search to improve performance, and (2) we systematically cast problem as reach checking in software model complement DSE-based approach,...

Achieving high code coverage is essential in testing, which gives us confidence quality. Testing floating-point usually requires painstaking efforts handling constraints, e.g., symbolic execution. This paper turns the challenge of testing into opportunity applying unconstrained programming --- mathematical solution for calculating function minimum points over entire search space. Our core insight to derive a representing from program, any whose test input guaranteed exercise new branch...

Numerical code uses floating-point arithmetic and necessarily suffers from roundoff truncation errors. Error analysis is the process to quantify such uncertainty in solution a problem. Forward error backward are two popular paradigms of analysis. more intuitive has been explored automated by programming languages (PL) community. In contrast, although preferred numerical analysts foundation for stability, it less known unexplored PL To fill gap, this paper presents an empower both application...

Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach provably overapproximative x86-64 lifting. A stripped verified certain sanity properties such as return address integrity calling convention adherence. Establishing these allows be lifted that contains overapproximation of all possible execution paths binary. The disassembled instructions, reconstructed...

This work studies the connection between problem of analyzing floating-point code and that function minimization. It formalizes this as a reduction theory, where semantics program is measured generalized metric, called weak distance, which faithfully captures any given analysis objective. theoretically guaranteed minimizing distance (e.g., via mathematical optimization) solves underlying problem. theory provides general framework for numerical code. Two important separate analyses from...

A dependency bug is a software fault that manifests itself when accessing an unavailable asset. Dependency bugs are pervasive and we all hate them. This paper presents case study of in the Robot Operating System (ROS), applying mixed methods: qualitative investigation 78 reports, quantitative analysis 1354 ROS reports against 19553 top 30 GitHub projects, design three linters evaluated on 406 packages.

Achieving high code coverage is essential in testing, which gives us confidence quality. Testing floating-point usually requires painstaking efforts handling constraints, e.g., symbolic execution. This paper turns the challenge of testing into opportunity applying unconstrained programming --- mathematical solution for calculating function minimum points over entire search space. Our core insight to derive a representing from program, any whose test input guaranteed exercise new branch...

This paper presents Mathematical Execution (ME), a new, unified approach for testing numerical code. The key idea is to (1) capture the desired objective via representing function and (2) transform automated problem minimization of function. be solved mathematical optimization. main feature ME that it directs input space exploration by only executing function, thus avoiding static or symbolic reasoning about program semantics, which particularly challenging To illustrate this feature, we...

Numerical code uses floating-point arithmetic and necessarily suffers from roundoff truncation errors. Error analysis is the process to quantify such uncertainty in solution a problem. Forward error backward are two popular paradigms of analysis. more intuitive has been explored automated by programming languages (PL) community. In contrast, although preferred numerical analysts foundation for stability, it less known unexplored PL To fill gap, this paper presents an empower both application...

Lowering the precision of neural networks from prevalent 32-bit has long been considered harmful to performance, despite gain in space and time. Many works propose various techniques implement half-precision networks, but none study pure 16-bit settings. This paper investigates unexpected performance over classification tasks. We present extensive experimental results that favorably compare networks' those models. In addition, a theoretical analysis efficiency models is provided, which...

Reducing the number of bits needed to encode weights and activations neural networks is highly desirable as it speeds up their training inference time while reducing memory consumption. It unsurprising that considerable attention has been drawn developing employ lower-precision computation. This includes IEEE 16-bit, Google bfloat16, 8-bit, 4-bit floating-point or fixed-point, 2-bit, various mixed-precision algorithms. Out these low-precision formats, 16-bit stands out due its universal...

Achieving high code coverage is essential in testing, which gives us confidence quality. Testing floating-point usually requires painstaking efforts handling constraints, e.g., symbolic execution. This paper turns the challenge of testing into opportunity applying unconstrained programming --- mathematical solution for calculating function minimum points over entire search space. Our core insight to derive a representing from program, any whose test input guaranteed exercise new branch...