Pith. sign in

REVIEW 4 major objections 4 minor 52 references

On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability

T0 review · 4 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A hybrid LLM-and-scenario-based workflow produced a Connect4 agent that defeated three online opponents and is provably winning from six fixed openings.

desk verdict Honest and structured LLM+SBP case study with real partial verification, but the 'beats strong opponents' claim sits on uncalibrated online baselines. read the letter →

arxiv 2509.09194 v1 pith:AH72FUNY submitted 2025-09-11 cs.SE cs.AI

Ayelet Berzack , Guy Katz This is my paper
classification cs.SEcs.AI
keywords LargeLanguageModelsScenario-BasedProgrammingLLMcodegenerationformalverificationmodelcheckingbehavioralsoftwarereliabilityConnect4
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that LLM-generated code can be made reliable if a human decomposes the system into small scenario objects and feeds them to the model one at a time, under a review-refine-verify loop, using Scenario-Based Programming as the structuring paradigm. The authors test this by building a Connect4 agent: the LLM translated natural-language scenario descriptions into working scenario objects, and the finished agent won every match against three publicly available Connect4 programs. They also formally verified, with an explicit model checker, that the agent is guaranteed to win from six fixed opening sequences. If the methodology holds, it offers a path to use LLMs in correctness-critical software without giving up formal checks.

What carries the argument

Scenario-Based Programming (SBP), a paradigm where a system's behavior is specified as concurrent scenario objects (b-threads) that request, wait for, or block events at synchronization points. The paper's central extension is event-specific priorities: each request and block can carry a numerical priority, with infinity as hard blocking and finite values as soft blocking, implemented through multi-sync statements. This machinery carries the argument because it keeps the LLM's contributions small and independently inspectable, and it gives the human a way to encode strategic trade-offs that standard blocking semantics cannot express.

What would settle it

Run a known-strong or perfect Connect4 solver against the three online opponents used as benchmarks; if any opponent loses to a simple heuristic, the claim that defeating them shows state-of-the-art performance collapses. Separately, replay any of the six formally verified opening sequences with a fresh referee—if red ever wins from one, the verification claim is false.

Watch

Extended reading notes

Core claim

At the center of the paper is a workflow: state the system's rules and strategies as discrete scenario objects, teach the LLM the SBP paradigm, then query it to generate one scenario object at a time, inspect and refine each output, and verify key properties with model checking. Applied to Connect4, this produced an agent (playing yellow) that beat three online AI opponents in all test games, and a model checker proved the agent wins from six constrained openings against any red replies. To make the approach work, the authors extended SBP with per-event priorities and soft blocking—an event can be blocked with a finite priority and still fire if requested with higher priority—which lets stra

Load-bearing premise

The results depend on the three online opponents being genuinely strong Connect4 programs; the paper provides no measurement of their strength.

Editorial extensions

If this is right

  • Following the workflow, LLM-generated code for reactive systems can be produced in small verifiable increments rather than as one opaque whole.
  • The event-priority extension gives SBP a general mechanism for soft constraints and trade-offs, potentially useful outside games in any system that must balance conflicting event requests.
  • Using 'scenarios as regression tests'—forcing a trace by blocking other events—gives a low-cost way to lock in fixes found during verification.
  • Partial formal verification from restricted starting states can provide meaningful guarantees for LLM-built agents when full state-space verification is infeasible.
  • The iterative query-review-refine loop was workable with a clear learning curve, suggesting the methodology's main cost is up-front scenario decomposition, not the LLM interaction itself.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: the same one-module-at-a-time, verify-as-you-go pattern could be layered onto other modular paradigms (e.g., actor models or plugin architectures), not just SBP; a direct test would apply the workflow to a second domain such as a robot controller.
  • A reader-level inference: the strength of the three benchmark opponents is unmeasured; if they are not actually strong, the headline performance claim reduces to the narrower, still meaningful, formal guarantees on the six openings.
  • The six verified openings could serve as a reusable benchmark suite for future LLM-generated Connect4 agents, enabling head-to-head comparison of correctness rather than only win rates.
  • The priority-extension semantics suggests a more general design principle: when LLMs generate code, allowing 'soft' overrides that are explicit and numerically ordered may be safer than hard static blocks, because verification can then check the ordering constraints.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper proposes a methodology for integrating LLM-based code generation with Scenario-Based Programming (SBP), aiming to make LLM-generated software more reliable through modular, human-guided development and formal verification. The methodology is evaluated on a Connect4 case study: the resulting agent plays yellow, was tested against three online opponents, and was partially verified with BPpy's explicit model checker. The paper reports wins against all three opponents, formal guarantees that the agent wins from six fixed opening configurations, and a qualitative assessment of the developer experience. It also introduces extensions to SBP (event-specific request/block priorities and multi-sync statements) that were motivated by the case study. The authors are careful to state that the agent is not perfect and that verification is partial.

Significance. If the results are valid, the paper makes a modest but useful contribution: it demonstrates a concrete workflow where SBP modularity helps an LLM build a non-trivial system and where at least some properties of the resulting agent can be formally checked. The formal verification results, though limited to six hand-picked openings, are concrete and falsifiable, and the authors deserve credit for bounding their correctness claims. The proposed SBP extensions are also interesting, though their semantics are not fully formalized. However, the performance claim that the agent is 'highly-capable' and 'comparable with state-of-the-art' is not supported by the evaluation as presented: the online opponents are not measured, the sample size is tiny, and the agent always plays as the first player, who has a known theoretical advantage in Connect4. The paper's significance therefore rests mainly on the methodology narrative and the narrow formal guarantees, not on the demonstrated competitive strength.

major comments (4)
  1. [Section 5.1, RQ2] The claim that the agent 'repeatedly defeat[s] advanced opponents' and achieves results 'comparable with state-of-the-art solutions' is not supported by the evidence. The three opponents are described only as 'strong, AI-based opponents available online'; no objective measure of their strength is given. One opponent is explicitly noted to merely 'boldly claim the title' 'Unbeatable AI'. Playing as the first player (yellow) in Connect4 is a significant advantage, since the first player can force a win with perfect play. To substantiate RQ2, the authors should benchmark against known-strength agents, e.g., a well-studied solver or a range of minimax agents with varying depths, and report win/loss/draw statistics over many games, ideally with the agent also playing as red. Without this, the abstract's 'defeat various strong existing agents' overstates what the 12 games show.
  2. [Section 5.2] The six fixed opening sequences used for formal verification appear to be selected because they match the agent's own strategies: the text explicitly states that the sequences are 'quite plausible in a real match' and 'occurs in practice due to our agent's strategies'. This is a selection bias: the verification shows that the agent wins from states that the developers already believed were favorable and that the agent's own heuristics tend to reach. It does not show that the agent reliably creates such states or that it is generally strong. The authors should clearly separate the existence of verified winning states from the agent's ability to reach them, and should temper claims like 'a significant subset of the strategy is provably correct.' The abstract's 'in some cases, we were able to formally verify the correctness of our agent' is defensible, but the introduction's 'results compar
  3. [Sections 4.3 and Appendix B] The proposed event-specific priority and soft/hard block extension changes the core SBP event-selection semantics, yet no formal semantics are given for the extended formalism. Appendix B describes the multi-sync mechanism and provides a code snippet, but it does not define precisely how priorities interact with hardBlock, softBlock, waitFor, and multiSync in all cases, nor how the BPPy model checker was extended to handle this new semantics. Since the formal verification guarantees in Section 5.2 are obtained with a model checker running on this extended runtime, the trustworthiness of the 'guaranteed to win' statements depends on an unstated formalization. The authors should supply a rigorous definition of the extended selection rule and, ideally, machine-checkable artifacts of the verification.
  4. [Section 5.1] The empirical evidence for the agent's performance is extremely limited: 10 games against the one nondeterministic opponent and 1 game each against the two deterministic opponents. With two of the three baselines, a single game is insufficient to demonstrate robustness, and with only 12 total games there is no statistical assurance. For the Pro Player, which has 'some small degree of non-determinism', the authors should report how many distinct opening moves actually occurred in the 10 matches and the margin of victory. As written, 'win every single match, with no losses or draws' is a thin basis for the RQ2 conclusion.
