Add Owicki-Gries annotations

Jenkinsfile.deploy_website

@@ -14,7 +14,6 @@ pipeline {
   tools {
     jdk 'JDK21'
     maven 'Maven 3.9.11'
-    maven 'Maven 3.9.11'
   }
   stages {
     stage('Checkout') {

releaseScripts/default/benchexec/concurrency-witness-validation.xml

@@ -1,13 +1,19 @@
 <?xml version="1.0"?>
 <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
 <benchmark tool="ultimateautomizer" timelimit="15 min" hardtimelimit="16 min" memlimit="8 GB" cpuCores="2">
-  <resultfiles></resultfiles>
+  <resultfiles>**/witness.yml</resultfiles>
+
 
   <option name="&#45;-full-output"/>
 
   <!-- serves as baseline to measure speedup when given witnesses -->
   <rundefinition name="verify" />
 
+  <rundefinition name="generate">
+    <option name="&#45;-traceabstraction.positions.where.we.compute.the.hoare.annotation">All</option>
+  </rundefinition>
+
+
   <!-- validation of witnesses generated by goblint -->
   <rundefinition name="validate-goblint-witnesses">
     <option name="&#45;-witness-type">correctness_witness</option>
@@ -17,6 +23,21 @@
     <option name="&#45;-validate">./goblint.2024-02-07_10-47-16.files/SV-COMP24_unreach-call/${taskdef_name}/witness.yml</option>
   </rundefinition>
 
+  <!-- validation of witnesses generated by ultimate -->
+  <rundefinition name="validate-ultimate-witnesses">
+    <option name="&#45;-witness-type">correctness_witness</option>
+    <option name="&#45;-witnessparser.only.consider.loop.invariants">false</option>
+
+    <!-- update path as needed -->
+    <option name="&#45;-validate">./concurrency-witness-validation.2024-02-20_11-21-23.files/generate/${taskdef_name}/witness.yml</option>
+  </rundefinition>
+
+
+  <tasks name="single">
+    <include>${benchmark_path}/../../../trunk/examples/svcomp/weaver/parallel-misc-2-unrolled-atomic.wvr.yml</include>
+    <propertyfile expectedverdict="true">${benchmark_path}/../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+  </tasks>
+
   <tasks name="ConcurrencySafety-Main-correct">
      <includesfile>${benchmark_path}/../../../trunk/examples/svcomp/ConcurrencySafety-Main.set</includesfile>
      <propertyfile expectedverdict="true">${benchmark_path}/../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>

releaseScripts/default/benchexec/concurrency.xml

@@ -1,8 +1,11 @@
 <?xml version="1.0" encoding="UTF-8" standalone="yes"?>
-<benchmark tool="ultimateautomizer" memlimit="8GB" timelimit="900" hardtimelimit="920" cpuCores="2">
-  <resultfiles></resultfiles>
+<benchmark tool="ultimateautomizer" memlimit="8GB" timelimit="600" hardtimelimit="620" cpuCores="2">
+  <resultfiles>*.yml</resultfiles>
 
-  <option name="--force-no-wrapper" />
+  <?ignore
+    <option name="--force-no-wrapper" />
+  ?>
+  <option name="--full-output" />
 
   <!-- === No Partial Order Reduction === -->
   <!-- ================================== -->
@@ -23,6 +26,28 @@
     <option name="-s">../../../trunk/examples/settings/gemcutter/None.epf</option>
   </rundefinition-->
 
+	<rundefinition name="Automizer_PN+OG">
+		<?ignore
+		  <option name="-s">../../../trunk/examples/settings/default/automizer/svcomp-Reach-32bit-Automizer_Default.epf</option>
+		?>
+
+		<option name="--icfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks">false</option>
+		<option name="--rcfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks">false</option>
+
+		<option name="--traceabstraction.automaton.type.used.in.concurrency.analysis">PETRI_NET</option>
+		<option name="--traceabstraction.owicki-gries.proof.computation.algorithm">LEGAL_FOCUS</option>
+
+		<option name="--witnessprinter.generate.graphml.witnesses">false</option>
+		<option name="--witnessprinter.generate.yaml.witnesses">true</option>
+		<option name="--witnessprinter.yaml.format.version">2.1</option>
+	</rundefinition>
+  <rundefinition name="AutomizerValidator">
+		<option name="--icfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks">false</option>
+		<option name="--rcfgbuilder.only.consider.context.switches.at.boundaries.of.atomic.blocks">false</option>
+
+    <option name="--witness-type">correctness_witness</option>
+    <option name="--validate">./results/concurrency.2026-05-04_12-55-51.files/Automizer_PN+OG/${taskdef_name}/witness.yml</option>
+  </rundefinition>
 
   <!-- === Cassez/Ziegler-style: single-shot up-front reduction, then normal verification === -->
   <!-- ====================================================================================== -->
@@ -478,6 +503,16 @@
   <!-- ==================================================== TASKS ==================================================== -->
   <!-- =============================================================================================================== -->
 
+  <tasks name="ogwitness-canary">
+    <include>../../../trunk/examples/svcomp/pthread-atomic/dekker.yml</include>
+    <propertyfile>../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+  </tasks>
+  <tasks name="ogwitness-atomic">
+    <include expectedverdict="true">../../../trunk/examples/svcomp/pthread-atomic/*.yml</include>
+    <exclude>../../../trunk/examples/svcomp/pthread-atomic/*-witness.yml</exclude>
+    <propertyfile>../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+  </tasks>
+
   <tasks name="POPL2023">
     <option name="-tc">../../../trunk/examples/toolchains/AutomizerBplInline.xml</option>
     <option name="&#45;-traceabstraction.dfs.order.used.in.por">LOOP_LOCKSTEP</option>

releaseScripts/default/benchexec/og-benchmark-generator.xml

@@ -0,0 +1,52 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<benchmark tool="ultimateautomizer" memlimit="8GB" timelimit="900" hardtimelimit="920" cpuCores="2">
+  <resultfiles>/storage/repos/ultimate/releaseScripts/default/UAutomizer-linux/*.ats</resultfiles>
+
+  <option name="--force-no-wrapper" />
+  <option name="-tc">../../../trunk/examples/toolchains/AutomizerCInline.xml</option>
+  <option name="-s">../../../trunk/examples/settings/automizer/concurrent/svcomp-Reach-32bit-Automizer_Default-noMmResRef-PN-NoLbe.epf</option>
+  <option name="--traceabstraction.positions.where.we.compute.the.hoare.annotation">All</option>
+  <option name="--cacsl2boogietranslator.behaviour.of.calls.to.undefined.functions">OVERAPPROXIMATE_BEHAVIOUR</option>
+
+  <rundefinition name="AutomizerPN-ReachSafety">
+    <tasks name="ConcurrencySafety-Main">
+      <includesfile>../../../trunk/examples/svcomp/Concurrency.set</includesfile>
+      <propertyfile expectedverdict="true">../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+    </tasks>
+  </rundefinition>
+
+  <rundefinition name="AutomizerPN-NoDataRace">
+    <tasks name="NoDataRace-Main">
+      <option name="&#45;-cacsl2boogietranslator.check.absence.of.data.races.in.concurrent.programs">true</option>
+      <option name="&#45;-cacsl2boogietranslator.check.unreachability.of.reach_error.function">false</option>
+
+      <includesfile>../../../trunk/examples/svcomp/Concurrency.set</includesfile>
+      <propertyfile expectedverdict="true">../../../trunk/examples/svcomp/properties/no-data-race.prp</propertyfile>
+    </tasks>
+  </rundefinition>
+
+  <rundefinition name="AutomizerPN-MemSafety">
+    <tasks name="ConcurrencySafety-MemSafety">
+      <option name="--cacsl2boogietranslator.check.unreachability.of.reach_error.function">false</option>
+      <option name="--cacsl2boogietranslator.pointer.base.address.is.valid.at.dereference">CHECK</option>
+      <option name="--cacsl2boogietranslator.pointer.to.allocated.memory.at.dereference">CHECK</option>
+      <option name="--cacsl2boogietranslator.check.array.bounds.for.arrays.that.are.off.heap">CHECK</option>
+      <option name="--cacsl2boogietranslator.check.if.freed.pointer.was.valid">true</option>
+      <option name="--cacsl2boogietranslator.adapt.memory.model.on.pointer.casts.if.necessary">true</option>
+
+      <includesfile>../../../trunk/examples/svcomp/Concurrency.set</includesfile>
+      <propertyfile expectedverdict="true">../../../trunk/examples/svcomp/properties/valid-memsafety.prp</propertyfile>
+    </tasks>
+  </rundefinition>
+
+  <rundefinition name="AutomizerPN-NoOverflow">
+    <tasks name="ConcurrencySafety-NoOverflow">
+      <option name="--cacsl2boogietranslator.check.unreachability.of.reach_error.function">false</option>
+      <option name="--cacsl2boogietranslator.check.absence.of.signed.integer.overflows">CHECK</option>
+
+      <includesfile>../../../trunk/examples/svcomp/Concurrency.set</includesfile>
+      <propertyfile expectedverdict="true">../../../trunk/examples/svcomp/properties/no-overflow.prp</propertyfile>
+    </tasks>
+  </rundefinition>
+
+</benchmark>

releaseScripts/default/benchexec/og-proof-generation.xml

@@ -0,0 +1,80 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<benchmark tool="shell" memlimit="8GB" timelimit="300" hardtimelimit="320">
+  <resultfiles></resultfiles>
+
+  <option name="success">1 tests successful</option>
+  <option name="failure">1 tests failed</option>
+
+  <rundefinition name="ModularLegalFocusOG-WithAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$ModularLegalFocusOG ${inputfile_name} true</option>
+  </rundefinition>
+
+  <rundefinition name="ModularLegalFocusOG-NoAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$ModularLegalFocusOG ${inputfile_name} false</option>
+  </rundefinition>
+
+  <rundefinition name="ModularLegalFocusOG-Validate">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1 -DOwickiGries.Validate=true' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$ModularLegalFocusOG ${inputfile_name} false</option>
+  </rundefinition>
+
+
+  <rundefinition name="GlobalLegalFocusOG-WithAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$GlobalLegalFocusOG ${inputfile_name} true</option>
+  </rundefinition>
+
+  <rundefinition name="GlobalLegalFocusOG-NoAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$GlobalLegalFocusOG ${inputfile_name} false</option>
+  </rundefinition>
+
+  <rundefinition name="GlobalLegalFocusOG-Validate">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1 -DOwickiGries.Validate=true' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$GlobalLegalFocusOG ${inputfile_name} false</option>
+  </rundefinition>
+
+
+  <rundefinition name="EmpireAutomatonOG-WithAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$EmpireAutomatonOG ${inputfile_name} true</option>
+  </rundefinition>
+
+  <rundefinition name="EmpireAutomatonOG-NoAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$EmpireAutomatonOG ${inputfile_name} false</option>
+  </rundefinition>
+
+  <rundefinition name="EmpireAutomatonOG-Validate">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1 -DOwickiGries.Validate=true' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$EmpireAutomatonOG ${inputfile_name} false</option>
+  </rundefinition>
+
+
+  <rundefinition name="NaiveOG-WithAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$NaiveOG ${inputfile_name} true</option>
+  </rundefinition>
+
+  <rundefinition name="NaiveOG-NoAssert">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$NaiveOG ${inputfile_name} false</option>
+  </rundefinition>
+
+  <rundefinition name="NaiveOG-Validate">
+    <option name="command">env JAVA_TOOL_OPTIONS='-DOwickiGries.Timeout=-1 -DOwickiGries.Validate=true' ${benchmark_path}/../run-test.sh Library-ProofsTest de.uni_freiburg.informatik.ultimate.lib.proofs.owickigries.OGProofProducerTest$NaiveOG ${inputfile_name} false</option>
+  </rundefinition>
+
+
+  <tasks name="SVBenchmarks-ConcurrencySafety">
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/ReachSafety.*.ats</include>
+  </tasks>
+
+  <tasks name="SVBenchmarks-MemSafety">
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/MemSafety.*.ats</include>
+  </tasks>
+
+  <tasks name="SVBenchmarks-NoDataRace">
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/NoDataRace.*.ats</include>
+  </tasks>
+
+  <tasks name="SVBenchmarks-NoOverflow">
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/NoOverflow.*.ats</include>
+  </tasks>
+
+  <tasks name="canary">
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/separate-threads*.ats</include>
+    <include>../../../trunk/examples/concurrent/OwickiGries/PetriPrograms/ReachSafety.test-*.ats</include>
+  </tasks>
+</benchmark>