הכנס הארצי למדעי המחשב והמידע

Abstract

The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on complex programs, producing invariants that are invalid or computationally ineffective. We present Wonda, a pipeline for fine-tuning Small Language Models (SLMs) to enable the to produce high-quality invariants. On the challenging InvBench suite, our approach enables small models to outperform off-the-shelf models 20x their size.

Based on joint work with Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu and Nina Narodytska. This work appeared in ICML 2026.

Abstract

AI lets us recover the old promises of formal specification—early error detection, explicit invariants, correctness by design—without the notational burden that kept formal methods out of industry. The trick is to treat the specification as the artifact you author, review, and refine, and the code as disposable output. Using two examples—a simulation of organizational knowledge growth and an online-banking fund-transfer service—I show one consistent discipline: an AI reviews the spec for ambiguities, conservation invariants are proved by induction and turned into runtime checks, and interfaces are captured in Z schemas. The punchline: the generated code was never inspected as it evolved—there was no need to. Specification-level review, proof, invariants, and Z gave enough confidence that the implementations were correct by construction.

תקציר

כפי שפיתוח מונחה עצמים הוביל להתפתחותן של מתודולוגיות פיתוח תוכנה חדשות (בעיקר אג'יליות), וכן לשינויים משמעותיים במבנה ותפקידי צוותי הפיתוח, כך גם פיתוח תוכנה אג'נטי צפוי לחולל שינוי משמעותי באופן שבו תוכנה מתוכננת, מפותחת ומתוחזקת.
כבר היום ברור כי בעידן פיתוח תהתוכנה האג'נטי, שבו מערכות אג'נטיות משתלבות בתהליך הפיתוח, משתנה מקצוע הנדסת התוכנה: מהתמקדות בכתיבת קוד והגדרת אלגוריתמים ניתן לראות מעבר לעיצוב פתרונות, הגדרת מטרות, ניהול אינטראקציה עם סוכנים חכמים והערכת תוצרים שנוצרים בשיתוף אדם–מכונה. שינוי זה מחייב חשיבה מחודשת על מתודולוגיות הפיתוח, על מבנה צוותי הפיתוח העתידיים ועל חלוקת האחריות בין חברי וחברות הצוות.
בהרצאה נבחן כיוונים אפשריים להתפתחות מתודולוגיות פיתוח בעידן הפיתוח האג'נטי, ונעסוק באופן שבו צוותי פיתוח עשויים להשתנות: אילו תפקידים חדשים ייווצרו, כיצד תשתנה חלוקת העבודה בין בני אדם לסוכנים, כיצד תשתנה התקשורת ושיתוף הפעולה בצוות, ואילו מיומנויות תדרשנה ממפתחי תוכנה בעתיד.
חשיבותו של נושא זה עולה במיוחד בתקופה שבה מקצוע הנדסת התוכנה עצמו עובר עיצוב מחדש; משבר הג'וניורים, אותו חווים בוגרים ובוגרות מדעי המחשב והנדסת תוכנה בתחילת דרכם בשוק העבודה המשתנה, נמצא בעיצומו; והאקדמיה נדרשת לחשב מסלול מחדש בכלל ובהקשר להכשרת מהנדסי ומהנדסות תוכנה בפרט.

תקציר

כפי שפיתוח מונחה עצמים הוביל להתפתחותן של מתודולוגיות פיתוח תוכנה חדשות (בעיקר אג'יליות), וכן לשינויים משמעותיים במבנה ותפקידי צוותי הפיתוח, כך גם פיתוח תוכנה אג'נטי צפוי לחולל שינוי משמעותי באופן שבו תוכנה מתוכננת, מפותחת ומתוחזקת.
כבר היום ברור כי בעידן פיתוח תהתוכנה האג'נטי, שבו מערכות אג'נטיות משתלבות בתהליך הפיתוח, משתנה מקצוע הנדסת התוכנה: מהתמקדות בכתיבת קוד והגדרת אלגוריתמים ניתן לראות מעבר לעיצוב פתרונות, הגדרת מטרות, ניהול אינטראקציה עם סוכנים חכמים והערכת תוצרים שנוצרים בשיתוף אדם–מכונה. שינוי זה מחייב חשיבה מחודשת על מתודולוגיות הפיתוח, על מבנה צוותי הפיתוח העתידיים ועל חלוקת האחריות בין חברי וחברות הצוות.
בהרצאה נבחן כיוונים אפשריים להתפתחות מתודולוגיות פיתוח בעידן הפיתוח האג'נטי, ונעסוק באופן שבו צוותי פיתוח עשויים להשתנות: אילו תפקידים חדשים ייווצרו, כיצד תשתנה חלוקת העבודה בין בני אדם לסוכנים, כיצד תשתנה התקשורת ושיתוף הפעולה בצוות, ואילו מיומנויות תדרשנה ממפתחי תוכנה בעתיד.
חשיבותו של נושא זה עולה במיוחד בתקופה שבה מקצוע הנדסת התוכנה עצמו עובר עיצוב מחדש; משבר הג'וניורים, אותו חווים בוגרים ובוגרות מדעי המחשב והנדסת תוכנה בתחילת דרכם בשוק העבודה המשתנה, נמצא בעיצומו; והאקדמיה נדרשת לחשב מסלול מחדש בכלל ובהקשר להכשרת מהנדסי ומהנדסות תוכנה בפרט.

Abstract

The demand for secure, privacy-preserving, and ethical software systems has never been higher, prompting industry-wide calls for proactive "by design" approaches. However, the actual implementation of these practices consistently falls short, often resulting in systemic vulnerabilities or the phenomenon of "AI ethics washing". This lecture explores why technical solutions and formal policies are insufficient on their own, highlighting the critical role of organizational climate in shaping developers' mindsets and behaviors. We will examine how organizational security and privacy climates dictate the true priority these facets receive, especially when pitted against competing goals, and the pheonmenon of "decoupling" – a distinct gap between formal ethical declarations and actual operational practices. Fostering the design of responsible and trustworthy AI and software systems requires actively cultivating a supportive organizational environment. This involves aligning leadership communication, resolving conflicting organizational goals, and closing the gap between declared policies and operational reality to genuinely support developers in proactive behavior of implementing responsibility by design.

Abstract

Traditional formal methods are based on Boolean structures, such as finite automata and classic temporal logics. While successful, these models are limited in their expressive power. Over the past few decades, there has been a surge of research on quantitative models—extensions of automata, logic, and games incorporating weights, counters, registers, etc. These models are far richer than traditional ones and can naturally capture infinite-configuration systems, with many still admitting decidable verification problems.
However, despite their expressive power, quantitative models have not yet seen widespread adoption in practice. In this talk, I will survey recent theoretical progress on various quantitative models, discuss potential application domains, and speculate on what is needed to bridge the gap between theory and practical application.