From 1af37fb7dbcb0a1c30c83d6c3010fe78f852188c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 23:00:02 +0100 Subject: [PATCH 1/3] Minor Changes --- _layouts/default.html | 2 +- pages/resources.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/_layouts/default.html b/_layouts/default.html index 8ee9fe0..5eff81a 100644 --- a/_layouts/default.html +++ b/_layouts/default.html @@ -20,7 +20,7 @@ {% include components/header.html %}
{% include components/breadcrumbs.html %} -
+
{% if site.heading_anchors != false %} {% include vendor/anchor_headings.html html=content beforeHeading="true" anchorBody="" anchorClass="anchor-heading" anchorAttrs="aria-labelledby=\"%html_id%\"" %} diff --git a/pages/resources.md b/pages/resources.md index f256691..9d2a206 100644 --- a/pages/resources.md +++ b/pages/resources.md @@ -14,7 +14,7 @@ description: Find LiquidJava papers, posters, and source repositories for deeper ## Posters -- [Usability-Oriented Design of Liquid Types for Java](https://icse2023.paperlessevents.com.au/share/Gamboa-85), ICSE 2023 Digital Poster Session +- [Usability-Oriented Design of Liquid Types for Java](https://conf.researchr.org/details/icse-2023/icse-2023-technical-track/142/Usability-Oriented-Design-of-Liquid-Types-for-Java), ICSE 2023 Poster Session - [LiquidJava: Adding Lightweight Verification to Java](https://catarinagamboa.github.io/assets/docs/poster_LiquidJava.pdf), INForum 2021 - [Improving the Usability of LiquidJava](https://rcosta358.github.io/improving_the_usability_of_liquidjava.pdf), 11th LASIGE Workshop Poster Session - [Barista: Synthesizing Typestate Specifications with LLM Agents](https://rcosta358.github.io/barista.pdf), 11th LASIGE Workshop Poster Session From 34535023f4d3e3d354297cffaf99664aabbeb9bc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 14:45:42 +0100 Subject: [PATCH 2/3] Document SMT unknown errors Co-authored-by: Codex --- pages/diagnostics/errors.md | 1 + 1 file changed, 1 insertion(+) diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md index d3e7e4c..a9bd07b 100644 --- a/pages/diagnostics/errors.md +++ b/pages/diagnostics/errors.md @@ -14,6 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot | --- | --- | | `RefinementError` | A refinement was violated or could not be proven | | `StateRefinementError` | A state refinement was violated or could not be proven | +| `SMTUnknownError` | The solver could not determine whether a refinement holds; the diagnostic includes the reason as a hint | | `NotFoundError` | An element used in a refinement could not be found | | `SyntaxError` | The syntax used in a refinement is invalid | | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments | From 0c9ef85d3321dd7a3e5fcfbef5095b026cf64dfb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 14:49:03 +0100 Subject: [PATCH 3/3] Minor Change --- pages/diagnostics/errors.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md index a9bd07b..e38300e 100644 --- a/pages/diagnostics/errors.md +++ b/pages/diagnostics/errors.md @@ -14,7 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot | --- | --- | | `RefinementError` | A refinement was violated or could not be proven | | `StateRefinementError` | A state refinement was violated or could not be proven | -| `SMTUnknownError` | The solver could not determine whether a refinement holds; the diagnostic includes the reason as a hint | +| `SMTUnknownError` | The solver could not determine whether a refinement holds | | `NotFoundError` | An element used in a refinement could not be found | | `SyntaxError` | The syntax used in a refinement is invalid | | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments |