diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
index 5ee902fd9..3463c7357 100644
--- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs
+++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
@@ -19,6 +19,12 @@ namespace PChecker
     public class CheckerConfiguration
     {
 
+        /// <summary>
+        /// The P compiled path.
+        /// </summary>
+        [DataMember]
+        public string PCompiledPath;
+        
         /// <summary>
         /// The output path.
         /// </summary>
@@ -280,6 +286,7 @@ public int MaxSchedulingSteps
         /// </summary>
         protected CheckerConfiguration()
         {
+            PCompiledPath = Directory.GetCurrentDirectory();
             OutputPath = "PCheckerOutput";
 
             Timeout = 0;
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs b/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
index 93208a1a3..b21d20ad1 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
@@ -115,10 +115,10 @@ internal static string AsFFIComment(string line)
     <modelVersion>4.0.0</modelVersion>
 
     <groupId>com.amazon.p</groupId>
-    <artifactId>-project-name-</artifactId>
+    <artifactId>-package-name-</artifactId>
     <version>1.0-SNAPSHOT</version>
 
-    <name>-project-name-</name>
+    <name>-package-name-</name>
     <properties>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
         <maven.compiler.source>11</maven.compiler.source>
@@ -165,7 +165,6 @@ internal static string AsFFIComment(string line)
                 </executions>
             </plugin>
         </plugins>
-        <directory>${{buildDirectory}}</directory>
         <sourceDirectory>.</sourceDirectory>
     </build>
 </project>";
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/JavaCompiler.cs b/Src/PCompiler/CompilerCore/Backend/Java/JavaCompiler.cs
index e44a7859c..b9970193c 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/JavaCompiler.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/JavaCompiler.cs
@@ -14,7 +14,7 @@ public void GenerateBuildScript(ICompilerConfiguration job)
 
             // create the pom.xml file
             var pomTemplate = Constants.pomTemplate;
-            pomTemplate = pomTemplate.Replace("-project-name-",job.ProjectName);
+            pomTemplate = pomTemplate.Replace("-package-name-",job.PObservePackageName);
             
             string foreignInclude = "";
             var foreignFiles = job.InputForeignFiles.Where(x => x.EndsWith(".java"));
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/JavaSourceGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/JavaSourceGenerator.cs
index 46298d2fc..3af2b83b0 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/JavaSourceGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/JavaSourceGenerator.cs
@@ -14,7 +14,7 @@ public abstract class JavaSourceGenerator
 
         internal NameManager Names => _context.Names;
         internal TypeManager Types => _context.Types;
-        internal String PackageName => $"{Job.ProjectName}.pobserve";
+        internal String PackageName => $"{Job.PObservePackageName}";
 
         /// <summary>
         /// Constructs a new Java source generator for a particular output file.
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
index 3c7092016..b05a576a2 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
@@ -15,6 +15,7 @@ internal class MachineGenerator : JavaSourceGenerator
     {
 
         private Machine _currentMachine; // Some generated code is machine-dependent, so stash the current machine here.
+        private HashSet<Function> _calledStaticFunctions = new HashSet<Function>(); // static functions allowed 
 
         internal MachineGenerator(ICompilerConfiguration job, string filename) : base(job, filename)
         {
@@ -47,6 +48,13 @@ protected override void GenerateCodeImpl()
                 }
                 _currentMachine = null;
             }
+            
+            // static functions
+            foreach (var f in _calledStaticFunctions)
+            {
+                WriteFunction(f);
+            }
+            
             WriteLine("}");
         }
 
@@ -608,7 +616,7 @@ private void WriteFunctionCallExpr(Function f, IEnumerable<IPExpr> args)
             var isStatic = f.Owner == null;
             if (isStatic && !f.IsForeign)
             {
-                throw new NotImplementedException("StaticFunCallExpr is not implemented.");
+                _calledStaticFunctions.Add(f);
             }
 
             var fname = Names.GetNameForDecl(f);
diff --git a/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs b/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs
index dee1dc332..9a17ea789 100644
--- a/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Symbolic/Constants.cs
@@ -62,7 +62,7 @@ internal class Constants
         <dependency>
             <groupId>io.github.p-org</groupId>
             <artifactId>psym</artifactId>
-            <version>[1.0.10,)</version>
+            <version>[1.1.0,)</version>
         </dependency>
 
         <!-- https://mvnrepository.com/artifact/org.projectlombok/lombok -->
diff --git a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs
index a72e0ed94..2af8de98f 100644
--- a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs
+++ b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs
@@ -16,6 +16,7 @@ public CompilerConfiguration()
             InputForeignFiles = new List<string>();
             Output = null;
             ProjectName = "generatedOutput";
+            PObservePackageName = $"{ProjectName}.pobserve";
             ProjectRootPath = new DirectoryInfo(Directory.GetCurrentDirectory());
             LocationResolver = new DefaultLocationResolver();
             Handler = new DefaultTranslationErrorHandler(LocationResolver);
@@ -47,6 +48,7 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, Co
                 }
             }
             ProjectName = projectName ?? Path.GetFileNameWithoutExtension(inputFiles[0]);
