KeynotesInternetware 2026

At Internetware 2026, we are excited to present the following four keynote speakers:

Jin-Song Dong

Title: Reasoning Beyond LLMs and a Vision for Life After Superintelligence: The Player Era

Abstract: The rise of code-centric Large Language Models (LLMs) has reshaped software engineering, with tools such as Copilot, GPT-5, and Gemini-3 now capable of generating code with remarkable ease. However, these systems offer no inherent guarantees of correctness and remain susceptible to hallucinations. The first part of this talk shows how program refinement calculus can serve as a "formal chain of thought" to guide LLMs and verify the correctness of generated code [POPL 2025]. The second part explores LLM-aided system design and validation, introducing LLM-enhanced model-checking agents [ICML 2025, NeurIPS 2025, ASE 2025, FSE 2026]. The third part examines the limitations of LLMs in tackling complex planning and strategic reasoning tasks that require rigorous symbolic methods [ICLR 2025, AAAI 2026]. The talk concludes with a forward-looking vision, the Player Era [ISACE 2026], for life beyond artificial superintelligence (ASI). This vision posits that humanity will evolve into four distinct yet interconnected roles: the Player, the Explorer, the Co-Creator, and the Gatekeeper, forming the foundation of a future civilization centered on meaning, creativity, and responsibility.

