diff --git a/doc/org/concepts.org b/doc/org/concepts.org
index 24156ddfd..ab59d75ce 100644
--- a/doc/org/concepts.org
+++ b/doc/org/concepts.org
@@ -54,7 +54,7 @@ Andersen's lecture notes]].
In Spot, BDDs are one way to represent Boolean formulas, and in
particular, they are used to labels the edges of [[#buchi][automata]]. Spot uses a
-customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]] for manipulating BDDs.
+customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]] for manipulating BDDs.
* ω-word
:PROPERTIES:
diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org
index 693a2650c..c0c3a9600 100644
--- a/doc/org/ltlcross.org
+++ b/doc/org/ltlcross.org
@@ -101,7 +101,7 @@ No problem detected.
=ltlcross= can only read four kinds of output:
- Never claims (only if they are restricted to representing an
automaton using =if=, =goto=, and =skip= statements) such as those
- output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. The
+ output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. The
newer syntax introduced by Spin 6.24, using =do= instead of =if=,
is also supported.
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with
diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org
index c83ad891b..1b5d4b481 100644
--- a/doc/org/ltldo.org
+++ b/doc/org/ltldo.org
@@ -19,7 +19,7 @@ any other tool.
* Example: computing statistics for =ltl3ba=
As a motivating example, consider a scenario where we want to run
-[[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula
+[[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula
we would like to compute compute the number of states and edges in the
Büchi automaton produced by =ltl3ba=.
diff --git a/python/ajax/trans.html b/python/ajax/trans.html
index 924719d20..74e2bb038 100644
--- a/python/ajax/trans.html
+++ b/python/ajax/trans.html
@@ -616,7 +616,7 @@ an identifier: aUb is an atomic proposition, unlike