+            PObservePackageName = $"{ProjectName}.pobserve";
             ProjectRootPath = projectRoot;
             LocationResolver = new DefaultLocationResolver();
             Handler = new DefaultTranslationErrorHandler(LocationResolver);
@@ -59,6 +61,7 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, Co
         public DirectoryInfo OutputDirectory { get; set; }
         public CompilerOutput OutputLanguage { get; set; }
         public string ProjectName { get; set; }
+        public string PObservePackageName { get; set; }
         public DirectoryInfo ProjectRootPath { get; set; }
         public ICodeGenerator Backend { get; set; }
         public IList<string> InputPFiles { get; set; }
@@ -79,6 +82,7 @@ public void Copy(CompilerConfiguration parsedConfig)
             LocationResolver = parsedConfig.LocationResolver;
             ProjectDependencies = parsedConfig.ProjectDependencies;
             ProjectName = parsedConfig.ProjectName;
+            PObservePackageName = parsedConfig.PObservePackageName;
             OutputLanguage = parsedConfig.OutputLanguage;
             ProjectRootPath = parsedConfig.ProjectRootPath;
         }
diff --git a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs
index 3f30cc12b..2f524166c 100644
--- a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs
+++ b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs
@@ -8,6 +8,7 @@ namespace Plang.Compiler
     public interface ICompilerConfiguration
     {
         string ProjectName { get; }
+        string PObservePackageName { get; }
         DirectoryInfo ProjectRootPath { get; }
         CompilerOutput OutputLanguage { get; }
         ICompilerOutput Output { get; }
diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
index b925d3dac..f41708116 100644
--- a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
+++ b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
@@ -86,6 +86,12 @@ internal CheckerConfiguration Parse(string[] args)
             try
             {
                 var result = Parser.ParseArguments(args);
+                // if there are no --pproj or --pfiles arguments, then search for a pproj file locally and load it
+                FindLocalPProject(result);
+
+                // load pproj file first
+                UpdateConfigurationWithPProjectFile(configuration, result);
+                
                 foreach (var arg in result)
                 {
                     UpdateConfigurationWithParsedArgument(configuration, arg);
@@ -119,6 +125,50 @@ internal CheckerConfiguration Parse(string[] args)
             return configuration;
         }
 
+        private static void FindLocalPProject(List<CommandLineArgument> result)
+        {
+            // CommandLineOutput.WriteInfo(".. Searching for a P project file *.pproj locally in the current folder");
+            var filtered = 
+                from file in Directory.GetFiles(Directory.GetCurrentDirectory(), "*.pproj")
+                let info = new FileInfo(file)
+                where (((info.Attributes & FileAttributes.Hidden) ==0)& ((info.Attributes & FileAttributes.System)==0))
+                select file;
+            var files = filtered.ToArray();
+            if (files.Length == 0)
+            {
+                // CommandLineOutput.WriteInfo(
+                //     $".. No P project file *.pproj found in the current folder: {Directory.GetCurrentDirectory()}");
+            }
+            else
+            {
+                var commandlineArg = new CommandLineArgument();
+                commandlineArg.Value = files.First();
+                commandlineArg.LongName = "pproj";
+                commandlineArg.ShortName = "pp";
+                // CommandLineOutput.WriteInfo($".. Found P project file: {commandlineArg.Value}");
+                result.Add(commandlineArg);
+            }
+        }
+
+
+        /// <summary>
+        /// Updates the checker configuration with the specified P project file.
+        /// </summary>
+        private static void UpdateConfigurationWithPProjectFile(CheckerConfiguration configuration, List<CommandLineArgument> result)
+        {
+            foreach (var option in result)
+            {
+                switch (option.LongName)
+                {
+                    case "pproj":
+                    {
+                        new ParsePProjectFile().ParseProjectFileForChecker((string)option.Value, configuration);
+                    }
+                        return;
+                }
+            }
+        }
+        
         /// <summary>
         /// Updates the checkerConfiguration with the specified parsed argument.
         /// </summary>
@@ -257,6 +307,9 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
                 case "jvm-args":
                     checkerConfiguration.JvmArgs = ((string)option.Value).Replace(':', ' ');
                     break;
+                case "pproj":
+                    // do nothing, since already configured through UpdateConfigurationWithPProjectFile
+                    break;
                 default:
                     throw new Exception(string.Format("Unhandled parsed argument: '{0}'", option.LongName));
             }
@@ -306,7 +359,7 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura
         {
             if (checkerConfiguration.AssemblyToBeAnalyzed == string.Empty)
             {
-                CommandLineOutput.WriteInfo(".. Searching for a P compiled file locally in the current folder");
+                CommandLineOutput.WriteInfo($".. Searching for a P compiled file locally in folder {checkerConfiguration.PCompiledPath}");
                 var pathSep = Path.DirectorySeparatorChar;
                 
                 string filePattern =  checkerConfiguration.Mode switch
@@ -323,7 +376,7 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura
                 
                 
                 var files = 
-                    from file in Directory.GetFiles(Directory.GetCurrentDirectory(), filePattern, enumerationOptions)
+                    from file in Directory.GetFiles(checkerConfiguration.PCompiledPath, filePattern, enumerationOptions)
                     let info = new FileInfo(file)
                     where (((info.Attributes & FileAttributes.Hidden) ==0)& ((info.Attributes & FileAttributes.System)==0))
                     select file;
diff --git a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs
index 2a2c3079e..02b8441d0 100644
--- a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs
+++ b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs
@@ -42,6 +42,8 @@ internal PCompilerOptions()
             var modes = Parser.AddArgument("mode", "md", "Compilation mode :: (bugfinding, verification, coverage, pobserve, stately). (default: bugfinding)");
             modes.AllowedValues = new List<string>() { "bugfinding", "verification", "coverage", "pobserve", "stately" };
             modes.IsHidden = true;
+
+            Parser.AddArgument("pobserve-package", "po", "PObserve package name").IsHidden = true;
         }
 
         /// <summary>
@@ -132,7 +134,7 @@ private static void UpdateConfigurationWithPProjectFile(CompilerConfiguration co
                 {
                     case "pproj":
                     {
-                        new ParsePProjectFile().ParseProjectFile((string)option.Value, out var parsedConfig);
+                        new ParsePProjectFile().ParseProjectFileForCompiler((string)option.Value, out var parsedConfig);
                         compilerConfiguration.Copy(parsedConfig);
                     }
                         return;
@@ -169,6 +171,9 @@ private static void UpdateConfigurationWithParsedArgument(CompilerConfiguration
                         compilerConfiguration.Backend = TargetLanguage.GetCodeGenerator(compilerConfiguration.OutputLanguage);
                     }
                     break;
+                case "pobserve-package":
+                    compilerConfiguration.PObservePackageName = (string)option.Value;
+                    break;
                 case "pfiles":
                     {
                         var files = (string[])option.Value;
diff --git a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs
index 970006bee..3f6c1ae3d 100644
--- a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs
+++ b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs
@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using System.Xml.Linq;
+using PChecker;
 using PChecker.IO.Debugging;
 using Plang.Compiler;
 
@@ -12,12 +13,12 @@ internal class ParsePProjectFile
     {
 
         /// <summary>
-        /// Parse the P Project file
+        /// Parse the P Project file for compiler
         /// </summary>
         /// <param name="projectFile">Path to the P project file</param>
         /// <param name="job">out parameter of P compilation job, after parsing the project file</param>
         /// <returns></returns>
-        public void ParseProjectFile(string projectFile, out CompilerConfiguration job)
+        public void ParseProjectFileForCompiler(string projectFile, out CompilerConfiguration job)
         {
             job = null;
             try
@@ -65,6 +66,33 @@ public void ParseProjectFile(string projectFile, out CompilerConfiguration job)
             }
         }
 
+        /// <summary>
+        /// Parse the P Project file for P checker
+        /// </summary>
+        /// <param name="projectFile">Path to the P project file</param>
+        /// <param name="job">out parameter of P checker job, after parsing the project file</param>
+        /// <returns></returns>
+        public void ParseProjectFileForChecker(string projectFile, CheckerConfiguration job)
+        {
+            try
+            {
+                if (!CheckFileValidity.IsLegalPProjFile(projectFile, out var projectFilePath))
+                {
+                    throw new CommandlineParsingError($"Illegal P project file name {projectFile} or file {projectFilePath?.FullName} not found");
+                }
+
+                // set compiler output directory as p compiled path
+                job.PCompiledPath = GetOutputDirectoryName(projectFilePath);
+            }
+            catch (CommandlineParsingError ex)
+            {
+                Error.ReportAndExit($"<Error parsing project file>:\n {ex.Message}");
+            }
+            catch (Exception other)
+            {
+                Error.ReportAndExit($"<Internal Error>:\n {other.Message}\n <Please report to the P team or create a issue on GitHub, Thanks!>");
+            }
+        }
        
 
         /// <summary>
@@ -141,6 +169,20 @@ private DirectoryInfo GetOutputDirectory(FileInfo fullPathName)
                 return new DirectoryInfo(Directory.GetCurrentDirectory());
         }
 
+        /// <summary>
+        /// Parse the output directory information from the pproj file
+        /// </summary>
+        /// <param name="fullPathName"></param>
+        /// <returns>If present returns the output directory name, else the current directory name</returns>
+        private string GetOutputDirectoryName(FileInfo fullPathName)
+        {
+            var projectXml = XElement.Load(fullPathName.FullName);
+            if (projectXml.Elements("OutputDir").Any())
+                return projectXml.Element("OutputDir")?.Value;
+            else
+                return Directory.GetCurrentDirectory();
+        }
+
         private void GetTargetLanguage(FileInfo fullPathName, ref CompilerOutput outputLanguage, ref bool generateSourceMaps)
         {
             var projectXml = XElement.Load(fullPathName.FullName);
diff --git a/Src/PRuntimes/PSymRuntime/pom.xml b/Src/PRuntimes/PSymRuntime/pom.xml
index babef9d68..771df08c7 100644
--- a/Src/PRuntimes/PSymRuntime/pom.xml
+++ b/Src/PRuntimes/PSymRuntime/pom.xml
@@ -327,7 +327,7 @@
         <maven.compiler.target>11</maven.compiler.target>
         <log4j2.configurationFile>${project.basedir}/src/main/resources/log4j2.xml</log4j2.configurationFile>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-        <revision>1.0.11</revision>
+        <revision>1.1.1</revision>
 
         <deps.path>${project.basedir}/../../../Bld</deps.path>
 
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSearchScheduler.java
index 0a824a4e4..02644f8d5 100644
--- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSearchScheduler.java
+++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSearchScheduler.java
@@ -382,21 +382,25 @@ public void reportEstimatedCoverage() {
       SearchLogger.log(String.format("Distinct States Explored %d", totalDistinctStateCount));
     }
 
-    BigDecimal coverage = PSymGlobal.getCoverage().getEstimatedCoverage(22);
-    assert (coverage.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+    BigDecimal coverage22 = PSymGlobal.getCoverage().getEstimatedCoverage(22);
+    assert (coverage22.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+
+    BigDecimal coverage12 = PSymGlobal.getCoverage().getEstimatedCoverage(12);
 
     String coverageGoalAchieved = PSymGlobal.getCoverage().getCoverageGoalAchieved();
     if (isFinalResult && PSymGlobal.getResult().equals("correct for any depth")) {
       PSymGlobal.getCoverage();
+      coverage22 = CoverageStats.getMaxCoverage();
+      coverage12 = CoverageStats.getMaxCoverage();
       coverageGoalAchieved = CoverageStats.getMaxCoverageGoal();
     }
 
-    StatWriter.log("progress", String.format("%.22f", coverage));
+    StatWriter.log("progress", String.format("%.22f", coverage22));
     StatWriter.log("coverage-achieved", String.format("%s", coverageGoalAchieved));
 
     SearchLogger.log(
         String.format(
-            "Progress Guarantee       %.12f", PSymGlobal.getCoverage().getEstimatedCoverage(12)));
+            "Progress Guarantee       %.12f", coverage12));
     SearchLogger.log(String.format("Coverage Goal Achieved   %s", coverageGoalAchieved));
   }
 
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSearchScheduler.java
index 6af35ed3b..689c44eaa 100644
--- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSearchScheduler.java
+++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSearchScheduler.java
@@ -376,22 +376,26 @@ public void print_search_stats() {
   public void reportEstimatedCoverage() {
     PSymGlobal.getCoverage().reportChoiceCoverage();
 
-    BigDecimal coverage = PSymGlobal.getCoverage().getEstimatedCoverage(22);
-    assert (coverage.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+    BigDecimal coverage22 = PSymGlobal.getCoverage().getEstimatedCoverage(22);
+    assert (coverage22.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+
+    BigDecimal coverage12 = PSymGlobal.getCoverage().getEstimatedCoverage(12);
 
     String coverageGoalAchieved = PSymGlobal.getCoverage().getCoverageGoalAchieved();
     if (isFinalResult && PSymGlobal.getResult().equals("correct for any depth")) {
       PSymGlobal.getCoverage();
+      coverage22 = CoverageStats.getMaxCoverage();
+      coverage12 = CoverageStats.getMaxCoverage();
       coverageGoalAchieved = CoverageStats.getMaxCoverageGoal();
     }
 
-    StatWriter.log("progress", String.format("%.22f", coverage));
+    StatWriter.log("progress", String.format("%.22f", coverage22));
     StatWriter.log("coverage-achieved", String.format("%s", coverageGoalAchieved));
 
     if (PSymGlobal.getConfiguration().isIterative()) {
       SearchLogger.log(
               String.format(
-                      "Progress Guarantee       %.12f", PSymGlobal.getCoverage().getEstimatedCoverage(12)));
+                      "Progress Guarantee       %.12f", coverage12));
       SearchLogger.log(String.format("Coverage Goal Achieved   %s", coverageGoalAchieved));
     }
   }
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/CoverageStats.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/CoverageStats.java
index 314f03338..daceb8d3c 100644
--- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/CoverageStats.java
+++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/CoverageStats.java
@@ -28,6 +28,10 @@ public class CoverageStats implements Serializable {
 
   public CoverageStats() {}
 
+  public static BigDecimal getMaxCoverage() {
+    return BigDecimal.ONE;
+  }
+
   public static String getMaxCoverageGoal() {
     return "∞ 9s";
   }