Titlebook: Static Analysis; 25th International S Andreas Podelski Conference proceedings 2018 Springer Nature Switzerland AG 2018 static analysis.prog

举止粗野的人

Verifying Bounded Subset-Closed Hyperproperties,f hyperproperties. In particular, we focus on the verification of . which are easier to verify than generic hyperproperties. It turns out that a lot of interesting specifications (e.g., Non-Interference) lie in this category.

predict

The Impact of Program Transformations on Static Program Analysis,mechanism for recovering lost precision through the systematic construction of a new, bisimulating analysis. Furthermore, it is shown that program analyses defined over a class of composite domains can be factored into a program transformation followed by simpler, equally precise analyses of the target program.

暗讽

Exposition

Deductive Verification in Decidable Fragments with Ivy, performance is relatively predictable, stable and transparent. In particular Ivy focuses on the use of . fragments of first-order logic. We consider the rationale or Ivy’s design, the various capabilities of the tool, as well as case studies and applications.

谷类

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints,orithms from constraint-only representation of convex polyhedra, most importantly Fourier-Motzkin elimination and projection-based convex hull. We made a prototype implementation of the new domain in our abstract interpreter for Horn clauses. Our initial experiments are, in our opinion, promising and show directions for future improvement.

橡子

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra, operator for NNC polyhedra, proposing a more appropriate specification based on the semantics of the domain elements, rather than their low level representation details. Finally, we provide an experimental evaluation comparing the efficiency of the new abstract domain with respect to more classical implementations.

新鲜

Process-Local Static Analysis of Synchronous Processes,oof and a prototype implementation of the approach for a synchronous subset of the Go programming language. Overall our approach tackles the combinatorial explosion of concurrent programs by suitable static analysis approximations, thereby lifting traditional sequential analysis techniques to a concurrent setting.

事情

Omniscient

NOT