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 gives an algorithm for computing $X(K)$(say, their coordinates)?

I agree to assume BSD and finitness of Shafarevich-Tate group.

Tryign to transform their proof to an algorithm I met the following bottlenecks. First, we need to compute $\log \overline{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 $Jac(K)$ but I still do not know any non-conjectural algrorithms.

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 extendindg the base field where it is easy to find a base point.

Finally, we nned an arguement fo computing zeroes of $p$-adic analytic functions. There is an arguement a la Hensel lemma for computing zeroes sign-by-sign which probably terminates if we search for points over number fields, but I am not sure.