IST
发表于 2025-3-26 21:14:19
Stratified Guarded First-Order Transition Systemsneral, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, strati
冬眠
发表于 2025-3-27 04:01:19
Predicate Abstraction and CEGAR for , Validity Checking of it to the fragment without the least fixpoint operator. The validity checking problem for . has recently been shown to provide a uniform approach to higher-order program verification. The restriction to . studied in this paper already provides an automated method for a large class of program ver
arabesque
发表于 2025-3-27 08:04:32
http://reply.papertrans.cn/88/8762/876199/876199_33.png
切割
发表于 2025-3-27 09:49:07
Formal Framework for Reasoning About the Precision of Dynamic Analysisnces of the more general problem of analysing programs by dynamically executing their code with selected inputs. While static program analysis has a beautiful and well established theoretical foundation in abstract interpretation, dynamic analysis still lacks such a foundation. In this paper, we int
铁塔等
发表于 2025-3-27 16:45:50
Simple and Efficient Computation of Minimal Weak Control Closureelming number of definitions of control dependency relations are found in the literature that capture various kinds of program control flow structures. Weak and strong control closure (WCC and SCC) relations capture nontermination insensitive and sensitive control dependencies and subsume all previo
Parallel
发表于 2025-3-27 17:49:49
A Library Modeling Language for the Static Analysis of C Programsnspiration from Behavioral Interface Specification Languages popular in deductive verification, notably Frama-C’s ACSL, as we annotate function prototypes with pre and post-conditions expressed concisely in a first-order logic, but with key differences. Firstly, the specification aims at replacing a
Contend
发表于 2025-3-27 23:29:35
Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summariesthe set of reachable states. By contrast, abstractions for transformation relations between input states and output states not only provide a finer description of program executions but also enable the composition of the effect of program fragments so as to make the analysis modular. However, few lo
项目
发表于 2025-3-28 02:18:36
Probabilistic Lipschitz Analysis of Neural Networksterested in probabilistic notions of robustness that assume it feasible to construct a statistical model of the process generating the inputs of a neural network. We find this a reasonable assumption given the rapid advances in algorithms for learning generative models of data. A neural network . is
轨道
发表于 2025-3-28 06:30:52
http://reply.papertrans.cn/88/8762/876199/876199_39.png
EVADE
发表于 2025-3-28 13:11:02
http://reply.papertrans.cn/88/8762/876199/876199_40.png