Does Chabauty-Coleman method give an algorithm for finding rational points? Let $X$ be a curve of genus $g\geq 2$ over a number field $K$. If $\mathrm{rk} \,\mathrm{Jac}\, X$ is less than $g$ there is a $p$-adic method of bounding $\# X(K)$ due to Chabauty and Coleman (see http://www-math.mit.edu/~poonen/papers/chabauty.pdf).

Does this method give an algorithm for computing $X(K)$ (say, their coordinates)? 

I agree to assume BSD and finitness of Shafarevich-Tate group.
Trying to transform their proof to an algorithm, I met the following bottlenecks. First, we need to compute $\log \overline{\mathrm{Jac}(K)}$ (bar means $p$-adic closure) in order to obtain a $1$-form whose integral will vanish on rational points, which is weaker than computing $\mathrm{Jac}(K)$ but I still do not know any non-conjectural algorithms.
Next, the proof requires choosing base points in each residue class and I do not know how to find them algorithmically. Maybe, a solution can be obtained by extending the base field to where it is easy to find a base point.
Finally, we need an argument for computing zeroes of $p$-adic analytic functions. There is an argument, à la Hensel's lemma, for computing zeroes sign-by-sign, which probably terminates if we search for points over number fields, but I am not sure.
 A: Conjecturally, yes. Check out Section 4.4 of this paper by Nils Bruin and myself.
The point is to combine Chabauty-Coleman with the "Mordell-Weil Sieve". 
In the following, I will assume for simplicity that the Jacobian of your 
curve $X$ is simple and that $K = \mathbb Q$. I will also assume that
one rational point $P_0$ on $X$ is known, which we use to embed
$X$ into $J = \operatorname{Jac} X$.
In any case, assuming finiteness of Sha (say), one can in principle determine the rank $r$ of $J(\mathbb Q)$ and find $r$ independent points. Given this information and a prime $p$ of good reduction, one can determine the space of regular 1-forms $\omega$ over ${\mathbb Q}_p$ on $X$ that kill $J(\mathbb Q)$
under the Chabauty-Coleman pairing to any desired $p$-adic precision.
In particular, one can compute the image of this space in the 1-forms
mod $p$. If $p > 2$ and there is such a 1-form mod $p$ that does not
vanish at any ${\mathbb F}_p$-point of $X$ (which heuristically happens
for a set of primes $p$ of positive density), then one can show
that each residue class mod $p$ can contain
at most one rational point. So we now just have to decide, for each
residue class, whether there is a rational point or not.
If there is a point, then we will eventually find it by searching for it.
If there is no point, then (again heuristically) we should be able
to prove this using the Mordell-Weil Sieve as explained in the paper.
Basically, one tries to use information obtained from reduction modulo
a bunch of further primes $q$, together with the knowledge of a
finite-index subgroup of $J(\mathbb Q)$, to get a contradiction.
So when $X$ and $J$ satisfy


*

*finiteness of Sha (or BSD)

*there exist $p$ of good reduction and a "good" differential
on $X$ mod $p$ that does not vanish in $X(\mathbb F_p)$

*the "main" conjecture of this paper
then the procedure outlined above will terminate and determine $X(\mathbb Q)$. Also, if the procedure terminates, then it will produce the
correct result. So for practical purposes, we can just use it and
hope that it finishes. I have implemented it for curves of genus 2
(with Jacobian of rank 1) over $\mathbb Q$ in Magma. It works very
well in practice, even though there is no proof so far that it will
always work.