Bio: Jin-Song Dong is a Professor at the National University of Singapore. His research spans formal methods for LLM-based agents, safety and security systems, trusted AI, probabilistic reasoning, sports analytics, and verified LLM-driven code synthesis. He is a co-founder of the PAT verification system, a widely adopted formal analysis platform with thousands of users across more than 150 countries. He also co-founded Silas (http://www.depintel.com), a commercialized trusted machine learning system with over 50,000 downloads. He has served on the editorial boards of ACM Transactions on Software Engineering and Methodology, Formal Aspects of Computing, and Innovations in Systems and Software Engineering, a NASA journal. He has supervised 34 PhD students, many of whom now hold tenured academic positions at leading institutions worldwide. He is a Fellow of the Institute of Engineers Australia. In sports analytics, he developed Markov Decision Process (MDP) models for tennis strategy analysis using PAT, supporting professional players with pre-match preparation at the highest levels of competition. He also founded ISACE, a new conference series on sports analytics. Outside academia, he is a tennis coach and enjoys mentoring his students and his three children, all of whom have achieved top national junior rankings in Singapore and Australia. Two of his children have received full NCAA Division I scholarships. His second son, Chen Dong, professionally ranked in ATP, played #1 singles for Australia in the Junior Davis Cup World Final and participated in both the Australian Open and US Open Junior Grand Slams.

Corina Pasareanu

Title: Building Trustworthy AI: Attacking Code Agents and Enhancing Code Generation via LLM Ensembles and Partial-Code Reward Models

Abstract: As Large Language Model (LLM) code agents are increasingly trusted to autonomously develop software and fix real-world bugs, ensuring code reliability and security has become a significant challenge. Traditional evaluation benchmarks heavily favor functional correctness, overlooking critical structural flaws and underlying security risks. We begin our talk by first exposing a critical, overlooked vulnerability in modern AI-driven engineering workflows: Functionally Correct yet Vulnerable (FCV) patches. Through our proposed black-box FCV-Attack, we show that state-of-the-art LLMs and agent scaffolds, including SWE-agent and OpenHands, can be manipulated via a single query to produce code that passes all functional test suites while stealthily embedding severe vulnerabilities. To defend against such threats and maximize code reliability, we describe two techniques. SecCodePRM, Security-Oriented Process Reward Model, moves beyond sparse end-of-completion feedback by deriving dense, step-level supervision labels from static analyzers and expert annotations to assign context-aware security scores along streaming code trajectories. This addresses the limitations of traditional detectors on long-horizon code and supports real-time, prefix-level inference scaling without a safety-utility tradeoff. Similarity-Based LLM Ensembles mitigate monolithic model biases by generating candidate solutions across a diverse ensemble of LLMs. Candidates are filtered via a structured voting mechanism that aggregates syntactic and semantic similarities using CodeBLEU alongside behavioral equivalence evaluated through differential symbolic execution.

Bio: Corina Pasareanu is an ACM Fellow and an IEEE ASE Fellow, working at Amazon PrimeAi. She is also affiliated with Carnegie Mellon University's CyLab. Her research interests include model checking, symbolic execution, compositional verification, probabilistic software analysis, autonomy, and security. She is the recipient of several awards, including ETAPS Test of Time Award (2021), ASE Most Influential Paper Award (2018), ESEC/FSE Test of Time Award (2018), ISSTA Retrospective Impact Paper Award (2018), ACM Impact Paper Award (2010), and ICSE 2010 Most Influential Paper Award (2010).

Naijun Zhan

Title: Formal Design of Safety-critical Cyber-Physical Systems

Abstract: I will report our recent work on model-based formal design of safety-critical CPSs. With our approach, one can build a graphical model for a system to be developed with the combination of Simulink/Stateflow and AADL (AADL+S/S), and then conduct extensive simulation. Afterwards, an AADL+S/S graphical model can be translated to an HCSP formal model automatically, so that the translated HCSP formal model can be verified using Hybrid Hoare Logic and its theorem prover, called HHLProver. To justify the correctness of the translation, we define formal semantics of AADL+S/S and HCSP respectively with HUTP (Higher-order Unifying Theories of Programming), and the correctness of the translation is therefore proved theoretically. Finally, we propose the notion of approximate bisimulation for HCSP, and define a set of refinement rules through which we can refine an HCSP process into a piece of SystemC code or ANSI-C code, which is approximate bisimilar to the original HCSP process. All the above are supported by a tool chain called MARS. The above approach is demonstrated by applying it to design some real-world case studies.

Bio: Naijun Zhan is a Boya distinguished professor in the School of Computer Science of Peking University. He got his BSc and MSc both from Nanjing University, and his PhD from Institute of Software Chinese Academy of Sciences (ISCAS). Prior to joining Peking University, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow, and afterwards worked at ISCAS as an associate professor, a full professor, and a distinguished professor. His research interests cover formal design of real-time, embedded and hybrid systems, and program verification. He is on the editorial boards of Journal of Automated Reasoning, Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Electronics, and Journal of Computer Research and Development, among others. He is a member of the steering committees of SETTA and MEMOCODE, the PC co-chair of TACAS 2027, ICFEM 2025, FM 2021 and SETTA 2016, the general co-chair of SETTA 2025, MEMOCODE 2019, MEMOCODE 2018 and ICESS 2019, and serves on more than 100 international conference program committees, including CAV, RTSS, HSCC, FM, TACAS, and EMSOFT. He has published more than 150 papers in leading international journals and conferences and 2 books, and has edited 5 conference proceedings and 7 journal special issues. See lcs.ios.ac.cn/~znj for more details.

Liming Zhu

Title: Software is Dead. Long Live the Environment: Towards Verification-First AIWare

Abstract: We have long treated software as something we specify, even as it is increasingly built by AI or relies on AI for intelligence. This framing is breaking down. In future AI software, the primary act of engineering shifts from specifying the software itself to shaping the environment in which AI software interact, receive verification signals, and iteratively build, operate, and improve. This talk introduces verification-first AIWare as a way to understand this shift: systems where AI, software, and environments co-evolve, and where capability emerges from the interaction between AIWare and the environment mechanisms that constrain and evaluate it, such as constraint checking, world model-based simulations, testing, and human feedback. In this view, both the AIWare and the environment adapt over time, with human input serving as one way of expressing intent rather than the source of design or error correction. The talk invites a rethinking of software not as something we fully specify, but as something that forms and reforms within an evolving environment of verification and feedback.

Bio: Dr Liming Zhu is a Research Director at CSIRO and former Head of Data61, Australia’s national digital and AI research capability, and is a conjoint professor at UNSW. A recognised leader in AI engineering and responsible AI, he contributes to the International AI Safety Report, OECD.AI work on Risks and Accountability, ISO AI standards, and Australia’s AI safety standards and guidance. His research leadership spans AI engineering, responsible and safe AI, privacy, cybersecurity, digital resilience, computational platforms, digital trust, software systems, and quantum software. He has authored more than 400 publications and delivered keynotes at major international venues, including “Software Engineering as the Linchpin of Responsible AI” at ICSE. His books, Responsible AI: Best Practices for Creating Trustworthy AI Systems and Engineering AI Systems: Architecture and DevOps Essentials, reflect his vision for rigorous, safe and societally beneficial AI systems.