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.

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.