@article{1832, abstract = {Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. }, author = {Chakraborty, Soham and Henzinger, Thomas A and Sezgin, Ali and Vafeiadis, Viktor}, journal = {Logical Methods in Computer Science}, number = {1}, publisher = {International Federation of Computational Logic}, title = {{Aspect-oriented linearizability proofs}}, doi = {10.2168/LMCS-11(1:20)2015}, volume = {11}, year = {2015}, } @article{2271, abstract = {A class of valued constraint satisfaction problems (VCSPs) is characterised by a valued constraint language, a fixed set of cost functions on a finite domain. Finite-valued constraint languages contain functions that take on rational costs and general-valued constraint languages contain functions that take on rational or infinite costs. An instance of the problem is specified by a sum of functions from the language with the goal to minimise the sum. This framework includes and generalises well-studied constraint satisfaction problems (CSPs) and maximum constraint satisfaction problems (Max-CSPs). Our main result is a precise algebraic characterisation of valued constraint languages whose instances can be solved exactly by the basic linear programming relaxation (BLP). For a general-valued constraint language Γ, BLP is a decision procedure for Γ if and only if Γ admits a symmetric fractional polymorphism of every arity. For a finite-valued constraint language Γ, BLP is a decision procedure if and only if Γ admits a symmetric fractional polymorphism of some arity, or equivalently, if Γ admits a symmetric fractional polymorphism of arity 2. Using these results, we obtain tractability of several novel and previously widely-open classes of VCSPs, including problems over valued constraint languages that are: (1) submodular on arbitrary lattices; (2) bisubmodular (also known as k-submodular) on arbitrary finite domains; (3) weakly (and hence strongly) tree-submodular on arbitrary trees. }, author = {Kolmogorov, Vladimir and Thapper, Johan and Živný, Stanislav}, journal = {SIAM Journal on Computing}, number = {1}, pages = {1 -- 36}, publisher = {SIAM}, title = {{The power of linear programming for general-valued CSPs}}, doi = {10.1137/130945648}, volume = {44}, year = {2015}, } @article{257, abstract = {For suitable pairs of diagonal quadratic forms in eight variables we use the circle method to investigate the density of simultaneous integer solutions and relate this to the problem of estimating linear correlations among sums of two squares.}, author = {Timothy Browning and Munshi, Ritabrata}, journal = {Forum Mathematicum}, number = {4}, pages = {2025 -- 2050}, publisher = {Walter de Gruyter GmbH}, title = {{Pairs of diagonal quadratic forms and linear correlations among sums of two squares}}, doi = {10.1515/forum-2013-6024}, volume = {27}, year = {2015}, } @inbook{258, abstract = {Given a number field k and a projective algebraic variety X defined over k, the question of whether X contains a k-rational point is both very natural and very difficult. In the event that the set X(k) of k-rational points is not empty, one can also ask how the points of X(k) are distributed. Are they dense in X under the Zariski topology? Are they dense in the set.}, author = {Browning, Timothy D}, booktitle = {Arithmetic and Geometry}, pages = {89 -- 113}, publisher = {Cambridge University Press}, title = {{A survey of applications of the circle method to rational points}}, doi = {10.1017/CBO9781316106877.009}, year = {2015}, } @article{259, abstract = {The Hasse principle and weak approximation is established for non-singular cubic hypersurfaces X over the function field }, author = {Timothy Browning and Vishe, Pankaj}, journal = {Geometric and Functional Analysis}, number = {3}, pages = {671 -- 732}, publisher = {Birkhäuser}, title = {{Rational points on cubic hypersurfaces over F_q(t) }}, doi = {10.1007/s00039-015-0328-5}, volume = {25}, year = {2015}, }