minor comments (4)
  1. [Throughout] There are typographical errors that should be corrected: 'enviornment' (Section 2.2), 'posses' (Section 4.1), 'implementaiton' (Appendix A), 'Drae' (Appendix A), 'verifably' (Section 5.2), and inconsistent capitalization of 'BPpy' (e.g., 'BPPy' in Sections 5.2 and 6).
  2. [Section 5.2] The paper says six fixed opening sequences were verified, but only three are shown (Figures 6–8). Please list all six configurations so the claim is reproducible, or state where the full set can be found.
  3. [Section 5.1] When describing the deployment, the statement that 'members of our team found it difficult to defeat it' is anecdotal and should be marked as such, or removed from the RQ2 evidence.
  4. [Section 6 / References] Reference [9] credits 'J. Doe' as the author of 'Unbeatable AI', which appears to be a placeholder name. Please verify and correct the citation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the formal guarantees are genuine model-checking results and the performance comparison is an empirical measurement, not a derivation from fitted inputs.

full rationale

The paper's central claims rest on two kinds of evidence. First, Section 5.2 reports model-checking results: 'From each such configuration, we successfully verified that our agent (yellow) was guaranteed to win, regardless of the subsequent moves played by its opponent.' This is an independent computation over the final agent program; the six openings are admittedly chosen because they match the agent's own strategies ('Both of these are strategies employed by our agent'), but the verified property is not defined as the input—it is a separate model-checking outcome. Second, Section 5.1 reports actual game results against three online opponents ('Our agent was able to win every single match'). The strength of those baselines is unmeasured, and the paper's 'state-of-the-art' language may overstate the evidence, but that is an external-validity / calibration concern, not circularity: the wins are empirical observations, not quantities fitted to the same data and then renamed as predictions. Self-citations in the related work (e.g., [25], [26], [29]) are contextual and do not carry any load-bearing derivation; no uniqueness theorem or ansatz is imported from the authors' prior work. The SBP extension in Appendix B is defined directly in the paper. Accordingly, no circular step can be exhibited with a specific reduction, and the appropriate finding is 'no significant circularity.'

Assumptions & free parameters 2 free parameters · 5 assumptions · 1 invented entities

The central claims rest on the correctness of the BPpy runtime with the new priority semantics, the completeness of the model checker, the strength of the three chosen baselines, and the human review process catching LLM errors. The priority constants are hand-tuned in the iterative loop. No artifacts are shipped to check any of this.

free parameters (2)
  • Strategy priority constants = BLOCK_BELOW_THREAT=19800, BLOCK_THREAT=19900, WIN=20000, POTENTIAL_WIN_P1 value not given
    Hand-chosen in the iterative LLM loop; they encode which strategy wins when requests and soft-blocks conflict at a synchronization point. The paper gives no principled derivation of these values; they are tuned until the verifier and matches pass.
  • Parity-based priority adjustments = Not disclosed; qualitative parity adjustments described in code comments
    The strategy comments assign higher priority to odd-row wins and even-row blocks (parity strategy from Allis). Specific numeric adjustments are not given, making them unexamined free parameters.
assumptions (5)
  • domain assumption SBP/BPpy event selection semantics, as extended with soft-block and multi-sync, behave as specified
    All gameplay claims rely on the runtime selecting an event iff requested by at least one object and not hard-blocked, and on soft-blocked events being triggerable when requested with higher priority. Invoked throughout Section 4.3 and Appendix B.
  • domain assumption DFSBProgramVerifier correctly enumerates all reachable states from the fixed openings
    The formal guarantees in Section 5.2 are only as strong as the explicit model checker's completeness; no independent artifact or independent re-verification is provided.
  • domain assumption The three online opponents are strong, state-of-the-art Connect4 agents
    RQ2 and the abstract's 'strong existing agents' claim are calibrated entirely to these baselines; their strength is never measured. The paper itself notes the Unbeatable AI 'boldly claims the title'.
  • domain assumption Allis' solved-game theorem and the odd/even row parity heuristics are applicable and correctly extracted
    Strategy inspiration [1, 2]; the agent inherits these heuristics. Standard domain knowledge.
  • domain assumption LLM-generated scenario objects, after human review, are correct implementations of the intended behaviors
    The methodology's core premise (Step 3, Section 3) is that human-in-the-loop review catches errors. The paper documents several LLM errors caught, which supports but does not prove the assumption for uncaught errors.
