diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 29aea1b1ba1f4f8b0c199414ce2db39e86f7e7cc..b889109f461ee67f67d95f3b46a0b4aab004edd1 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -33,7 +33,7 @@ module Translate: sig
   exception No_simple_translation of term
   val term_to_exp: typ option -> term -> exp
 (** @raise New_typing_error when the given term cannot be typed (something wrong
-    happends with this term)
+    happened with this term)
     @raise Not_yet when the given term contains an unsupported construct.
     @raise No_simple_translation when the given term cannot be translated into
     a single expression. *)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index bbcf78dedebb7f60052f788e1606d485795cd53e..b482e45965e933015939a0b2f318fa8ac4b1e1af 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -16,7 +16,7 @@
   \item \changeinsection{statement_contract}{fix syntax rule for statement
     contracts in allowing completeness clauses}
   \item \changeinsection{memory}{add syntax for defining a set by giving
-    explicitely its element}
+    explicitly its element}
   \item \changeinsection{typedpointers}{new section}
   \end{itemize}
 \end{itemize}
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 45e382a42f8f72c07573373ee6b6d206ed302506..a4a7c550087912c9fde632c5b3d7790fc6270d75 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -121,7 +121,7 @@ let dup_fundec loc spec bhv kf vi new_vi =
   let mk_formal vi =
     let name =
       if vi.vname = "" then
