diff --git a/bin/common_output.cc b/bin/common_output.cc
index 81eff78aa..9cee42349 100644
--- a/bin/common_output.cc
+++ b/bin/common_output.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -165,7 +165,7 @@ namespace
     }
 
     virtual void
-    print(std::ostream& os, const char*) const
+    print(std::ostream& os, const char*) const override
     {
       stream_escapable_formula(os, val_->f, val_->filename, val_->line);
     }
diff --git a/spot/kripke/fairkripke.hh b/spot/kripke/fairkripke.hh
index 090709214..e55fa2425 100644
--- a/spot/kripke/fairkripke.hh
+++ b/spot/kripke/fairkripke.hh
@@ -54,8 +54,8 @@ namespace spot
     fair_kripke_succ_iterator(const bdd& cond, acc_cond::mark_t acc_cond);
     virtual ~fair_kripke_succ_iterator();
 
-    virtual bdd cond() const;
-    virtual acc_cond::mark_t acc() const;
+    virtual bdd cond() const override;
+    virtual acc_cond::mark_t acc() const override;
   protected:
     bdd cond_;
     acc_cond::mark_t acc_cond_;
diff --git a/spot/kripke/kripke.hh b/spot/kripke/kripke.hh
index 163e694b8..5c710da5c 100644
--- a/spot/kripke/kripke.hh
+++ b/spot/kripke/kripke.hh
@@ -59,8 +59,8 @@ namespace spot
 
     virtual ~kripke_succ_iterator();
 
-    virtual bdd cond() const;
-    virtual acc_cond::mark_t acc() const;
+    virtual bdd cond() const override;
+    virtual acc_cond::mark_t acc() const override;
   protected:
     bdd cond_;
   };
diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh
index b97bfd01f..81fe5273a 100644
--- a/spot/kripke/kripkegraph.hh
+++ b/spot/kripke/kripkegraph.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE)
+// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -39,7 +39,7 @@ namespace spot
     {
     }
 
-    virtual int compare(const spot::state* other) const
+    virtual int compare(const spot::state* other) const override
     {
       auto o = down_cast<const kripke_graph_state*>(other);
       assert(o);
@@ -52,19 +52,19 @@ namespace spot
       return 0;
     }
 
-    virtual size_t hash() const
+    virtual size_t hash() const override
     {
       return
 	reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
     }
 
     virtual kripke_graph_state*
-    clone() const
+    clone() const override
     {
       return const_cast<kripke_graph_state*>(this);
     }
 
-    virtual void destroy() const
+    virtual void destroy() const override
     {
     }
 
@@ -104,30 +104,30 @@ namespace spot
     {
     }
 
-    virtual void recycle(const typename Graph::state_storage_t* s)
+    void recycle(const typename Graph::state_storage_t* s)
     {
       cond_ = s->cond();
       t_ = s->succ;
     }
 
-    virtual bool first()
+    virtual bool first() override
     {
       p_ = t_;
       return p_;
     }
 
-    virtual bool next()
+    virtual bool next() override
     {
       p_ = g_->edge_storage(p_).next_succ;
       return p_;
     }
 
-    virtual bool done() const
+    virtual bool done() const override
     {
       return !p_;
     }
 