invented entities (1)
  • Event-specific priority and soft-block extension to SBP (softBlock, hardBlock, requestPriority, blockPriority, multiSync)
    purpose: Allow blocked events to fire when requested with higher priority, and assign per-event priorities, to resolve strategy conflicts in the Connect4 agent
    A genuine language and tool extension described in Section 4.3 and Appendix B. It is motivated by the LLM's suggestion, but no implementation is shipped, so the claimed semantics cannot be independently checked. It is testable in principle via code, hence not a physical entity; independent_evidence is false because no artifact is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability." pith.science (2026). https://pith.science/paper/AH72FUNY

@misc{pith2026250909194,
  author       = {Pith},
  title        = {Pith review of: On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AH72FUNY}},
  note         = {Machine review of arXiv:2509.09194}
}
read the original abstract

Large Language Models (LLMs) are fast becoming indispensable tools for software developers, assisting or even partnering with them in crafting complex programs. The advantages are evident -- LLMs can significantly reduce development time, generate well-organized and comprehensible code, and occasionally suggest innovative ideas that developers might not conceive on their own. However, despite their strengths, LLMs will often introduce significant errors and present incorrect code with persuasive confidence, potentially misleading developers into accepting flawed solutions. In order to bring LLMs into the software development cycle in a more reliable manner, we propose a methodology for combining them with ``traditional'' software engineering techniques in a structured way, with the goal of streamlining the development process, reducing errors, and enabling users to verify crucial program properties with increased confidence. Specifically, we focus on the Scenario-Based Programming (SBP) paradigm -- an event-driven, scenario-based approach for software engineering -- to allow human developers to pour their expert knowledge into the LLM, as well as to inspect and verify its outputs. To evaluate our methodology, we conducted a significant case study, and used it to design and implement the Connect4 game. By combining LLMs and SBP we were able to create a highly-capable agent, which could defeat various strong existing agents. Further, in some cases, we were able to formally verify the correctness of our agent. Finally, our experience reveals interesting insights regarding the ease-of-use of our proposed approach. The full code of our case-study will be made publicly available with the final version of this paper.

Figures

Figures reproduced from arXiv: 2509.09194 by the authors.