-        (* unamed formal parameter: must generate a fresh name since a fundec
+        (* unnamed formal parameter: must generate a fresh name since a fundec
            cannot have unnamed formals (see bts #2303). *)
         Env.Varname.get ~scope:Env.Function
           (Functions.RTL.mk_gen_name "unamed_formal")
@@ -219,7 +219,7 @@ class dup_functions_visitor prj = object (self)
   val mutable before_memory_model = Before_gmp
   val mutable new_definitions: global list = []
   (* new definitions of the annotated functions which will contain the
-     translation of the E-ACSL constract *)
+     translation of the E-ACSL contract *)
 
   method private before_memory_model = match before_memory_model with
   | Before_gmp | Gmp | After_gmp -> true
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 9c604d2135eca498d0f694ae0eb3980cd5fcc0cc..c23b7089391859f366f7f5ccb651de7881b662a4 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -483,7 +483,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
     else
       b
   in
-  (* remove superflous brackets inside the generated block *)
+  (* remove superfluous brackets inside the generated block *)
   let final_blk = Cil.flatten_transient_sub_blocks final_blk in
   (* remove the non-scoping mark of the outermost block *)
   let final_blk = Cil.block_of_transient final_blk in
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 958f24409ddb7955bf1f35c341107e3408732121..0a1e07d7b7845b5cb3305271bd22b74c452e3ffe 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -23,7 +23,7 @@
 (** Interval inference for terms.
 
     Compute the smallest interval that contains all the possible values of a
-    given integer term. The interval of C variables is directly infered from
+    given integer term. The interval of C variables is directly inferred from
     their C type. The interval of logic variables must be registered from
     outside before computing the interval of a term containing such variables
     (see module {!Interval.Env}).
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index d8c90534dff4829adb75f1c158ed3b170279a6bd..e3b74c7e0d8b54af5ba9c77b5fe70097f94a7585 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -58,7 +58,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
           s_ref := new_stmt;
         Cil.SkipChildren
       | _ -> Cil.DoChildren
-      (* improve efficiency: skip childrens which cannot contain any label *)
+      (* improve efficiency: skip children which cannot contain any label *)
       method !vinst _ = Cil.SkipChildren
       method !vexpr _ = Cil.SkipChildren
       method !vlval _ = Cil.SkipChildren
diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli
index 27a0596d6bebac28d96e9cf2fb72244e49616c6b..ed7dd9c48609582174e44991ede2c0b94e2f174a 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -37,7 +37,7 @@ val mv_invariants: Env.t -> old:stmt -> stmt -> unit
 val preserve_invariant:
   Project.t -> Env.t -> Kernel_function.t -> stmt -> stmt * Env.t * bool
 (** modify the given stmt loop to insert the code which preserves its loop
-    invarariants. Also return the modify environment and a boolean which
+    invariants. Also return the modify environment and a boolean which
     indicates whether the annotations corresponding to the loop invariant must
     be moved from the new statement to the old one. *)
 
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index ee27e0f4521669541c6d780dc0e6f5860a90219a..e346f67efef5bad0369f2f0db61d42feb40e9b21 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -56,7 +56,7 @@ let get_lib_fun_vi fname =
     with Not_found ->
       try Builtins.find fname
       with Not_found ->
-        (* could not happen in normal mode, but coud be raised when E-ACSL is
+        (* could not happen in normal mode, but could be raised when E-ACSL is
            used as a library *)
         raise (Unregistered_library_function fname)
 
diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
index d4f5ff13979b7fd57b831f14c0c01dfa25bea346..5880b8b8024cf01321fa47a8cbf48573f349d4e7 100644
--- a/src/plugins/e-acsl/mmodel_translate.ml
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -45,7 +45,7 @@ let term_to_exp_ref
     [\forall integer q1; n-1 <= q1 <= n+2 ==>
       \forall integer q2; 0 <= q2 <= 1 ==>
         \valid(&t[q1][1][q2])]
-  However, the substition can be unsound,
+  However, the substitution can be unsound,
   in which case [Range_elimination_exception] must be raised.
   Example:
     [\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
@@ -134,7 +134,7 @@ let call ~loc kf name ctx env t =
 (********************** \initialized, \valid, \valid_read ********************)
 (*****************************************************************************)
 
-(* Take the term [size] thas has been typed into GMP
+(* Take the term [size] that has been typed into GMP
    and return an expression of type [size_t].
    The case where [!(0 <= size < SIZE_MAX)] is an UB ==> guard against it. *)
 let gmp_to_sizet ~loc kf env size p =
@@ -256,7 +256,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
        The generated code is a SET OF calls to the corresponding E-ACSL builtin
     C: Any other use of ranges/No range
        Call [call_default] which performs the translation for
-       range free terms, and raises Not_yet if it ever encouters a range.
+       range free terms, and raises Not_yet if it ever encounters a range.
   Example for case:
     A: [\valid(&t[3..5])]
        Contiguous locations -> a single call to [__e_acsl_valid]
@@ -393,4 +393,4 @@ let call_valid ~loc kf name ctx env t p =
     env
     t
     p
-    call_for_unsupported_constructs
\ No newline at end of file
+    call_for_unsupported_constructs
diff --git a/src/plugins/e-acsl/prepare_ast.mli b/src/plugins/e-acsl/prepare_ast.mli
index c2db62e1ea87f389e9522aba28f00fa8356d49cf..9ba5b76b9a9082487f74257ef0b27ac8ce58995e 100644
--- a/src/plugins/e-acsl/prepare_ast.mli
+++ b/src/plugins/e-acsl/prepare_ast.mli
@@ -22,7 +22,7 @@
 
 (** Prepare AST for E-ACSL generation.
 
-    So for this mudule performs two tasks:
+    So for this module performs two tasks:
     - move declarations of variables declared in the bodies of switch
     statements to upper scopes;
     - store what is necessary to translate in [Keep_status]. *)
diff --git a/src/plugins/e-acsl/temporal.mli b/src/plugins/e-acsl/temporal.mli
index bd2e1606a1eb3c8e4be6a1a911657f735140dfb4..17b419e08d98b6391fe1024d857f18dfeb0cca53 100644
--- a/src/plugins/e-acsl/temporal.mli
+++ b/src/plugins/e-acsl/temporal.mli
@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Transformations to detect temporal memory errors (e.g., derererence of
+(** Transformations to detect temporal memory errors (e.g., dereference of
     stale pointers). *)
 
 val enable: bool -> unit
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 4195ec14f10a235721c0f99a692de9b75a1314d3..8182360e77e376bfb86627f152fc2e3377706b13 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -50,7 +50,7 @@ open Cil_types
 (** {2 Datatypes} *)
 (******************************************************************************)
 
-(** Possible types infered by the system. *)
+(** Possible types inferred by the system. *)
 type integer_ty = private
   | Gmp
   | C_type of ikind
@@ -105,15 +105,15 @@ val clear: unit -> unit
     predicate. *)
 
 val get_integer_ty: term -> integer_ty
-(** @return the infered type for the given term. *)
+(** @return the inferred type for the given term. *)
 
 val get_integer_op: term -> integer_ty
-(** @return the infered type for the top operation of the given term.
+(** @return the inferred type for the top operation of the given term.
     It is meaningless to call this function over a non-arithmetical/logical
     operator. *)
 
 val get_integer_op_of_predicate: predicate -> integer_ty
-(** @return the infered type for the top operation of the given predicate. *)
+(** @return the inferred type for the top operation of the given predicate. *)
 
 val get_typ: term -> typ
 (** Get the type which the given term must be generated to. *)