-    virtual kripke_graph_state* dst() const
+    virtual kripke_graph_state* dst() const override
     {
       assert(!done());
       return const_cast<kripke_graph_state*>
@@ -138,7 +138,7 @@ namespace spot
 
   /// \class kripke_graph
   /// \brief Kripke Structure.
-  class SPOT_API kripke_graph : public kripke
+  class SPOT_API kripke_graph final : public kripke
   {
   public:
     typedef digraph<kripke_graph_state, void> graph_t;
@@ -180,7 +180,7 @@ namespace spot
       return init_number_;
     }
 
-    virtual const kripke_graph_state* get_init_state() const
+    virtual const kripke_graph_state* get_init_state() const override
     {
       if (num_states() == 0)
 	const_cast<graph_t&>(g_).new_state();
@@ -190,7 +190,7 @@ namespace spot
     /// \brief Allow to get an iterator on the state we passed in
     /// parameter.
     virtual kripke_graph_succ_iterator<graph_t>*
-    succ_iter(const spot::state* st) const
+    succ_iter(const spot::state* st) const override
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
       assert(s);
@@ -235,13 +235,13 @@ namespace spot
       return ss.str();
     }
 
-    virtual std::string format_state(const state* st) const
+    virtual std::string format_state(const state* st) const override
     {
       return format_state(state_number(st));
     }
 
     /// \brief Get the condition on the state
-    virtual bdd state_condition(const state* s) const
+    virtual bdd state_condition(const state* s) const override
     {
       return down_cast<const kripke_graph_state*>(s)->cond();
     }
diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc
index 1b1a4b4e9..b84f5b980 100644
--- a/spot/ltsmin/ltsmin.cc
+++ b/spot/ltsmin/ltsmin.cc
@@ -258,7 +258,7 @@ namespace spot
     ////////////////////////////////////////////////////////////////////////
     // SUCC_ITERATOR
 
-    class spins_succ_iterator: public kripke_succ_iterator
+    class spins_succ_iterator final: public kripke_succ_iterator
     {
     public:
 
@@ -280,28 +280,24 @@ namespace spot
 	delete cc_;
       }
 
-      virtual
-      bool first()
+      virtual bool first() override
       {
 	it_ = cc_->transitions.begin();
 	return it_ != cc_->transitions.end();
       }
 
-      virtual
-      bool next()
+      virtual bool next() override
       {
 	++it_;
 	return it_ != cc_->transitions.end();
       }
 
-      virtual
-      bool done() const
+      virtual bool done() const override
       {
 	return it_ == cc_->transitions.end();
       }
 
-      virtual
-      state* dst() const
+      virtual state* dst() const override
       {
 	return (*it_)->clone();
       }
@@ -605,7 +601,7 @@ namespace spot
     ////////////////////////////////////////////////////////////////////////
     // KRIPKE
 
-    class spins_kripke: public kripke
+    class spins_kripke final: public kripke
     {
     public:
 
@@ -615,7 +611,7 @@ namespace spot
 	: kripke(dict),
 	  d_(d),
 	  state_size_(d_->get_state_size()),
-	  dict_(dict), ps_(ps),
+	  ps_(ps),
 	  compress_(compress == 0 ? nullptr
 		    : compress == 1 ? int_array_array_compress
 		    : int_array_array_compress2),
@@ -696,8 +692,7 @@ namespace spot
 	delete state_condition_last_cc_; // Might be 0 already.
       }
 
-      virtual
-      state* get_init_state() const
+      virtual state* get_init_state() const override
       {
 	if (compress_)
 	  {
@@ -848,8 +843,7 @@ namespace spot
 
 
       virtual
-      spins_succ_iterator*
-      succ_iter(const state* st) const
+      spins_succ_iterator* succ_iter(const state* st) const override
       {
 	// This may also compute successors in state_condition_last_cc
 	bdd scond = compute_state_condition(st);
@@ -882,14 +876,13 @@ namespace spot
       }
 
       virtual
-      bdd
-      state_condition(const state* st) const
+      bdd state_condition(const state* st) const override
       {
 	return compute_state_condition(st);
       }
 
       virtual
-      std::string format_state(const state *st) const
+      std::string format_state(const state *st) const override
       {
 	const int* vars = get_vars(st);
 
@@ -917,16 +910,9 @@ namespace spot
 	return res.str();
       }
 
-      virtual
-      spot::bdd_dict_ptr get_dict() const
-      {
-	return dict_;
-      }
-
     private:
       spins_interface_ptr d_;
       int state_size_;
-      bdd_dict_ptr dict_;
       const char** vname_;
       bool* format_filter_;
       const spot::prop_set* ps_;
diff --git a/spot/misc/formater.hh b/spot/misc/formater.hh
index 0dc04f54a..8ce11dccb 100644
--- a/spot/misc/formater.hh
+++ b/spot/misc/formater.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2016 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -72,7 +72,7 @@ namespace spot
     }
 
     virtual void
-    print(std::ostream& os, const char*) const
+    print(std::ostream& os, const char*) const override
     {
       os << val_;
     }
@@ -83,7 +83,7 @@ namespace spot
   {
   public:
     virtual void
-    print(std::ostream& os, const char* x) const
+    print(std::ostream& os, const char* x) const override
     {
       os << '%' << *x;
     }
@@ -94,7 +94,7 @@ namespace spot
   {
   public:
     virtual void
-    print(std::ostream& os, const char*) const
+    print(std::ostream& os, const char*) const override
     {
       os << '%';
     }
diff --git a/spot/priv/bddalloc.hh b/spot/priv/bddalloc.hh
index 1716e0762..990ed3fa2 100644
--- a/spot/priv/bddalloc.hh
+++ b/spot/priv/bddalloc.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2016 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -49,6 +49,6 @@ namespace spot
   private:
     /// Require more variables.
     void extvarnum(int more);
-    virtual int extend(int n);
+    virtual int extend(int n) override;
   };
 }
diff --git a/spot/ta/ta.hh b/spot/ta/ta.hh
index a7d503c8a..5a4916bcd 100644
--- a/spot/ta/ta.hh
+++ b/spot/ta/ta.hh
@@ -201,20 +201,10 @@ namespace spot
     ~ta_succ_iterator()
     {
     }
-
-    virtual bool first() = 0;
-    virtual bool next() = 0;
-    virtual bool done() const = 0;
-
-    virtual const state* dst() const = 0;
-
     /// \brief Get the changeset on the transition leading to current successor.
     ///
     /// This is a boolean function of atomic propositions.
     virtual bdd cond() const = 0;
-
-    acc_cond::mark_t acc() const = 0;
-
   };
 
 #ifndef SWIG
diff --git a/spot/ta/taexplicit.hh b/spot/ta/taexplicit.hh
index 532ce81f4..a2f836c30 100644
--- a/spot/ta/taexplicit.hh
+++ b/spot/ta/taexplicit.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -64,38 +64,35 @@ namespace spot
     // ta interface
     virtual
     ~ta_explicit();
-    virtual const_states_set_t
-    get_initial_states_set() const;
+    virtual const_states_set_t get_initial_states_set() const override;
+
+    virtual ta_succ_iterator* succ_iter(const spot::state* s) const override;
 
     virtual ta_succ_iterator*
-    succ_iter(const spot::state* s) const;
+    succ_iter(const spot::state* s, bdd condition) const override;
 
-    virtual ta_succ_iterator*
-    succ_iter(const spot::state* s, bdd condition) const;
-
-    virtual bdd_dict_ptr
-    get_dict() const;
+    bdd_dict_ptr get_dict() const;
 
     virtual std::string
-    format_state(const spot::state* s) const;
+    format_state(const spot::state* s) const override;
 
     virtual bool
-    is_accepting_state(const spot::state* s) const;
+    is_accepting_state(const spot::state* s) const override;
 
     virtual bool
-    is_livelock_accepting_state(const spot::state* s) const;
+    is_livelock_accepting_state(const spot::state* s) const override;
 
     virtual bool
-    is_initial_state(const spot::state* s) const;
+    is_initial_state(const spot::state* s) const override;
 
     virtual bdd
-    get_state_condition(const spot::state* s) const;
+    get_state_condition(const spot::state* s) const override;
 
     virtual void
-    free_state(const spot::state* s) const;
+    free_state(const spot::state* s) const override;
 
-    spot::state*
-    get_artificial_initial_state() const
+    virtual spot::state*
+    get_artificial_initial_state() const override
     {
       return (spot::state*) artificial_initial_state_;
     }
@@ -107,7 +104,7 @@ namespace spot
 
     }
 
-    virtual void
+    void
     delete_stuttering_and_hole_successors(const spot::state* s);
 
     ta::states_set_t
@@ -129,7 +126,7 @@ namespace spot
 
   /// states used by spot::ta_explicit.
   /// \ingroup ta_representation
-  class SPOT_API state_ta_explicit : public spot::state
+  class SPOT_API state_ta_explicit final: public spot::state
   {
 #ifndef SWIG
   public:
@@ -156,15 +153,11 @@ namespace spot
     {
     }
 
-    virtual int
-    compare(const spot::state* other) const;
-    virtual size_t
-    hash() const;
-    virtual state_ta_explicit*
-    clone() const;
+    virtual int compare(const spot::state* other) const override;
+    virtual size_t hash() const override;
+    virtual state_ta_explicit* clone() const override;
 
-    virtual void
-    destroy() const
+    virtual void destroy() const override
     {
     }
 
@@ -227,21 +220,21 @@ namespace spot
   };
 
   /// Successor iterators used by spot::ta_explicit.
