This work introduces StageSAT , a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages, each with increasing precision. It begins with a fast, projection-aided descent objective to efficiently guide the search toward a feasible region, then proceeds to bit-level accuracy with units-in-the-last-place (ULP) 2 optimization and a final n -ULP lattice refinement to ensure correctness. By construction, the final two stages use a representing function that evaluates to zero if and only if a candidate satisfies all constraints. Thus, whenever optimization drives the bit-precise objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness (no spurious SAT results). To further improve the search, StageSAT introduces a partial monotone descent property on linear constraints via an orthogonal projection technique, which prevents the optimizer from stalling on flat or misleading objective landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions of floating-point arithmetic; it treats complex arithmetic as a black box, using runtime evaluations to navigate the input space. We implement StageSAT and evaluate it on extensive benchmarks, including the SMT-COMP’25 floating-point suites and difficult cases from prior work. In our experiments, StageSAT proved both more scalable and more accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget – in fact, StageSAT found most of the satisfiable instances in our benchmarks and never produced a spurious model for an unsatisfiable formula. This amounts to 99.4% recall on satisfiable cases with 0% false SAT in our benchmarks, exceeding the reliability of prior optimization-based solvers we tested. StageSAT also delivered significant speedups (often 5–10× faster) over traditional bit-precise SMT solvers and earlier numeric solvers. These results demonstrate that our staged optimization strategy can significantly improve both the performance and correctness of floating-point satisfiability solving.

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 backwards reasoning. We show t at this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries- closed-form symbolic representations that summarize the effects of executing an entire loop at once- is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle/HOL theorem prover.

Designing a fallback authentication that is both memorable and strong poses a challenging task due to the need for authentication secrets to remain secure and easily recallable without frequent reinforcement. This could be especially prevalent for cloud computing security and resiliency. Inspired by the robust visual-spatial memory and associative memory of individuals, we introduce AuthZit, a novel system. AuthZit encodes authentication secrets as paths implementing a fault-tolerant algorithm through a 3D map of real-life places, navigated in both first person and 2D bird’s-eye perspective, coupled with a loci-tag (textual secret) associated with the location. Two experiments were conducted to iteratively design and evaluate AuthZit. First, it was observed that visual-spatial secrets are most memorable when navigated through a combination of 3D first-person and 2D bird’s-eye view perspectives. Second, we evaluated AuthZit against security questions and Android’s 9-dot pattern lock across three dimensions: memorability, security, and speed. AuthZit’s complexity-controlled secrets were significantly more memorable after three months, more resilient to shoulder surfing, and close adversaries.

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 to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel’s Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then – under the generated assumptions – the lifted representation is correct.

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 that leverages the mathematically rigorously analyzed condition numbers for atomic numerical operations, which we call atomic conditions , to effectively guide the search for large floating-point errors. Compared with existing approaches, our work based on atomic conditions has several distinctive benefits: (1) it does not rely on high-precision implementations to act as approximate oracles, which are difficult to obtain in general and computationally costly; and (2) atomic conditions provide accurate, modular search guidance. These benefits in combination lead to a highly effective approach that detects more significant errors in real-world code (e.g., widely-used numerical library functions) and achieves several orders of speedups over the state-of-the-art, thus making error analysis significantly more practical. We expect the methodology and principles behind our approach to benefit other floating-point program analysis tasks such as debugging, repair and synthesis. To facilitate the reproduction of our work, we have made our implementation, evaluation data and results publicly available on GitHub at https://github.com/FP-Analysis/atomic-condition.

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

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

Data flow testing (DFT) focuses on the flow of data through a program. Despite its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on dynamic symbolic execution (DSE), enhanced with a novel guided path search to improve testing performance, and (2) we systematically cast the DFT problem as reach ability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches' respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasible test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results.

Numerical code uses floating-point arithmetic and necessarily suffers from roundoff and truncation errors. Error analysis is the process to quantify such uncertainty in the solution to a problem. Forward error analysis and backward error analysis are two popular paradigms of error analysis. Forward error analysis is more intuitive and has been explored and automated by the programming languages (PL) community. In contrast, although backward error analysis is more preferred by numerical analysts and the foundation for numerical stability, it is less known and unexplored by the PL community. To fill the gap, this paper presents an automated backward error analysis for numerical code to empower both numerical analysts and application developers. In addition, we use the computed backward error results to also compute the condition number, an important quantity recognized by numerical analysts for measuring how sensitive a function is to changes or errors in the input. Experimental results on Intel X87 FPU functions and widely-used GNU C Library functions demonstrate that our analysis is effective at analyzing the accuracy of floating-point programs.