Merited
发表于 2025-3-23 13:03:29
Refinement-Based CFG Reconstruction from Unstructured Programs,ly an executable file. The problem is tackled in an original way, with a refinement-based static analysis working over finite sets of constant values. Requirement propagation allows the analysis to automatically adjust the domain precision only where it is needed, resulting in precise CFG recovery a
尖牙
发表于 2025-3-23 16:40:18
SAT-Based Model Checking without Unrolling,e inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful
减至最低
发表于 2025-3-23 19:21:13
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifi
thwart
发表于 2025-3-23 22:13:47
,Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds, strictly between 0 and 1. Many practical randomized algorithms are designed to work under non-extremal threshold probabilities and thus it is important to study power of PBAs for such cases..The paper presents a number of surprising expressiveness and decidability results for PBAs when the threshol
吗啡
发表于 2025-3-24 04:22:53
http://reply.papertrans.cn/99/9818/981731/981731_15.png
JUST
发表于 2025-3-24 06:50:22
Proving Stabilization of Biological Systems, scalability, our procedure uses modular proof techniques, where state-space exploration is applied only locally to small pieces of the system rather than the entire system as a whole. Our procedure exploits the observation that, in practice, the form of modular proofs can be restricted to a very li
Largess
发表于 2025-3-24 12:53:28
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections,y contracts, these assertions would better be given as a precondition of the method/procedure which can detect that a caller has violated the procedure’s contract in a way which definitely leads to an assertion violation (., for separate static analysis). We define precisely and formally the contrac
转向
发表于 2025-3-24 16:38:40
Strengthening Induction-Based Race Checking with Lightweight Static Analysis,ncorrectly orchestrated DMAs cause ., leading to subtle bugs that are hard to reproduce and fix. In previous work, we have shown that .-induction yields an effective method for proving absence of a restricted class of DMA races. We extend this work to handle a larger class of DMA races. We show that
摇曳
发表于 2025-3-24 21:58:29
http://reply.papertrans.cn/99/9818/981731/981731_19.png
细胞学
发表于 2025-3-25 00:50:32
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creawned processes allow to extend the basic model with joining of created processes . Orthogonally DPNs can be extended with nested locking . Reachability of a regular set . of configurations in presence of stable constraints as well as reachability without constraints but with nested locking are