Figure 1
Figure 1. A Connect4 board game sample where red wins [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. From the trace of a counterexample found by the [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. SBM Agent (yellow) vs AI Pro (red) [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: SBM Agent (yellow) vs “Unbeatable AI” (red). [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: SBM Agent (yellow) vs “Galli’s AI” (red). [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 7
Figure 7. Figure 7: shows another verified opening configuration, in which yellow forms a classic fork, simultaneously creating a diagonal and a horizontal threat. The discs marked with an “X” highlight positions where yellow is poised to win via either line, making it impossible for red …
Figure 8
Figure 8. Figure 8: Fixed Moves Example 3. errors were challenging to overcome, but we soon recognized that providing clear feedback allowed the model to improve rapidly. For instance, the draw-detection logic was generated almost correctly on the first try once we supplied the appropriat…
Figure 6
Figure 6. Figure 6: illustrates one such opening sequence, where we observe that yellow has a diagonal odd-threat (the last disc that needs to be placed is in an odd row, and it will inevitably be yellow’s turn when it is time to place it); and also that yellow controls most of the middle…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

52 extracted references · 2 linked inside Pith

  1. [1]

    V. Allis. 1988.A Knowledge-Based Approach of Connect-Four — The Game is Solved: White Wins. Master’s thesis. Vrije Universiteit Amsterdam

    1988

  2. [2]

    V. Allis. 2025. How to Win Connect 4. Technical Report. https://www.rd.com/ article/how-to-win-connect-4/

    2025

  3. [3]

    Anthropic. 2023. Introducing Claude. https://www.anthropic.com/index/ introducing-claude

    2023

  4. [4]

    Ashrov and G

    A. Ashrov and G. Katz. 2023. Enhancing Deep Learning with Scenario-Based Override Rules: a Case Study. InProc. 11th Int. Conf. on Model-Driven Engineering and Software Development (MODELSW ARD). 253–268

    2023

  5. [5]

    Ashrov, A

    A. Ashrov, A. Sturm, A. Elyasaf, and G. Katz. 2025. A Study on the Comprehensi- bility of Behavioral Programming Variants. InProc. 20th Int. Conf. on Evaluation of Novel Approaches to Software Engineering (ENASE). 252–267

    2025

  6. [6]

    Chowdhery, S

    A. Chowdhery, S. Narang, J. Devlin, et al. 2022. PaLM: Scaling Language Modeling with Pathways. Technical Report. https://arxiv.org/abs/2204.02311

    arXiv 2022

  7. [7]

    Corsi, R

    D. Corsi, R. Yerushalmi, G. Amir, A. Farinelli, D. Harel, and G. Katz. 2024. Enforc- ing Specific Behaviours via Constrained DRL and Scenario-Based Programming. InProc. 31st Int. Conf. on Neural Information Processing (ICONIP). 284–302

    2024

  8. [8]

    Cursor. 2023. Cursor: The IDE that helps you Code with AI. https://www.cursor. com

    2023

Show all 52 references
  1. [9]

    J. Doe. 2025. Unbeatable AI — Connect4. https://websim.com/@Ch13fB1gT4lk/ connect-4-unbeatable-ai

    2025

  2. [10]

    X. Du, M. Liu, K. Wang, H. Wang, J. Liu, Y. Chen, J. Feng, C. Sha, X. Peng, and Y. Lou. 2024. Evaluating Large Language Models in Class-Level Code Generation. InProc. 46th Int. Conf. on Software Engineering (ICSE)

    2024

  3. [11]

    K. Galli. 2025. Connect4 Python GitHub Repository. https://github.com/ KeithGalli

    2025

  4. [12]

    Greenyer, D

    J. Greenyer, D. Gritzner, T. Gutjahr, F. König, N. Glade, A. Marron, and G. Katz

  5. [13]

    Greenyer, D

    J. Greenyer, D. Gritzner, G. Katz, and A. Marron. 2016. Scenario-Based Modeling and Synthesis for Reactive Systems with Dynamic System Structure in Scenari- oTools. InProc. 19th ACM/IEEE Int. Conf. on Model Driven Engineering Languages and Systems (MODELS). 16–23

    2016

  6. [14]

    Greenyer, D

    J. Greenyer, D. Gritzner, G. Katz, A. Marron, N. Glade, T. Gutjahr, and F. König

  7. [15]

    M. Haque. 2025. LLMs: A Game-Changer for Software Engineers? Technical Report. https://arxiv.org/abs/2411.00932

    2025 arXiv

  8. [16]

    Harel, A

    D. Harel, A. Kantor, and G. Katz. 2013. Relaxing Synchronization Constraints in Behavioral Programs. InProc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 355–372

    2013

  9. [17]

    Harel, A

    D. Harel, A. Kantor, G. Katz, A. Marron, L. Mizrahi, and G. Weiss. 2013. On Composing and Proving the Correctness of Reactive Behavior. InProc. 13th Int. Conf. on Embedded Software (EMSOFT). 1–10

    2013

  10. [18]

    Harel, A

    D. Harel, A. Kantor, G. Katz, A. Marron, G. Weiss, and G. Wiener. 2015. Towards Behavioral Programming in Distributed Architectures.Journal of Science of Computer Programming (J. SCP)98 (2015), 233–267

    2015

  11. [19]

    Harel and G

    D. Harel and G. Katz. 2014. Scaling-Up Behavioral Programming: Steps from Basic Principles to Application Architectures. InProc. 4th SPLASH Workshop on Programming based on Actors, Agents and Decentralized Control (AGERE!). 95–108

    2014

  12. [20]

    Harel, G

    D. Harel, G. Katz, R. Lampert, A. Marron, and G. Weiss. 2015. On the Succinctness of Idioms for Concurrent Programming. InProc. 26th Int. Conf. on Concurrency Theory (CONCUR). 85–99

    2015

  13. [21]

    Harel, G

    D. Harel, G. Katz, R. Marelly, and A. Marron. 2016. An Initial Wise Development Environment for Behavioral Models. InProc. 4th Int. Conf. on Model-Driven Engineering and Software Development (MODELSW ARD). 600–612

    2016

  14. [22]

    Harel, G

    D. Harel, G. Katz, R. Marelly, and A. Marron. 2016. First Steps Towards a Wise Development Environment for Behavioral Models.Int. Journal of Information System Modeling and Design (IJISMD)7(3) (2016), 1–22

    2016

  15. [23]

    Harel, G

    D. Harel, G. Katz, R. Marelly, and A. Marron. 2018. Wise Computing: Toward Endowing System Development with Proactive Wisdom.IEEE Computer51(2) (2018), 14–26

    2018

  16. [24]

    Harel, G

    D. Harel, G. Katz, A. Marron, A. Sadon, and G. Weiss. 2020. Executing Scenario- Based Specification with Dynamic Generation of Rich Events.Communications in Computer and Information Science (CCIS)1161 (2020), 246–274

    2020

  17. [25]

    Harel, G

    D. Harel, G. Katz, A. Marron, and S. Szekely. 2024. On Augmenting Scenario- Based Modeling with Generative AI. InProc. 12th Int. Conf. on Model-Driven Engineering and Software Development (MODELSW ARD). 235–246

    2024

  18. [26]

    Harel, G

    D. Harel, G. Katz, A. Marron, and S. Szekely. 2025. Enhancing Scenario-Based Modeling using Large Language Models.Communications in Computer and Information Science (CCIS)2547 (2025), 43–68

    2025

  19. [27]

    Harel, G

    D. Harel, G. Katz, A. Marron, and G. Weiss. 2012. Non-Intrusive Repair of Reactive Programs. InProc. 17th IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS). 3–12

    2012

  20. [28]

    Harel, G

    D. Harel, G. Katz, A. Marron, and G. Weiss. 2014. Non-Intrusive Repair of Safety and Liveness Violations in Reactive Programs.Transactions on Computational Collective Intelligence (TCCI)16 (2014), 1–33

    2014

  21. [29]

    Harel, G

    D. Harel, G. Katz, A. Marron, and G. Weiss. 2015. The Effect of Concurrent Programming Idioms on Verification. InProc. 3rd Int. Conf. on Model-Driven Engineering and Software Development (MODELSW ARD). 363–369

    2015

  22. [30]

    Harel, R

    D. Harel, R. Lampert, A. Marron, and G. Weiss. 2011. Model-Checking Behavioral Programs. InProc. 11th Int. Conf. on Embedded Software (EMSOFT). 279–288

    2011

  23. [31]

    Harel, A

    D. Harel, A. Marron, and G. Weiss. 2012. Behavioral Programming.Commun. ACM55, 7 (2012), 90–100

    2012

  24. [32]

    G. Katz. 2013. On Module-Based Abstraction and Repair of Behavioral Pro- grams. InProc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 518–535

    2013

  25. [33]

    G. Katz. 2020. Guarded Deep Learning using Scenario-Based Modeling. InProc. 8th Int. Conf. on Model-Driven Engineering and Software Development (MODEL- SW ARD). 126–136

    2020

  26. [34]

    G. Katz. 2021. Augmenting Deep Neural Networks with Scenario-Based Guard Rules.Communications in Computer and Information Science (CCIS)1361 (2021), 147–172

    2021

  27. [35]

    G. Katz. 2021. Towards Repairing Scenario-Based Models with Rich Events. InProc. 9th Int. Conf. on Model-Driven Engineering and Software Development (MODELSW ARD). 362–372

    2021

  28. [36]

    G. Katz, C. Barrett, and D. Harel. 2015. Theory-Aided Model Checking of Concur- rent Transition Systems. InProc. 15th Int. Conf. on Formal Methods in Computer- Aided Design (FMCAD). 81–88

    2015

  29. [37]

    Katz and A

    G. Katz and A. Elyasaf. 2021. Towards Combining Deep Learning, Verification, and Scenario-Based Programming. InProc. 1st Workshop on Verification of Autonomous and Robotic Systems (V ARS). 1–3

    2021

  30. [38]

    G. Katz, A. Marron, A. Sadon, and G. Weiss. 2019. On-the-Fly Construction of Composite Events in Scenario-Based Modeling Using Constraint Solvers. InProc. 7th Int. Conf. on Model-Driven Engineering and Software Development (MODEL- SW ARD). 143–156

    2019

  31. [39]

    Y. Li, J. Parsert, and E. Polgreen. 2024. Guiding Enumerative Program Syn- thesis with Large Language Models. Proc. 36th Int. Conf. on Computer Aided Verification (CAV)

    2024

  32. [40]

    Marron, Y

    A. Marron, Y. Hacohen, D. Harel, A. Mülder, and A. Terfloth. 2018. Embedding Scenario-based Modeling in Statecharts. InProc. 5th Int. Workshop on Model-driven Robot Software Engineering (MORSE). 443–452

    2018

  33. [41]

    OpenAI. 2023. GPT-4. Technical Report. https://openai.com/research/gpt-4

    2023

  34. [42]

    Steinberg, J

    S. Steinberg, J. Greenyer, D. Gritzner, D. Harel, G. Katz, and A. Marron. 2017. Distributing Scenario-Based Models: A Replicate-and-Project Approach. InProc. 5th Int. Conf. on Model-Driven Engineering and Software Development (MODEL- SW ARD). 182–195

    2017

  35. [43]

    Steinberg, J

    S. Steinberg, J. Greenyer, D. Gritzner, D. Harel, G. Katz, and A. Marron. 2018. Efficient Distributed Execution of Multi-Component Scenario-Based Models. Communications in Computer and Information Science (CCIS)880 (2018), 449–483

    2018

  36. [44]

    C. Sun, Y. Sheng, O. Padon, and C. Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. InProc. 1st Int. Symposium on AI Verification (SAIV). 134–155

    2024

  37. [45]

    Tleemann

    T. Tleemann. 2025. Pro Player — Connect4. https://tleemann.de/four.html

    2025

  38. [46]

    T. Yaacov. 2023. BPpy: Behavioral Programming in Python.SoftwareX24 (2023)

    2023

  39. [47]

    Yaacov, A

    T. Yaacov, A. Elyasaf, and G. Weiss. 2024. Boosting LLM-Based Software Genera- tion by Aligning Code with Requirements. Proc. IEEE 32nd Int. Requirements Engineering Conference Workshops (REW)

    2024

  40. [48]

    Yaacov, G

    T. Yaacov, G. Weiss, A. Ashrov, G. Katz, and H. Zisser. 2025. Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods. InProc. 20th Int. Conf. on Evaluation of Novel Approaches to Software Engineering (ENASE). 27–40

    2025

  41. [49]

    Yerushalmi, G

    R. Yerushalmi, G. Amir, A. Elyasaf, D. Harel, G. Katz, and A. Marron. 2022. Scenario-Assisted Deep Reinforcement Learning. InProc. 10th Int. Conf. on Model- Driven Engineering and Software Development (MODELSW ARD). 310–319

    2022

  42. [50]

    Yerushalmi, G

    R. Yerushalmi, G. Amir, A. Elyasaf, D. Harel, G. Katz, and A. Marron. 2023. En- hancing Deep Reinforcement Learning with Scenario-Based Modeling.Springer Nature Computer Science (SNCS)4 (2023), 1–13

    2023

  43. [2016]

    Distributed Execution of Scenario-Based Specifications of Structurally Dynamic Cyber-Physical Systems. InProc. 3rd Int. Conf. on System-Integrated Intelligence: New Challenges for Product and Production Engineering (SYSINT). 552–559

  44. [2017]

    SCP)149 (2017), 15–27

    ScenarioTools — A Tool Suite for the Scenario-based Modeling and Analysis of Reactive Systems.Journal of Science of Computer Programming (J. SCP)149 (2017), 15–27

    2017

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.