Titlebook: Static Analysis; 27th International S David Pichardie,Mihaela Sighireanu Conference proceedings 2020 Springer Nature Switzerland AG 2020 lo

IST

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

冬眠

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

切割

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

铁塔等

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

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

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

项目

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

轨道

EVADE