javapathfinder · syheliel · Oct 15, 2021 · Nov 22, 2021 · Nov 23, 2021 · Nov 23, 2021
diff --git a/Google-Summer-of-Code.md b/Google-Summer-of-Code.md
@@ -1,10 +1,10 @@
 ## Google Summer of Code ##
 The JPF project has participated in the Google Summer of Code for a number of years. More details can be found [here](https://summerofcode.withgoogle.com/).
 
-# [[GSoC 2021 Project Ideas]]
+# [[GSoC 2023 Project Ideas]]
 
 A list of ideas (not exhaustive); other ideas are welcome.
 
-# [[JPF Google Summer of Code 2021]]
+# [[JPF Google Summer of Code 2023]]
 
 An overview of GSoC and JPF's aims for this summer.
diff --git a/Home.md b/Home.md
@@ -1,5 +1,5 @@
-# <img src="https://ti.arc.nasa.gov/m/events/jpf-workshop-2012/swissarmy.png" width="84" height="84"> Java Pathfinder 
-This is the main page for Java™ Pathfinder (JPF). JPF is an extensible software model checking framework for Java™ bytecode programs. The system was developed at the [NASA Ames Research Center](http://arc.nasa.gov), open sourced in 2005, and is freely available on this server under the [Apache-2.0 license](http://www.apache.org/licenses/LICENSE-2.0).
+# <img src="https://avatars.githubusercontent.com/u/23702826?s=280&v=4" width="84" height="84"> Java Pathfinder 
+This is the main page for Java™ Pathfinder (JPF). JPF is an extensible software model checking framework for Java™ bytecode programs. The system was developed at the [NASA Ames Research Center](https://www.nasa.gov/centers/ames/about/index.html), open sourced in 2005, and is freely available on this server under the [Apache-2.0 license](http://www.apache.org/licenses/LICENSE-2.0).
 
 ---
 
@@ -45,14 +45,26 @@ This is the main page for Java™ Pathfinder (JPF). JPF is an extensible softwar
 * [JPF core project](JPF-core) - description and link to jpf-core
 * [Projects](Projects) - link to currently active and legacy extensions of JPF
 * [Workshops](JPF-Workshops) - link to annual workshops on JPF
-* [Google Summer of Code](Google-Summer-of-Code) - link to JPF's participation in the Google Summer of Code program, current ideas page [here](GSoC-2021-Project-Ideas). 
+* [Google Summer of Code](Google-Summer-of-Code) - link to JPF's participation in the Google Summer of Code program, current ideas page [here](GSoC-2023-Project-Ideas). 
 * [Mailing list](https://groups.google.com/forum/#!forum/java-pathfinder) - discussion about JPF takes place in Google Groups [JPF Google Group](https://groups.google.com/forum/#!forum/java-pathfinder)
+* [Discord](https://discord.gg/sX4YZUVHK7) - join our [Discord server](https://discord.gg/sX4YZUVHK7) for more discussions
 <!--* [Related research and publications](Related-publications)-->
 
 ---
-
+<!--*  02/08/2025 [GSoC 2025](https://summerofcode.withgoogle.com): The JPF team will apply again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](https://github.com/javapathfinder/jpf-core/wiki/JPF-Google-Summer-of-Code-2025) page.-->
+
+<<<<<<< HEAD
+#### Latest JPF News
+*  02/28/2025 [GSoC 2025](https://summerofcode.withgoogle.com): The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](https://github.com/javapathfinder/jpf-core/wiki/JPF-Google-Summer-of-Code-2025) page.
+*  02/23/2024 [GSoC 2024](https://summerofcode.withgoogle.com): The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](https://github.com/javapathfinder/jpf-core/wiki/JPF-Google-Summer-of-Code-2024) page.
+*  07/21/2022 JPF is now on [Twitter](https://twitter.com/Java_Pathfinder)! Follow us and check out our feed for the latest news and updates.
+*  05/13/2022 [JPF Workshop 2022](https://github.com/javapathfinder/jpf-core/wiki/Java-Pathfinder-Workshop-2022) will be co-located with [ASE 2022](https://conf.researchr.org/track/ase-2022/ase-2022-workshops) in the Oakland Center, Michigan, United States. Please consider submitting a paper.
+*  03/09/2022 [GSoC 2022](https://summerofcode.withgoogle.com): The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](JPF-Google-Summer-of-Code-2022) page.
+*  11/23/2021 [JPF 2021](https://github.com/javapathfinder/jpf-core/wiki/JPF-Day-2021-(Online)): The JPF team organizes a virtual JPF day this year! Check our [call for participation](https://github.com/javapathfinder/jpf-core/wiki/JPF-Day-2021-(Online)).
+=======
 #### Latest JPF News 
 *  22/02/2023 [GSoC 2023](https://developers.google.com/open-source/gsoc/): The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](JPF-Google-Summer-of-Code-2023) page.
+>>>>>>> 49e2db116830c9aee80800731dc274749702c58a
 *  03/09/2021 [GSoC 2021](https://developers.google.com/open-source/gsoc/): The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the [JPF/GSoC](JPF-Google-Summer-of-Code-2021) page.
 *  02/21/2020 The JPF team has been accepted to the [GSoC](https://developers.google.com/open-source/gsoc/) program for 2020! To learn more, please visit the [JPF/GSoC](JPF-Google-Summer-of-Code-2020) page.
 *  07/24/2019 [JPF Workshop 2019](https://2019.ase-conferences.org/home/jpf-2019). The workshop will be co-located with [ASE](https://2019.ase-conferences.org/) in San Diego, CA.
@@ -65,11 +77,11 @@ This is the main page for Java™ Pathfinder (JPF). JPF is an extensible softwar
 *  06/01/2016 [JPF Workshop 2016](JPF-Workshop-2016) will be co-located with [FSE 2016](http://www.cs.ucdavis.edu/fse2016/) in Seattle, WA, on November 18, 2016. Please consider submitting a paper.
 *  04/22/2016 JPF student proposals accepted for GSoC 2016 [announced](https://summerofcode.withgoogle.com/organizations/5791763432210432/#projects) - Congratulations to the students!
 *  02/29/2016 JPF got accepted for [GSoC 2016](https://summerofcode.withgoogle.com/organizations/5791763432210432/). Please visit our [ideas page](Google-Summer-of-Code-2016-Project-Ideas), and let us know if you would like to propose a project.
-*  17/08/2015 JPF Workshop 2015 Accepted Papers are announced. Please visit [ASE 2015](http://ase2015.unl.edu) for registration, date and venue information. 
-*  10/03/2014 JPF Workshop 2014 [Accepted Papers](JPF-Workshop-2014-Accepted-Papers). Please visit [SOAR Lab](http://soarlab.org/events/jpf2014/) for registration, date and venue information. 
 <details close>
 <summary>Old news</summary>
 <ul>
+<li>17/08/2015 JPF Workshop 2015 Accepted Papers are announced. Please visit <a href="http://ase2015.unl.edu">ASE 2015</a> for registration, date and venue information.</li> 
+<li>10/03/2014 JPF Workshop 2014 <a href="https://github.com/javapathfinder/jpf-core/wiki/JPF-Workshop-2014-Accepted-Papers">Accepted Papers</a>. Please visit <a href="http://soarlab.org/events/jpf2014/">SOAR Lab</a> for registration, date and venue information.</li> 
 <li>10/01/2013 JPF Workshop 2013 <a href="JPF-Workshop-2013-Accepted-Papers">Accepted Papers</a>. Please note <a href="http://ti.arc.nasa.gov/events/jpf-workshop-2013">JPF Workshop 2013</a> website is down due to the shutdown, please visit <a href="http://ase2013.org">ASE 2013</a> for registration, date and venue information.</li>
 
 <li>06/20/2013 <a href="http://ti.arc.nasa.gov/events/jpf-workshop-2013/">JPF Workshop 2013</a> will be co-located with <a href="http://ase2013.org">ASE 2013</a> Please submit papers.<\li>

diff --git a/JPF-Day-2021-(Online).md b/JPF-Day-2021-(Online).md
@@ -0,0 +1,98 @@
+<!-- JPF 2021 - December 4 - *online*-->
+
+<!--## Call for participation-->
+
+Since 2008, ten times the _Java PathFinder (JPF)_ workshop has been organized. Given the current pandemic, as in 2020 also this year we will organize a **JPF day** instead. On **Saturday, December 4**, a Zoom session will be held (15:00-17:45 UTC).
+
+## Schedule
+
+All times are in UTC.
+
+<table>
+   <tr>
+      <td>15:00 - 15:10</td>
+      <td>Opening</td>
+   </tr>
+   <tr>
+      <td>15:10 - 15:55</td>
+      <td>Invited Talk: Divya Gopinath<br>
+      <i>Constraint-based repair of neural network classifiers</i></td>
+   </tr>
+   <tr>
+      <td>15:55 - 16:00</td>
+      <td>Short break</td>
+   </tr>
+   <tr>
+      <td>16:00 - 16:05</td>
+      <td>GSoC’2021 Overview and Results</td>
+   </tr>
+   <tr>
+      <td>16:05 - 16:25</td>
+      <td>Pu Yi, Pavel Parizek, Cyrille Artho<br>
+      <i>Systematic Bit-Flip Fault Injection and Exploration using Java PathFinder</i></td>
+   </tr>
+   <tr>
+      <td>16:25 - 16:45</td>
+      <td>Parssa Khazra, Anto Nanah Ji, Matt Walker, Hongru Wang, Franck van Breugel<br>
+      <i>jpf-ctl: CTL Model Checking of Java Code</i></td>
+   </tr>
+   <tr>
+      <td>16:45 - 17:05</td>
+      <td>Ward Muylaert, Coen De Roover<br>
+      <i>Detecting Semantic Merge Conflicts with Symbolic Execution</i></td>
+   </tr>
+   <tr>
+      <td>17:05 - 17:45</td>
+      <td>Closing Panel Discussion</td>
+   </tr>
+</table>
+
+## Participation
+
+For those interested in participating, please send an email to [[email protected]](mailto:[email protected]) with the subject JPF 2021. The receipt of your email will be acknowledged and the Zoom details will be emailed to you one day in advance of the meeting.
+
+Additionally, we encourage you to join the official [JPF Day 2021 discord server](https://discord.gg/dQvmMYkd8u) where you can engage in project-specific discussions with the authors, ask JPF-related questions, or just hang out during the event. We hope to see you there!
+
+<!--
+## Call for presentations
+
+Since 2008, ten times the *Java PathFinder (JPF) workshop* has been
+organized. Given the current pandemic, as in 2020 also this year we
+will organize a **JPF day** instead. On **Saturday, December 4**, two Zoom
+sessions will be held (11:00-13:00 UTC and 17:00-19:00 UTC).
+
+For the JPF day, we solicit presentations on research and applications
+related to JPF and its extensions, including work in progress. If the
+underlying research idea has been presented in another venue, the
+one-page abstract needs to clarify the novel aspects that are being
+presented. We also welcome comparative analysis presentations that
+evaluate algorithms in JPF or its extensions with other relevant tools.
+The goal of the JPF day is to encourage the flow of ideas relevant to
+JPF and Java (byte)code analysis in general.
+
+Topics of interest include the following:
+* JPF extensions or tools
+* JPF case studies
+* Position papers on JPF, such as future directions
+* Java (byte)code analysis or verification
+* General software verification and symbolic execution techniques or
+tools
+
+## Submissions
+
+Submit a one-page abstract to [[email protected]](mailto:[email protected]) by 
+**Friday, November 13**.
+
+## Presentations
+
+Each accepted presenter will get assigned a 15 minutes slot, 5-10
+minutes presentation (leaving the exact length up to the presenter), and
+the remainder for questions and discussion. Preference for the early or
+late session will be taken into account, but cannot be guaranteed.The
+presentation can be either recorded in advance or live.
+-->
+
+## Organizers
+
+* [Yannic Noller](https://yannicnoller.github.io), National University of Singapore
+* [Franck van Breugel](http://www.cse.yorku.ca/~franck/index.shtml), York University, Toronto
diff --git a/Java-Pathfinder-Workshop-2022.md b/Java-Pathfinder-Workshop-2022.md
@@ -0,0 +1,112 @@
+The goal of the workshop is to highlight current research and tools development for Java/Android program verification and analysis. Although the workshop’s theme revolves around the JPF tool, e.g., use of JPF to support basic research, tool development, or in verification case studies, we also welcome contributions related to program analysis of Java/Android applications. The workshop will serve as a platform to grow the community of researchers, foster collaboration and define future directions for JPF development and Java/Android program analysis research.
+
+> Check our [Twitter](https://twitter.com/Java_Pathfinder) account for the latest news and updates!
+
+## Page Content
+
+* [Accepted Papers](#Accepted-Papers)
+* [Workshop Program](#Workshop-Program)
+* [Participation](#Participation)
+* [Call for Submissions](#Call-for-Submissions)
+* [Important Dates](#important-dates-in-aoe-warning)
+* [Organizers](#Organizers)
+* [Program Committee](#Program-Committee)
+* [Contact](#Contact)
+
+## Accepted Papers
+
+* **Using Theia Traceviewer to Visualize JPF Traces**<br>*Johan Besseling and Cyrille Artho*
+* **Towards Wider Support for Java String Functions**<br>*Qiuchen Yan, Cyrille Artho and Pavel Parizek*
+* **Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs**<br>*Pavel Parizek and Filip Kliber*
+* **jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code**<br>*Matt Walker, Parssa Khazra, Anto Nanah Ji, Hongru Wang and Franck van Breugel*
+
+## Workshop Program
+*(all times are in the local timezone: Eastern Daylight Time, i.e., UTC-4)*
+
+Start | End | Agenda Item
+--- | --- | :---
+09:00 | 09:15 | Welcome
+09:15 | 10:00 | **Invited talk: "Eclipse Foundation: Enabling Open, Vendor Neutral Collaboration"**<br>John Kellerman (Cloud Development Tools Program Manager, Eclipse Foundation)<br>→ [recording](https://youtu.be/tt40pqLjXQE)
+*10:00* | *10:30* | *Coffee break*
+10:30 | 10:45 | **Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs**<br>Pavel Parizek and Filip Kliber
+10:45 | 11:00 | **Using Theia Traceviewer to Visualize JPF Traces**<br>Johan Besseling and Cyrille Artho
+11:00 | 12:00 | **Tutorial: Java PathFinder**<br>Cyrille Artho (KTH Royal Institute of Technology)<br>→ [recording](https://youtu.be/KnN7HkV1iPM)
+*12:00* | *13:30* | *Lunch*
+13:30 | 14:15 | **Invited talk: "Virtual threads: scalable, harmonious concurrency"**<br>Ron Pressler (Developer in the Java Platform Group, Oracle)<br>→ [recording](https://youtu.be/3BzKf7XvqKM)
+14:15 | 14:30 | **jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code**<br>Matt Walker, Parssa Khazra, Anto Nanah Ji, Hongru Wang and Franck van Breugel
+14:30 | 14:45 | **Towards Wider Support for Java String Functions**<br>Qiuchen Yan, Cyrille Artho and Pavel Parizek
+14:45 | 15:00 | **Gradle support for Symbolic PathFinder**<br>Gaurang Kudale
+*15:00* | *15:30* | *Coffee break*
+15:30 | 16:30 | **Tutorial: Symbolic PathFinder**<br>Corina Pasareanu (CMU, NASA Ames)<br>→ [recording](https://youtu.be/4NJW1Q_ASuY)
+16:30 | 17:00 | Open Discussion
+*18:00* | | *Dinner*
+
+
+## Participation
+We invite practitioners, academics, and students who are interested in Java development, automated program analysis, and related software engineering research and practice to attend the JPF workshop. Submitting a paper is not required to participate, enjoy, and learn about JPF. The workshop will be co-located with [ASE 2022](https://conf.researchr.org/track/ase-2022/ase-2022-workshops) in [Oakland Center, Michigan, United States](https://conf.researchr.org/venue/ase-2022/ase-2022-venue).
+
+
+While we want to encourage all participants to join on-site in the Oakland Center, we want to highlight that the **JPF workshop will be held as a hybrid event**. This also means that authors are not necessarily required to present in person but can also present virtually.
+
+## Call for Submissions
+We solicit regular paper submissions on existing research and applications related to JPF or its extensions, as well as topics on Java/Android static analysis. We welcome comparative analysis papers that evaluate algorithms in JPF or its extensions with other relevant tools. If the underlying research idea has been published in another venue, authors need to clarify the novel aspects that are being presented in their papers. We also solicit extended abstracts and position papers on recent or in progress work. Submissions should be at most 5 pages long (including references) in the [ACM SIGSOFT SEN format](https://www.sigsoft.org/SEN/subpub.html). The extended abstracts and position paper should be at most 2-pages (including references). Accepted regular papers will be published in the Software Engineering Notes (SEN) and the ACM digital library.
+
+Topics of interest include the following:
+* JPF extensions or tools
+* JPF case studies
+* Position papers on JPF, such as future directions
+* Java program analysis or verification
+* Android program analysis or verification
+* General software verification techniques or tools
+
+All papers must be submitted electronically through the JPF 2022 EasyChair submission site: https://easychair.org/conferences/?conf=jpf2022. All submissions must be in English.
+
+## Important Dates (in AoE) :warning:
+<table>
+  <tbody>
+    <tr>
+      <td><b>Submission</b>:</td>
+      <td>Friday, <s>July 29, 2022</s> <b>August 5, 2022</b> :point_left:</td>
+    </tr>
+    <tr>
+      <td><b>Notification</b>:</td>
+      <td>Wednesday, <s>August 24, 2022</s> <b>August 31, 2022</b></td>
+    </tr>
+    <tr>
+      <td><b>Final Version</b>:</td>
+      <td>Friday, <s>September 2, 2022</s> <b>September 9, 2022</b></td>
+    </tr>
+    <tr>
+      <td><b>Workshop day</b>:</td>
+      <td>Monday, October 10, 2022</td>
+    </tr>
+  </tbody>
+</table>
+
+<!-- Bidding: Tuesday, August, 2 -->
+<!-- Assignments: Wednesday, August, 3 -->
+<!-- Review: August, 4-19 -->
+<!-- Discussion: August, 20-22 -->
+
+## Organizers
+* [Elena Sherman](http://cs.boisestate.edu/~esherman/), Boise State University
+* [Yannic Noller](https://comp.nus.edu.sg/~yannic), National University of Singapore
+
+## Program Committee
+* [Cyrille Artho](https://people.kth.se/~artho/), KTH Royal Institute of Technology
+* [Franck van Breugel](http://www.cse.yorku.ca/~franck/), York University
+* [Antonio Filieri](https://www.antonio.filieri.name), Imperial College London
+* [Milos Gligoric](https://users.ece.utexas.edu/~gligoric/), University of Texas at Austin
+* [Falk Howar](https://ls14-www.cs.tu-dortmund.de/cms/de/mitarbeiter/profs/Howar.html), TU Dortmund
+* [Xuan-Bach D. Le](https://xuanbachle.github.io), University of Melbourne
+* [Thanh Vu H. Nguyen](https://nguyenthanhvuh.github.io), George Mason University
+* [Pavel Parizek](https://d3s.mff.cuni.cz/people/pavelparizek/), Charles University
+* [Corina Pasareanu](https://www.cylab.cmu.edu/directory/bios/pasareanu-corina.html), NASA Ames and CMU
+* [Sang Phan](https://research.facebook.com/people/phan-sang/), Meta
+* [Vaibhav Sharma](https://sites.google.com/view/vaibhavbsharma/home), Amazon
+* [Arnaud Venet](https://dblp.org/pid/59/4227.html), Meta
+* [Guowei Yang](https://guoweiyang.github.io), University of Queensland
+
+## Contact
+* Email: [[email protected]](mailto:[email protected])
+* Twitter: [https://twitter.com/Java_Pathfinder](https://twitter.com/Java_Pathfinder)
diff --git a/devel/Writing-JPF-tests.md → Writing-JPF-tests.md b/devel/Writing-JPF-tests.md → Writing-JPF-tests.md
@@ -1,9 +1,9 @@
 As a complex runtime system for (almost) arbitrary Java programs, it goes without saying that JPF needs a lot of regression tests. You can find these under the `src/tests` directories in (hopefully) all JPF projects. All tests follow the same scheme, which is motivated by the need to run tests in a number of different ways:
 
-  1. as part of the Ant-based build system, i.e. from build.xml
-  1. as explicitly invoked JUnit tests
-  1. by directly running JPF on the test application (i.e. without JUnit, either as a JPF `shell` or via RunTest.jar)
-  1. by running the test application on a normal JVM
+  1. as part of the Gradle-based build system, as configures in `build.gradle`;
+  1. as explicitly invoked JUnit tests;
+  1. by directly running JPF on the test application (i.e. without JUnit, either as a JPF `shell` or via RunTest.jar);
+  1. by running the test application on a normal JVM.
 
 The rationale for this is to support various levels of inspection and debugging. 
 
@@ -144,3 +144,4 @@ Typically, JPF tests are only executed from within an IDE if they fail and need
 Under NetBeans, this can be done by selecting the test class, and then executing the *Debug File* command from the context menu. This will pop up a dialog that lets you enter a specific test method to debug. This method requires a properly set up ide-file-target.xml, which comes with most JPF projects.
 
 Under Eclipse, you can select the test class and then execute **Debug As..** -> **Java Application**.
+