-  class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator
+  class SPOT_API ta_explicit_succ_iterator final: public ta_succ_iterator
   {
   public:
     ta_explicit_succ_iterator(const state_ta_explicit* s);
 
     ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);
 
-    virtual bool first();
-    virtual bool next();
-    virtual bool done() const;
+    virtual bool first() override;
+    virtual bool next() override;
+    virtual bool done() const override;
 
-    virtual const state* dst() const;
-    virtual bdd cond() const;
+    virtual const state* dst() const override;
+    virtual bdd cond() const override;
 
-    virtual acc_cond::mark_t acc() const;
+    virtual acc_cond::mark_t acc() const override;
 
   private:
     state_ta_explicit::transitions* transitions_;
diff --git a/spot/ta/taproduct.hh b/spot/ta/taproduct.hh
index 8c4d23bb7..a52eabcb0 100644
--- a/spot/ta/taproduct.hh
+++ b/spot/ta/taproduct.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -60,11 +60,11 @@ namespace spot
     }
 
     virtual int
-    compare(const state* other) const;
+    compare(const state* other) const override;
     virtual size_t
-    hash() const;
+    hash() const override;
     virtual state_ta_product*
-    clone() const;
+    clone() const override;
 
   private:
     const state* ta_state_; ///< State from the ta automaton.
@@ -82,22 +82,17 @@ namespace spot
     ~ta_succ_iterator_product();
 
     // iteration
-    bool first();
-    bool next();
-    bool done() const;
+    virtual bool first() override;
+    virtual bool next() override;
+    virtual bool done() const override;
 
     // inspection
-    state_ta_product*
-    dst() const;
-    bdd
-    cond() const;
-
-    acc_cond::mark_t
-    acc() const;
+    virtual state_ta_product* dst() const override;
+    virtual bdd cond() const override;
+    virtual acc_cond::mark_t acc() const override;
 
     /// \brief Return true if the changeset of the current transition is empty
-    bool
-    is_stuttering_transition() const;
+    bool is_stuttering_transition() const;
 
   protected:
     //@{
@@ -129,7 +124,7 @@ namespace spot
   /// \ingroup ta_emptiness_check
   /// \brief A lazy product between a Testing automaton and a Kripke structure.
   /// (States are computed on the fly.)
-  class SPOT_API ta_product: public ta
+  class SPOT_API ta_product final: public ta
   {
   public:
     /// \brief Constructor.
@@ -142,39 +137,39 @@ namespace spot
     ~ta_product();
 
     virtual ta::const_states_set_t
-    get_initial_states_set() const;
+    get_initial_states_set() const override;
 
     virtual ta_succ_iterator_product*
-    succ_iter(const spot::state* s) const;
+    succ_iter(const spot::state* s) const override;
 
     virtual ta_succ_iterator_product*
-    succ_iter(const spot::state* s, bdd changeset) const;
+    succ_iter(const spot::state* s, bdd changeset) const override;
 
-    virtual bdd_dict_ptr
+    bdd_dict_ptr
     get_dict() const;
 
     virtual std::string
-    format_state(const spot::state* s) const;
+    format_state(const spot::state* s) const override;
 
     virtual bool
-    is_accepting_state(const spot::state* s) const;
+    is_accepting_state(const spot::state* s) const override;
 
     virtual bool
-    is_livelock_accepting_state(const spot::state* s) const;
+    is_livelock_accepting_state(const spot::state* s) const override;
 
     virtual bool
-    is_initial_state(const spot::state* s) const;
+    is_initial_state(const spot::state* s) const override;
 
     /// \brief Return true if the state \a s has no succeseurs
     /// in the TA automaton (the TA component of the product automaton)
-    virtual bool
+    bool
     is_hole_state_in_ta_component(const spot::state* s) const;
 
     virtual bdd
-    get_state_condition(const spot::state* s) const;
+    get_state_condition(const spot::state* s) const override;
 
     virtual void
-    free_state(const spot::state* s) const;
+    free_state(const spot::state* s) const override;
 
     const const_ta_ptr&
     get_ta() const
diff --git a/spot/ta/tgta.hh b/spot/ta/tgta.hh
index cae65a6cd..b997eeb3b 100644
--- a/spot/ta/tgta.hh
+++ b/spot/ta/tgta.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -79,7 +79,7 @@ namespace spot
     /// longer needed.
     ///
     virtual twa_succ_iterator*
-    succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0;
+    succ_iter_by_changeset(const spot::state* s, bdd change_set) const = 0;
   };
 
   typedef std::shared_ptr<tgta> tgta_ptr;
diff --git a/spot/ta/tgtaexplicit.cc b/spot/ta/tgtaexplicit.cc
index 32861d1a2..03a41a05d 100644
--- a/spot/ta/tgtaexplicit.cc
+++ b/spot/ta/tgtaexplicit.cc
@@ -44,12 +44,6 @@ namespace spot
     return ta_->succ_iter(state);
   }
 
