Explicit arithmetic intersection theory and computation of Néron-Tate heights

We describe a general algorithm for computing intersection pairings on arithmetic surfaces. We have implemented our algorithm for curves over Q, and we show how to use it to compute regulators for a number of Jacobians of smooth plane quartics, and to numerically verify the conjecture of Birch and Swinnerton-Dyer for the Jacobian of the split Cartan curve of level 13, up to squares.