Program analysis via efficient symbolic abstraction

This paper concerns the scalability challenges of symbolic abstraction: given a formula ϕ in a logic L and an abstract domain A , find a most precise element in the abstract domain that over-approximates the meaning of ϕ. Symbolic abstraction is an important point in the space of abstract interpretation, as it allows for automatically synthesizing the best abstract transformers. However, current techniques for symbolic abstraction can have difficulty delivering on its practical strengths, due to performance issues. In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.

Box-constrained optimization for minimax supervised learning

In this paper, we present the optimization procedure for computing the discrete boxconstrained minimax classifier introduced in [1, 2]. Our approach processes discrete or beforehand discretized features. A box-constrained region defines some bounds for each class proportion independently. The box-constrained minimax classifier is obtained from the computation of the least favorable prior which maximizes the minimum empirical risk of error over the box-constrained region. After studying the discrete empirical Bayes risk over the probabilistic simplex, we consider a projected subgradient algorithm which computes the prior maximizing this concave multivariate piecewise affine function over a polyhedral domain. The convergence of our algorithm is established.

Optimized Layout of Spherical Objects in a Polyhedral Domain

Introduction. The article studies the problem of arranging spherical objects in a bounded polyhedral domain in order to maximize the packing factor. The spherical objects have variable placement parameters and variable radii within the given upper and lower bounds. The constraints on the allowable distance between each pair of spherical objects are taken into account. The phi-function technique is used for analytical description of the placement constraints, involving object non-overlapping and containment conditions. The problem is considered as a nonlinear programming problem. The feasible region is described by a system of inequalities with differentiable functions. To find the local maximum of the problem the decomposition algorithm is used. We employ the strategy of active set of inequalities for reducing the computational complexity of the algorithm. IPOPT solver for solving nonlinear programming subproblems is used. The multistart strategy allows selecting the best local maximum point. Numerical results and the appropriate graphic illustration are given. The purpose of the article is presenting a mathematical model and developing a solution algorithm for arranging spherical objects in a polyhedral region with the maximum packing factor. It allows obtaining a locally optimal solution in a reasonable time. Results. A new formulation of the problem of arranging spherical objects in a polyhedral domain is considered, where both the placement parameters and the radii of the spherical objects are variable. A mathematical model in the form of nonlinear programming problem is derived. A solution approach based on the decomposition algorithm and multistart strategy is developed. The numerical results combined with the graphical illustration are given. Conclusions. The proposed approach allows modeling optimized layouts of spherical objects into a polyhedral domain. Keywords: layout, spherical objects, polyhedral domain, phi-function.

Penalty method with Crouzeix–Raviart approximation for the Stokes equations under slip boundary condition

The Stokes equations subject to non-homogeneous slip boundary conditions are considered in a smooth domain Ω ⊂ ℝN (N = 2,3). We propose a finite element scheme based on the nonconforming P1/P0 approximation (Crouzeix–Raviart approximation) combined with a penalty formulation and with reduced-order numerical integration in order to address the essential boundary condition u · n∂Ω = g on ∂Ω. Because the original domain Ω must be approximated by a polygonal (or polyhedral) domain Ωh before applying the finite element method, we need to take into account the errors owing to the discrepancy Ω ≠ Ωh, that is, the issues of domain perturbation. In particular, the approximation of n∂Ω by n∂Ωh makes it non-trivial whether we have a discrete counterpart of a lifting theorem, i.e., continuous right inverse of the normal trace operator H1 (Ω)N → H1/2(∂Ω); u ↦ u⋅n∂Ω. In this paper we indeed prove such a discrete lifting theorem, taking advantage of the nonconforming approximation, and consequently we establish the error estimates O(hα + ε) and O(h2α + ε) for the velocity in the H1- and L2-norms respectively, where α = 1 if N = 2 and α = 1/2 if N = 3. This improves the previous result [T. Kashiwabara et al., Numer. Math. 134 (2016) 705–740] obtained for the conforming approximation in the sense that there appears no reciprocal of the penalty parameter ϵ in the estimates.

A mixed finite-element method for elliptic operators with Wentzell boundary condition

In this paper we introduce and analyze a mixed finite-element approach for a coupled bulk-surface problem of second order with a Wentzell boundary condition. The problem is formulated on a domain with a curved smooth boundary. We introduce a mixed formulation that is equivalent to the usual weak formulation. Furthermore, optimal a priori error estimates between the exact solution and the finite-element approximation are derived. To this end, the curved domain is approximated by a polyhedral domain introducing an additional geometrical error that has to be bounded. A computational result confirms the theoretical findings.

Numerical Integration Approach Based on Radial Integration Method for General 3D Polyhedral Finite Elements

We construct an efficient quadrature method for the integration of the Galerkin weak form over general 3D polyhedral elements based on the radial integration method (RIM). The basic idea of the proposed method is to convert the polyhedral domain integrals to contour plane integrals of the element by utilizing the RIM which can be used for accurate evaluation of various complicated domain integrals. The quadrature construction scheme for irregular polyhedral elements involves the treatment of the nonpolynomial shape functions as well as the arbitrary geometry shape of the elements. In this approach, the volume integrals for polyhedral elements with triangular or quadrilateral faces are evaluated by transforming them into face integrals using RIM. For those polyhedral elements with irregular polygons, RIM is again used to convert the face integrals into line integrals. As a result, the volume integration of Galerkin weak form over the polyhedral elements can be easily carried out by a number of line integrals along the edges of the polyhedron. Some benchmark numerical examples including the patch tests are utilized to demonstrate the accuracy and convenience of the proposed method.