-  bdd_dict_ptr
-  tgta_explicit::get_dict() const
-  {
-    return ta_->get_dict();
-  }
-
   std::string
   tgta_explicit::format_state(const spot::state* s) const
   {
diff --git a/spot/ta/tgtaexplicit.hh b/spot/ta/tgtaexplicit.hh
index 52a285dfc..574fa3490 100644
--- a/spot/ta/tgtaexplicit.hh
+++ b/spot/ta/tgtaexplicit.hh
@@ -34,7 +34,7 @@ namespace spot
 
   /// Explicit representation of a spot::tgta.
   /// \ingroup ta_representation
-  class SPOT_API tgta_explicit : public tgta
+  class SPOT_API tgta_explicit final : public tgta
   {
   public:
     tgta_explicit(const const_twa_ptr& tgba,
@@ -42,21 +42,18 @@ namespace spot
 		  state_ta_explicit* artificial_initial_state);
 
     // tgba interface
-    virtual spot::state* get_init_state() const;
+    virtual spot::state* get_init_state() const override;
 
     virtual twa_succ_iterator*
-    succ_iter(const spot::state* local_state) const;
-
-    virtual bdd_dict_ptr
-    get_dict() const;
+    succ_iter(const spot::state* local_state) const override;
 
     const_ta_explicit_ptr get_ta() const { return ta_; }
     ta_explicit_ptr get_ta() { return ta_; }
 
-    virtual std::string format_state(const spot::state* s) const;
+    virtual std::string format_state(const spot::state* s) const override;
 
     virtual twa_succ_iterator*
-    succ_iter_by_changeset(const spot::state* s, bdd change_set) const;
+    succ_iter_by_changeset(const spot::state* s, bdd change_set) const override;
   protected:
     ta_explicit_ptr ta_;
   };
diff --git a/spot/ta/tgtaproduct.hh b/spot/ta/tgtaproduct.hh
index 399308e4a..36ca271cb 100644
--- a/spot/ta/tgtaproduct.hh
+++ b/spot/ta/tgtaproduct.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -35,10 +35,10 @@ namespace spot
     tgta_product(const const_kripke_ptr& left,
 		 const const_tgta_ptr& right);
 
-    virtual const state* get_init_state() const;
+    virtual const state* get_init_state() const override;
 
     virtual twa_succ_iterator*
-    succ_iter(const state* local_state) const;
+    succ_iter(const state* local_state) const override;
   };
 
   inline twa_ptr product(const const_kripke_ptr& left,
@@ -48,7 +48,7 @@ namespace spot
   }
 
   /// \brief Iterate over the successors of a product computed on the fly.
