diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 2530178dcd3dd3803749afeab3842d2ccd122b1b..27d890da479eb9d570ef74b9d5586eac150c299a 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1103,7 +1103,7 @@ let getInitialState () =
 (** This function computes all newly introduced globals (variables, enumeration structure, invariants, etc. *)
 let initGlobals root complete =
   mk_global_comment "//****************";
-  mk_global_comment "//* BEGIN Primitives generated for LTL verification";
+  mk_global_comment "//* BEGIN Primitives generated for Aorai verification";
   mk_global_comment "//* ";
   mk_global_comment "//* ";
   mk_global_comment "//* Some constants";
@@ -1168,7 +1168,7 @@ let initGlobals root complete =
      in
      Annotations.add_global Aorai_option.emitter annot);
   mk_global_comment "//* ";
-  mk_global_comment "//* END Primitives generated for LTL verification";
+  mk_global_comment "//* END Primitives generated for Aorai verification";
   mk_global_comment "//****************";
 
   flush_globals ()
diff --git a/src/plugins/aorai/automaton_ast.ml b/src/plugins/aorai/automaton_ast.ml
index 897f87b0ed177c5d9585d54eb7294ddd31c89461..d7ea342f2314e38023446cd231b151f1d9ba4cc4 100644
--- a/src/plugins/aorai/automaton_ast.ml
+++ b/src/plugins/aorai/automaton_ast.ml
@@ -23,7 +23,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** The abstract tree of promela representation. Such tree is used by promela
+(** The abstract tree of Ya representation. Such tree is used by
     parser/lexer before its translation into Data_for_aorai module. *)
 
 type expression =
@@ -57,7 +57,7 @@ and seq_elt = {
 
 and sequence = seq_elt list
 
-(** Promela parsed abstract syntax trees. Either a sequence of event or the
+(** Ya parsed abstract syntax trees. Either a sequence of event or the
     otherwise keyword. A single condition is expressed with a singleton
     having an empty nested sequence and min_rep and max_rep being equal to one.
 *)
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 8cf944ec63b26485c71fa9d0e8e3a732caaf0556..a3c5d4599533d02f684a9e1cef6774b260fcb51f 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -35,10 +35,10 @@ open Automaton_ast
 exception Empty_automaton
 
 (* ************************************************************************* *)
-(** {2 LTL/Promela primitives} *)
+(** {2 Automaton primitives} *)
 (* ************************************************************************* *)
 
-(** Here are some operations used for generation of LTL AST or Promela AST. *)
+(** Here are some operations used for generation of automaton AST. *)
 
 module Aorai_state: Datatype.S_with_collections with type t = Automaton_ast.state
 
diff --git a/src/plugins/aorai/pretty_automaton.ml b/src/plugins/aorai/pretty_automaton.ml
index 1ccf2caf684396893a2b19c3631df498a13de067..b91c1d103ba79fac5d267c3f2be5b544139187fa 100644
--- a/src/plugins/aorai/pretty_automaton.ml
+++ b/src/plugins/aorai/pretty_automaton.ml
@@ -249,7 +249,7 @@ struct
       let spaces = String.make fill ' ' in
       Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces
     in
-    one_line_comment "File generated by Aorai LTL2ACSL Plug-in";
+    one_line_comment "File generated by Aorai Plug-in";
     one_line_comment "";
     one_line_comment "Usage of dot files '.dot' :";
     one_line_comment "  dot <MyFile.dot> -T<DesiredType> > <OutputFile>";
diff --git a/src/plugins/aorai/utils_parser.mli b/src/plugins/aorai/utils_parser.mli
index bb89f79da9fc0eb76cd72ee21f221e2d0ff3e439..4505784eea27422d420ab6a5a86a8e04af78eb82 100644
--- a/src/plugins/aorai/utils_parser.mli
+++ b/src/plugins/aorai/utils_parser.mli
@@ -23,7 +23,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** utilities for parsing automata and LTL formulas *)
+(** utilities for parsing automaton's formulas *)
 
 (** returns the position corresponding to the
     current character in the lexbuf. *)