弯腰
发表于 2025-3-25 06:21:25
Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Progn, multiplication, GEMM (general matrix multiplication), or more generally BLAS (Basic Linear Algebra Subprograms). In order to do so, we introduce a family of abstract domains parameterized by a set of matrix predicates and by a numeric domain. We show that our analysis is robust enough to prove th
ALIEN
发表于 2025-3-25 10:53:54
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesisiables, generates constraints for . to be an invariant, and solves the generated constraints. However, this approach often suffers from an increasing template size if the degree of a template polynomial is too high..We propose a technique to make template-based methods more efficient. Our technique
严厉谴责
发表于 2025-3-25 14:24:30
http://reply.papertrans.cn/88/8763/876220/876220_23.png
outer-ear
发表于 2025-3-25 19:01:30
http://reply.papertrans.cn/88/8763/876220/876220_24.png
Ige326
发表于 2025-3-25 22:14:34
http://reply.papertrans.cn/88/8763/876220/876220_25.png
cortisol
发表于 2025-3-26 02:30:06
Automated Verification of Linearization Policiesp structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.
spinal-stenosis
发表于 2025-3-26 07:02:48
Bounded Abstract Interpretationhave implemented it for the .NET static analyzer Clousot. Our experiments show that bounded abstract interpretation can significantly increase the performance of the analysis (by up to 8x) while also increasing the quality of the reported warnings (more definite warnings that detect genuine bugs).
Adulate
发表于 2025-3-26 08:53:26
http://reply.papertrans.cn/88/8763/876220/876220_28.png
声明
发表于 2025-3-26 14:41:56
Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVMfined behavior and under-specification in the LLVM’s language reference manual. We have translated all optimizations that belong to this category into Alive-FP. In this process, we have discovered seven wrong optimizations in LLVM.
泥瓦匠
发表于 2025-3-26 18:04:46
0302-9743 16, held in Edinburgh, UK, in September 2016. ..The 21 papers presented in this volume were carefully reviewed and selected from 55 submissions. The contributions cover a variety of multi-disciplinary topics in abstract domains; abstract interpretation; abstract testing; bug detection; data flow ana