-  class SPOT_API tgta_succ_iterator_product : public twa_succ_iterator
+  class SPOT_API tgta_succ_iterator_product final : public twa_succ_iterator
   {
   public:
     tgta_succ_iterator_product(const state_product* s,
diff --git a/spot/taalgos/emptinessta.hh b/spot/taalgos/emptinessta.hh
index a6c334567..32c219141 100644
--- a/spot/taalgos/emptinessta.hh
+++ b/spot/taalgos/emptinessta.hh
@@ -109,7 +109,7 @@ namespace spot
     /// \param disable_heuristic_for_livelock_detection disable the heuristic
     /// used in the first pass to detect livelock-accepting runs,
     /// this heuristic is described in the paper cited above
-    virtual bool
+    bool
     check(bool disable_second_pass = false,
 	  bool disable_heuristic_for_livelock_detection = false);
 
@@ -117,11 +117,11 @@ namespace spot
     /// a livelock-accepting run
     /// Return false if the product automaton accepts no livelock-accepting run,
     /// otherwise true
-    virtual bool
+    bool
     livelock_detection(const const_ta_product_ptr& t);
 
     /// Print statistics, if any.
-    virtual std::ostream&
+    std::ostream&
     print_stats(std::ostream& os) const;
 
   protected:
diff --git a/spot/tl/declenv.hh b/spot/tl/declenv.hh
index b1123fcdb..863391aa2 100644
--- a/spot/tl/declenv.hh
+++ b/spot/tl/declenv.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2013, 2014, 2015 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -44,10 +44,10 @@ namespace spot
     /// proposition was already declared.
     bool declare(const std::string& prop_str);
 
-    virtual formula require(const std::string& prop_str);
+    virtual formula require(const std::string& prop_str) override;
 
     /// Get the name of the environment.
-    virtual const std::string& name() const;
+    virtual const std::string& name() const override;
 
     typedef std::map<const std::string, formula> prop_map;
 
diff --git a/spot/tl/defaultenv.hh b/spot/tl/defaultenv.hh
index 53f120d90..6bd4468cb 100644
--- a/spot/tl/defaultenv.hh
+++ b/spot/tl/defaultenv.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -38,8 +38,8 @@ namespace spot
   {
   public:
     virtual ~default_environment();
-    virtual formula require(const std::string& prop_str);
-    virtual const std::string& name() const;
+    virtual formula require(const std::string& prop_str) override;
+    virtual const std::string& name() const override;
 
     /// Get the sole instance of spot::default_environment.
     static default_environment& instance();
diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh
index 537c30412..7c310cd39 100644
--- a/spot/tl/randomltl.hh
+++ b/spot/tl/randomltl.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -167,7 +167,7 @@ namespace spot
   /// constant and all Boolean operators supported by Spot.
   ///
   /// By default each operator has equal chance to be selected.
-  class SPOT_API random_boolean: public random_formula
+  class SPOT_API random_boolean final: public random_formula
   {
   public:
     /// Create a random Boolean formula generator using atomic
@@ -207,7 +207,7 @@ namespace spot
   /// constant and all SERE operators supported by Spot.
   ///
   /// By default each operator has equal chance to be selected.
-  class SPOT_API random_sere: public random_formula
+  class SPOT_API random_sere final: public random_formula
   {
   public:
     /// Create a random SERE genere using atomic propositions from \a ap.
diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc
index 0ace49d63..538ba895e 100644
--- a/spot/tl/relabel.cc
+++ b/spot/tl/relabel.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -47,7 +47,7 @@ namespace spot
 	{
 	}
 
-      formula next()
+      virtual formula next() override
       {
 	std::ostringstream s;
 	s << 'p' << nn++;
@@ -65,7 +65,7 @@ namespace spot
 
       unsigned nn;
 
-      formula next()
+      virtual formula next() override
       {
 	std::string s;
 	unsigned n = nn++;
diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc
index f5c0b121a..67969d790 100644
--- a/spot/twa/bdddict.cc
+++ b/spot/twa/bdddict.cc
@@ -55,7 +55,7 @@ namespace spot
       }
 
       virtual int
-      extend(int n)
+      extend(int n) override
       {
 	assert(priv_);
 	int b = priv_->allocate_variables(n);
diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh
index 949b36e40..6d8c1dab0 100644
--- a/spot/twa/taatgba.hh
+++ b/spot/twa/taatgba.hh
@@ -53,9 +53,9 @@ namespace spot
 
     /// TGBA interface.
     virtual ~taa_tgba();
-    virtual spot::state* get_init_state() const final;
-    virtual twa_succ_iterator* succ_iter(const spot::state* state) const final;
-    virtual std::string format_state(const spot::state* state) const = 0;
+    virtual spot::state* get_init_state() const override final;
+    virtual twa_succ_iterator* succ_iter(const spot::state* state)
+      const override final;
 
   protected:
 
@@ -81,9 +81,9 @@ namespace spot
     {
     }
 
-    virtual int compare(const spot::state*) const;
-    virtual size_t hash() const;
-    virtual set_state* clone() const;
+    virtual int compare(const spot::state*) const override;
+    virtual size_t hash() const override;
+    virtual set_state* clone() const override;
 
     virtual ~set_state()
     {
@@ -103,13 +103,13 @@ namespace spot
     taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);
     virtual ~taa_succ_iterator();
 
-    virtual bool first();
-    virtual bool next();
-    virtual bool done() const;
+    virtual bool first() override;
+    virtual bool next() override;
+    virtual bool done() const override;
 
-    virtual set_state* dst() const;
-    virtual bdd cond() const;
-    virtual acc_cond::mark_t acc() const;
+    virtual set_state* dst() const override;
+    virtual bdd cond() const override;
+    virtual acc_cond::mark_t acc() const override;
 
   private:
     /// Those typedefs are used to generate all possible successors in
@@ -206,7 +206,7 @@ namespace spot
     /// Otherwise a string composed of each string corresponding to
     /// each state->get_state() in the spot::set_state is returned,
     /// e.g. like {string_1,...,string_n}.
-    virtual std::string format_state(const spot::state* s) const
+    virtual std::string format_state(const spot::state* s) const override
     {
       const spot::set_state* se = down_cast<const spot::set_state*>(s);
       assert(se);
@@ -311,7 +311,8 @@ namespace spot
     ~taa_tgba_string()
       {}
   protected:
-    virtual std::string label_to_string(const std::string& label) const;
+    virtual std::string label_to_string(const std::string& label)
+      const override;
   };
 
   typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
@@ -335,7 +336,8 @@ namespace spot
     ~taa_tgba_formula()
       {}
   protected:
-    virtual std::string label_to_string(const label_t& label) const;
+    virtual std::string label_to_string(const label_t& label)
+      const override;
   };
 
   typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index 21e139763..9842aee1d 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -42,7 +42,7 @@ namespace spot
     {
     }
 
-    virtual int compare(const spot::state* other) const
+    virtual int compare(const spot::state* other) const override
     {
       auto o = down_cast<const twa_graph_state*>(other);
       assert(o);
@@ -55,19 +55,19 @@ namespace spot
       return 0;
     }
 
-    virtual size_t hash() const
+    virtual size_t hash() const override
     {
       return
 	reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
     }
 
     virtual twa_graph_state*
-    clone() const
+    clone() const override
     {
       return const_cast<twa_graph_state*>(this);
     }
 
-    virtual void destroy() const
+    virtual void destroy() const override
     {
     }
   };
@@ -121,41 +121,41 @@ namespace spot
     {
     }
 
-    virtual void recycle(edge t)
+    void recycle(edge t)
     {
       t_ = t;
     }
 
-    virtual bool first()
+    virtual bool first() override
     {
       p_ = t_;
       return p_;
     }
 
-    virtual bool next()
+    virtual bool next() override
     {
       p_ = g_->edge_storage(p_).next_succ;
       return p_;
     }
 
-    virtual bool done() const
+    virtual bool done() const override
     {
       return !p_;
     }
 
-    virtual const twa_graph_state* dst() const
+    virtual const twa_graph_state* dst() const override
     {
       assert(!done());
       return &g_->state_data(g_->edge_storage(p_).dst);
     }
 
-    virtual bdd cond() const
+    virtual bdd cond() const override
     {
       assert(!done());
       return g_->edge_data(p_).cond;
     }
 
-    virtual acc_cond::mark_t acc() const
+    virtual acc_cond::mark_t acc() const override
     {
       assert(!done());
       return g_->edge_data(p_).acc;
@@ -267,7 +267,7 @@ namespace spot
       return init_number_;
     }
 
-    virtual const twa_graph_state* get_init_state() const
+    virtual const twa_graph_state* get_init_state() const override
     {
       if (num_states() == 0)
 	const_cast<graph_t&>(g_).new_state();
@@ -275,7 +275,7 @@ namespace spot
     }
 
     virtual twa_succ_iterator*
-    succ_iter(const state* st) const
+    succ_iter(const state* st) const override
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
       assert(s);
@@ -313,7 +313,7 @@ namespace spot
       return ss.str();
     }
 
-    virtual std::string format_state(const state* st) const
+    virtual std::string format_state(const state* st) const override
     {
       return format_state(state_number(st));
     }
diff --git a/spot/twa/twaproduct.hh b/spot/twa/twaproduct.hh
index 59dc188ab..5af90fd33 100644
--- a/spot/twa/twaproduct.hh
+++ b/spot/twa/twaproduct.hh
@@ -49,7 +49,7 @@ namespace spot
     {
     }
 
-    virtual void destroy() const;
+    virtual void destroy() const override;
 
     const state*
     left() const
@@ -63,9 +63,9 @@ namespace spot
       return right_;
     }
 
-    virtual int compare(const state* other) const;
-    virtual size_t hash() const;
-    virtual state_product* clone() const;
+    virtual int compare(const state* other) const override;
+    virtual size_t hash() const override;
+    virtual state_product* clone() const override;
 
   private:
     const state* left_;		///< State from the left automaton.
@@ -74,7 +74,7 @@ namespace spot
     fixed_size_pool* pool_;
 
     virtual ~state_product();
-    state_product(const state_product& o); // No implementation.
+    state_product(const state_product& o) = delete;
   };
 
 
@@ -90,14 +90,15 @@ namespace spot
 
     virtual ~twa_product();
 
-    virtual const state* get_init_state() const;
+    virtual const state* get_init_state() const override;
 
     virtual twa_succ_iterator*
-    succ_iter(const state* state) const;
+    succ_iter(const state* state) const override;
 
-    virtual std::string format_state(const state* state) const;
+    virtual std::string format_state(const state* state) const override;
 
-    virtual state* project_state(const state* s, const const_twa_ptr& t) const;
+    virtual state* project_state(const state* s, const const_twa_ptr& t)
+      const override;
 
     const acc_cond& left_acc() const;
     const acc_cond& right_acc() const;
@@ -120,7 +121,7 @@ namespace spot
   public:
     twa_product_init(const const_twa_ptr& left, const const_twa_ptr& right,
 		      const state* left_init, const state* right_init);
-    virtual const state* get_init_state() const;
+    virtual const state* get_init_state() const override;
   protected:
     const state* left_init_;
     const state* right_init_;
@@ -135,11 +136,11 @@ namespace spot
 
   /// \brief on-the-fly TGBA product with forced initial states
   inline twa_product_ptr otf_product_at(const const_twa_ptr& left,
-					 const const_twa_ptr& right,
-					 const state* left_init,
-					 const state* right_init)
+					const const_twa_ptr& right,
+					const state* left_init,
+					const state* right_init)
   {
     return std::make_shared<twa_product_init>(left, right,
-					       left_init, right_init);
+					      left_init, right_init);
   }
 }
diff --git a/spot/twaalgos/gtec/ce.cc b/spot/twaalgos/gtec/ce.cc
index 3beb69c49..77c931234 100644
--- a/spot/twaalgos/gtec/ce.cc
+++ b/spot/twaalgos/gtec/ce.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -170,7 +170,7 @@ namespace spot
     const state* substart = ecs_->cycle_seed;
     do
       {
-	struct scc_bfs: bfs_steps
+	struct scc_bfs final: bfs_steps
 	{
 	  const couvreur99_check_status* ecs;
 	  couvreur99_check_result* r;
@@ -186,7 +186,7 @@ namespace spot
 	  }
 
 	  virtual const state*
-	  filter(const state* s)
+	  filter(const state* s) override
 	  {
 	    auto i = ecs->h.find(s);
 	    s->destroy();
@@ -201,7 +201,7 @@ namespace spot
 	  }
 
 	  virtual bool
-	  match(twa_run::step& st, const state* s)
+	  match(twa_run::step& st, const state* s) override
 	  {
 	    acc_cond::mark_t less_acc =
 	      acc_to_traverse - st.acc;
diff --git a/spot/twaalgos/gtec/ce.hh b/spot/twaalgos/gtec/ce.hh
index 4de35904a..a23e921cc 100644
--- a/spot/twaalgos/gtec/ce.hh
+++ b/spot/twaalgos/gtec/ce.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
+// Copyright (C) 2013, 2014, 2016 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -29,7 +29,7 @@
 namespace spot
 {
   /// Compute a counter example from a spot::couvreur99_check_status
-  class SPOT_API couvreur99_check_result:
+  class SPOT_API couvreur99_check_result final:
     public emptiness_check_result,
     public acss_statistics
   {
@@ -38,11 +38,11 @@ namespace spot
 			    std::shared_ptr<const couvreur99_check_status>& ecs,
 			    option_map o = option_map());
 
-    virtual twa_run_ptr accepting_run();
+    virtual twa_run_ptr accepting_run() override;
 
     void print_stats(std::ostream& os) const;
 
-    virtual unsigned acss_states() const;
+    virtual unsigned acss_states() const override;
 
   protected:
     /// Called by accepting_run() to find a cycle which traverses all
diff --git a/spot/twaalgos/gtec/gtec.hh b/spot/twaalgos/gtec/gtec.hh
index 4d834d30a..5373aeedc 100644
--- a/spot/twaalgos/gtec/gtec.hh
+++ b/spot/twaalgos/gtec/gtec.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -146,12 +146,13 @@ namespace spot
   {
   public:
     couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
+
     virtual ~couvreur99_check();
 
     /// Check whether the automaton's language is empty.
-    virtual emptiness_check_result_ptr check();
+    virtual emptiness_check_result_ptr check() override;
 
-    virtual std::ostream& print_stats(std::ostream& os) const;
+    virtual std::ostream& print_stats(std::ostream& os) const override;
 
     /// \brief Return the status of the emptiness-check.
     ///
@@ -190,7 +191,7 @@ namespace spot
     couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
     virtual ~couvreur99_check_shy();
 
-    virtual emptiness_check_result_ptr check();
+    virtual emptiness_check_result_ptr check() override;
 
   protected:
     struct successor {
diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc
index bfe1628e3..5e8756d1f 100644
--- a/spot/twaalgos/gv04.cc
+++ b/spot/twaalgos/gv04.cc
@@ -85,7 +85,7 @@ namespace spot
       }
 
       virtual emptiness_check_result_ptr
-      check()
+      check() override
       {
 	top = dftop = -1;
 	violation = false;
@@ -226,7 +226,7 @@ namespace spot
       }
 
       virtual std::ostream&
-      print_stats(std::ostream& os) const
+      print_stats(std::ostream& os) const override
       {
 	os << h.size() << " unique states visited\n";
 	os << transitions() << " transitions explored\n";
@@ -264,7 +264,7 @@ namespace spot
 	}
 
 	virtual unsigned
-	acss_states() const
+	acss_states() const override
 	{
 	  // Gross!
 	  const_cast<result*>(this)->update_lowlinks();
@@ -282,7 +282,7 @@ namespace spot
 	}
 
 	virtual twa_run_ptr
-	accepting_run()
+	accepting_run() override
 	{
 	  auto res = std::make_shared<twa_run>(automaton());
 
@@ -335,7 +335,7 @@ namespace spot
 	    }
 
 	    virtual const state*
-	    filter(const state* s)
+	    filter(const state* s) override
 	    {
 	      // Do not escape the SCC
 	      auto j = data.h.find(s);
@@ -357,13 +357,13 @@ namespace spot
 	    }
 
 	    virtual bool
-	    match(twa_run::step& step, const state*)
+	    match(twa_run::step& step, const state*) override
 	    {
 	      return step.acc != 0U;
 	    }
 	  };
 
-	  struct second_bfs: first_bfs
+	  struct second_bfs final: first_bfs
 	  {
 	    const state* target;
 	    second_bfs(result* r, int scc_root, const state* target)
@@ -372,7 +372,7 @@ namespace spot
 	    }
 
 	    virtual bool
-	    match(twa_run::step&, const state* s)
+	    match(twa_run::step&, const state* s) override
 	    {
 	      return s == target;
 	    }
diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc
index c4275e7c3..cd3672751 100644
--- a/spot/twaalgos/ltl2taa.cc
+++ b/spot/twaalgos/ltl2taa.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -29,7 +29,7 @@ namespace spot
   namespace
   {
     /// \brief Recursively translate a formula into a TAA.
-    class ltl2taa_visitor
+    class ltl2taa_visitor final
     {
     public:
       ltl2taa_visitor(const taa_tgba_formula_ptr& res,
@@ -40,7 +40,6 @@ namespace spot
       {
       }
 
-      virtual
       ~ltl2taa_visitor()
       {
       }
diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc
index 92fe4f766..9a979fabb 100644
--- a/spot/twaalgos/magic.cc
+++ b/spot/twaalgos/magic.cc
@@ -87,7 +87,7 @@ namespace spot
       /// check() can be called several times (until it returns a null
       /// pointer) to enumerate all the visited accepting paths. The method
       /// visits only a finite set of accepting paths.
-      virtual emptiness_check_result_ptr check()
+      virtual emptiness_check_result_ptr check() override
       {
 	auto t = std::static_pointer_cast<magic_search_>
 	  (this->emptiness_check::shared_from_this());
@@ -114,7 +114,7 @@ namespace spot
         return nullptr;
       }
 
-      virtual std::ostream& print_stats(std::ostream &os) const
+      virtual std::ostream& print_stats(std::ostream &os) const override
       {
         os << states() << " distinct nodes visited" << std::endl;
         os << transitions() << " transitions explored" << std::endl;
@@ -128,7 +128,7 @@ namespace spot
         return os;
       }
 
-      virtual bool safe() const
+      virtual bool safe() const override
       {
 	return heap::Safe;
       }
@@ -319,7 +319,7 @@ namespace spot
         return false;
       }
 
-      class result_from_stack: public emptiness_check_result,
+      class result_from_stack final: public emptiness_check_result,
         public acss_statistics
       {
       public:
@@ -328,7 +328,7 @@ namespace spot
         {
         }
 
-        virtual twa_run_ptr accepting_run()
+        virtual twa_run_ptr accepting_run() override
         {
           assert(!ms_->st_blue.empty());
           assert(!ms_->st_red.empty());
@@ -366,7 +366,7 @@ namespace spot
           return run;
         }
 
-        unsigned acss_states() const
+        virtual unsigned acss_states() const override
         {
           return 0;
         }
@@ -376,7 +376,7 @@ namespace spot
 
 #     define FROM_STACK "ar:from_stack"
 
-      class magic_search_result: public emptiness_check_result
+      class magic_search_result final: public emptiness_check_result
       {
       public:
         magic_search_result(const std::shared_ptr<magic_search_>& m,
@@ -389,7 +389,7 @@ namespace spot
             computer = new ndfs_result<magic_search_<heap>, heap>(ms);
         }
 
-        virtual void options_updated(const option_map& old)
+        virtual void options_updated(const option_map& old) override
         {
           if (old[FROM_STACK] && !options()[FROM_STACK])
             {
@@ -408,12 +408,12 @@ namespace spot
           delete computer;
         }
 
-        virtual twa_run_ptr accepting_run()
+        virtual twa_run_ptr accepting_run() override
         {
           return computer->accepting_run();
         }
 
-        virtual const unsigned_statistics* statistics() const
+        virtual const unsigned_statistics* statistics() const override
         {
           return computer->statistics();
         }
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 7fc6ded58..22d394455 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -174,7 +174,7 @@ namespace spot
       return res;
     }
 
-    struct wdba_search_acc_loop : public bfs_steps
+    struct wdba_search_acc_loop final : public bfs_steps
     {
       wdba_search_acc_loop(const const_twa_ptr& det_a,
 			   unsigned scc_n, scc_info& sm,
@@ -185,7 +185,7 @@ namespace spot
       }
 
       virtual const state*
-      filter(const state* s)
+      filter(const state* s) override
       {
 	s = seen(s);
 	if (sm.scc_of(std::static_pointer_cast<const twa_graph>(a_)
@@ -195,7 +195,7 @@ namespace spot
       }
 
       virtual bool
-      match(twa_run::step&, const state* to)
+      match(twa_run::step&, const state* to) override
       {
 	return to == dest;
       }
diff --git a/spot/twaalgos/ndfs_result.hxx b/spot/twaalgos/ndfs_result.hxx
index a5d5281d1..28c074f37 100644
--- a/spot/twaalgos/ndfs_result.hxx
+++ b/spot/twaalgos/ndfs_result.hxx
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de recherche et
-// développement de l'Epita (LRDE).
+// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche
+// et développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -76,8 +76,8 @@ namespace spot
     struct stats_interface<T, 1>
       : public acss_statistics
     {
-      unsigned
-      acss_states() const
+      virtual unsigned
+      acss_states() const override
       {
 	// all visited states are in the state space search
 	return static_cast<const T*>(this)->h_.size();
@@ -88,7 +88,7 @@ namespace spot
 
 
   template <typename ndfs_search, typename heap>
-  class ndfs_result:
+  class ndfs_result final:
     public emptiness_check_result,
     // Conditionally inherit from acss_statistics or ars_statistics.
     public stats_interface<ndfs_result<ndfs_search, heap>, heap::Has_Size>
@@ -104,7 +104,7 @@ namespace spot
     {
     }
 
-    virtual twa_run_ptr accepting_run()
+    virtual twa_run_ptr accepting_run() override
     {
       const stack_type& stb = ms_->get_st_blue();
       const stack_type& str = ms_->get_st_red();
diff --git a/spot/twaalgos/reachiter.hh b/spot/twaalgos/reachiter.hh
index d7f11906e..e0ea4d374 100644
--- a/spot/twaalgos/reachiter.hh
+++ b/spot/twaalgos/reachiter.hh
@@ -102,8 +102,8 @@ namespace spot
   public:
     tgba_reachable_iterator_breadth_first(const const_twa_ptr& a);
 
-    virtual void add_state(const state* s);
-    virtual const state* next_state();
+    virtual void add_state(const state* s) override;
+    virtual const state* next_state() override;
 
   protected:
     std::deque<const state*> todo; ///< A queue of states yet to explore.
@@ -189,8 +189,8 @@ namespace spot
     /// the stack after process_link() has been called.
     bool on_stack(int sn) const;
   protected:
-    virtual void push(const state* s, int sn);
-    virtual void pop();
+    virtual void push(const state* s, int sn) override;
+    virtual void pop() override;
 
     std::unordered_set<int> stack_;
   };
diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc
index 13df110fd..9d6f7def5 100644
--- a/spot/twaalgos/se05.cc
+++ b/spot/twaalgos/se05.cc
@@ -47,7 +47,7 @@ namespace spot
     /// \brief Emptiness checker on spot::tgba automata having at most one
     /// acceptance condition (i.e. a TBA).
     template <typename heap>
-    class se05_search : public emptiness_check, public ec_statistics
+    class se05_search final : public emptiness_check, public ec_statistics
     {
     public:
       /// \brief Initialize the Magic Search algorithm on the automaton \a a
@@ -87,7 +87,7 @@ namespace spot
       /// check() can be called several times (until it returns a null
       /// pointer) to enumerate all the visited accepting paths. The method
       /// visits only a finite set of accepting paths.
-      virtual emptiness_check_result_ptr check()
+      virtual emptiness_check_result_ptr check() override
       {
 	auto t = std::static_pointer_cast<se05_search>
 	  (this->emptiness_check::shared_from_this());
@@ -114,7 +114,7 @@ namespace spot
         return nullptr;
       }
 
-      virtual std::ostream& print_stats(std::ostream &os) const
+      virtual std::ostream& print_stats(std::ostream &os) const override
       {
         os << states() << " distinct nodes visited" << std::endl;
         os << transitions() << " transitions explored" << std::endl;
@@ -128,7 +128,7 @@ namespace spot
         return os;
       }
 
-      virtual bool safe() const
+      virtual bool safe() const override
       {
 	return heap::Safe;
       }
@@ -334,7 +334,7 @@ namespace spot
         {
         }
 
-        virtual twa_run_ptr accepting_run()
+        virtual twa_run_ptr accepting_run() override
         {
           assert(!ms_->st_blue.empty());
           assert(!ms_->st_red.empty());
@@ -378,7 +378,7 @@ namespace spot
           return run;
         }
 
-        unsigned acss_states() const
+        virtual unsigned acss_states() const override
         {
           return 0;
         }
@@ -388,7 +388,7 @@ namespace spot
 
 #     define FROM_STACK "ar:from_stack"
 
-      class se05_result: public emptiness_check_result
+      class se05_result final: public emptiness_check_result
       {
       public:
         se05_result(const std::shared_ptr<se05_search>& m,
@@ -401,7 +401,7 @@ namespace spot
             computer = new ndfs_result<se05_search<heap>, heap>(ms);
         }
 
-        virtual void options_updated(const option_map& old)
+        virtual void options_updated(const option_map& old) override
         {
           if (old[FROM_STACK] && !options()[FROM_STACK])
             {
@@ -420,12 +420,12 @@ namespace spot
           delete computer;
         }
 
-        virtual twa_run_ptr accepting_run()
+        virtual twa_run_ptr accepting_run() override
         {
           return computer->accepting_run();
         }
 
-        virtual const unsigned_statistics* statistics() const
+        virtual const unsigned_statistics* statistics() const override
         {
           return computer->statistics();
         }
diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc
index 654b46c35..288c696bb 100644
--- a/spot/twaalgos/stutter.cc
+++ b/spot/twaalgos/stutter.cc
@@ -40,7 +40,7 @@ namespace spot
 {
   namespace
   {
-    class state_tgbasl: public state
+    class state_tgbasl final: public state
     {
     public:
       state_tgbasl(const state* s, bdd cond) : s_(s), cond_(cond)
@@ -54,7 +54,7 @@ namespace spot
       }
 
       virtual int
-      compare(const state* other) const
+      compare(const state* other) const override
       {
         const state_tgbasl* o =
           down_cast<const state_tgbasl*>(other);
@@ -66,13 +66,13 @@ namespace spot
       }
 
       virtual size_t
-      hash() const
+      hash() const override
       {
         return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
       }
 
       virtual
-      state_tgbasl* clone() const
+      state_tgbasl* clone() const override
       {
         return new state_tgbasl(*this);
       }
@@ -94,7 +94,7 @@ namespace spot
       bdd cond_;
     };
 
-    class twasl_succ_iterator : public twa_succ_iterator
+    class twasl_succ_iterator final : public twa_succ_iterator
     {
     public:
       twasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state,
@@ -111,8 +111,8 @@ namespace spot
 
       // iteration
 
-      bool
-      first()
+      virtual bool
+      first() override
       {
         loop_ = false;
         done_ = false;
@@ -125,8 +125,8 @@ namespace spot
         return true;
       }
 
-      bool
-      next()
+      virtual bool
+      next() override
       {
         if (cond_ != bddfalse)
           {
@@ -148,32 +148,32 @@ namespace spot
           }
       }
 
-      bool
-      done() const
+      virtual bool
+      done() const override
       {
         return it_->done() && done_;
       }
 
       // inspection
 
-      state_tgbasl*
-      dst() const
+      virtual state_tgbasl*
+      dst() const override
       {
         if (loop_)
           return new state_tgbasl(state_->real_state(), state_->cond());
         return new state_tgbasl(it_->dst(), one_);
       }
 
-      bdd
-      cond() const
+      virtual bdd
+      cond() const override
       {
         if (loop_)
           return state_->cond();
         return one_;
       }
 
-      acc_cond::mark_t
-      acc() const
+      virtual acc_cond::mark_t
+      acc() const override
       {
         if (loop_)
           return 0U;
diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc
index 874f816b6..0e9cd2512 100644
--- a/spot/twaalgos/tau03.cc
+++ b/spot/twaalgos/tau03.cc
@@ -50,7 +50,7 @@ namespace spot
     /// \brief Emptiness checker on spot::tgba automata having at most one
     /// acceptance condition (i.e. a TBA).
     template <typename heap>
-    class tau03_search : public emptiness_check, public ec_statistics
+    class tau03_search final : public emptiness_check, public ec_statistics
     {
     public:
       /// \brief Initialize the search algorithm on the automaton \a a
@@ -82,7 +82,7 @@ namespace spot
       ///
       /// \return non null pointer iff the algorithm has found an
       /// accepting path.
-      virtual emptiness_check_result_ptr check()
+      virtual emptiness_check_result_ptr check() override
       {
         if (!st_blue.empty())
             return nullptr;
@@ -98,7 +98,7 @@ namespace spot
         return nullptr;
       }
 
-      virtual std::ostream& print_stats(std::ostream &os) const
+      virtual std::ostream& print_stats(std::ostream &os) const override
       {
         os << states() << " distinct nodes visited" << std::endl;
         os << transitions() << " transitions explored" << std::endl;