No information available yet.
Fri 20 FebDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
09:00 - 09:30 | |||
09:30 - 10:30 | |||
09:30 60mKeynote | Software Dependencies: Then, Now, and What’s Next ISEC 2026 Keynotes Sarah Nadi New York University Abu Dhabi | ||
14:00 - 15:00 | |||
14:00 60mKeynote | On Estimating Incorrectness in the Absence of Evidence ISEC 2026 Keynotes Marcel Böhme MPI for Security and Privacy | ||
Sat 21 FebDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
09:00 - 09:45 | |||
09:00 45mTalk | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming ISEC 2026 Keynotes Saikat Chakraborty Microsoft Research | ||
09:45 - 10:30 | |||
09:45 45mTalk | A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification ISEC 2026 Keynotes Nian-Ze Lee National Taiwan University, Taiwan | ||
11:00 - 11:30 | |||
11:00 30mTalk | Impact of Feature Selection Techniques on Bug Prediction Models ISEC 2026 Keynotes | ||
14:00 - 15:00 | |||
14:00 60mKeynote | Shipping Models, Not Just Code: How AI Is Forcing Software Engineering to Evolve ISEC 2026 Keynotes Siddhartha Asthana Mastercard | ||
17:30 - 18:00 | |||
Accepted Papers
| Title | |
|---|---|
| A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification ISEC 2026 Keynotes | |
| Impact of Feature Selection Techniques on Bug Prediction Models ISEC 2026 Keynotes | |
| On Estimating Incorrectness in the Absence of Evidence ISEC 2026 Keynotes | |
| Shipping Models, Not Just Code: How AI Is Forcing Software Engineering to Evolve ISEC 2026 Keynotes | |
| Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming ISEC 2026 Keynotes |
Keynote Speakers
Dr. Sarah Nadi
Sarah Nadi is an Associate Professor in the Computer Science Program at New York University Abu Dhabi (NYUAD). Before joining NYUAD, she spent 7.5 years at the University of Alberta in Canada where she held a Tier II Canada Research Chair in Software reuse and lead the Software Maintenance and Reuse (SMR) lab. Sarah obtained her Master's (2010) and PhD (2014) degrees from the University of Waterloo in Canada and spent approximately two years as a post-doctoral researcher at the Technische Universität Darmstadt in Germany. At NYUAD, Sarah co-directs the SANAD lab whose goal is to enhance how software engineers develop and maintain software systems by providing them with the tools and insights that they need. Sarah's research expertise lies in empirical software engineering and software analytics. She has worked on a wide range of software engineering problems including finding bugs and inconsistencies in software product line, detecting insecure API usage, and using AI for software engineering. Her recent work focuses on supporting developers as they use software libraries, including the initial selection process, correctly using the library's API, and potential migration to newer versions or alternative libraries.
Keynote Talk & Abstract:
Title: Software Dependencies: Then, Now, and What's Next
Click to view Abstract
Modern software development heavily relies on third-party libraries. While these dependencies accelerate development, they introduce their own set of challenges. In this talk, I will explore three common hurdles developers face and the techniques and tools that we have built to address them: comparing and selecting libraries, avoiding API misuse, and migrating to newer library versions or entirely different libraries. Then we will fast-forward to today’s reality: the growing and pervasive reliance on Large Language Models (LLMs). While LLMs are helping to alleviate some of the above challenges, new advances are also redefining software dependencies and how we can ensure their correct usage, opening the door to a new set of challenges we are only beginning to understand.
Profiles:
• Website
• NYUAD Profile
Dr. Marcel Bohme
Marcel Böhme is a faculty member at the Max Planck Institute for Security and Privacy (MPI-SP) in Germany where he leads the Software Security research group. His group has made foundational contributions to automatic software testing, specifically fuzzing which has become one of the most successful techniques for automatic vulnerability discovery at scale: While conventional wisdom has that testing can only show the presence of bugs but never their absence, Marcel has developed the first statistical framework to make statements about a program's correctness after an error-less testing campaign. While testing is embarrassingly parallel, his probabilistic theory explains how the cost of bug finding is actually exponential in the number of machines, and when even the most effective systematic testing technique is outperformed by a simple, random approach. More recently, his group has been developing the statistical and causal foundations of empirical software security analysis at scale, supported by an ERC grant. To find out more about the research in his group, head over to https://mpi-softsec.github.io
Keynote Talk & Abstract:
Title: On Estimating Incorrectness in the Absence of Evidence
Click to view Abstract
We introduce a statistical framework for automated software testing that allows us estimate, extrapolate, and explain various interesting properties of a testing campaign. We will show how to quantify our confidence in the correctness of a program after a long-running testing campaign that has found no bugs. We will explain how Shannon’s entropy is a non-parametric measure of testing efficiency and why the cost of bug finding appears to be exponential even if testing is embarrassingly parallel. We will extend the approach to statistical program analysis and make progress on the statistical problem itself. Finally, we will talk about our most recent work on estimating incorrectness (of an LLM-generated program) in the absence of an oracle.
Profiles:
• Website
• MPI SoftSec Group
• LinkedIn
Dr. Siddhartha Asthan
Dr. Siddhartha Asthana is Vice President at Mastercard’s AI Garage in Gurgaon, where he leads AI and machine learning innovation across payments and cybersecurity, driving strategy and production-scale AI systems. He also serves as Adjunct Faculty at Ahmedabad University, mentoring emerging AI talent. He earned his Ph.D. from IIIT-Delhi in machine learning and human–computer interaction, with research on mobile systems for developing regions supported by a TCS Research Fellowship. He has received grants and recognition from Google India, ACM SIGSOFT, and Microsoft Research India. An active researcher with an h-index of 13 and over 480 citations, his work includes CHI 2016’s “A Real-Time IVR Platform for Community Radio,” ICTD 2013’s “Airavat,” and research spanning HCI, data science, and graph-based fraud detection. He regularly reviews for venues such as ACM SIGCHI, ACM CODS-COMAD, and AAAI. Previously, he held senior roles at Optum (UnitedHealth Group) and Accenture, leading analytics initiatives across healthcare and cloud platforms. At ICSE 2026, he will discuss translating research into scalable, real-world AI systems. .
Keynote Talk & Abstract:
Title: Shipping Models, Not Just Code: How AI Is Forcing Software Engineering to Evolve
Click to view Abstract
AI-driven systems are forcing software engineering to move beyond deterministic code toward probabilistic, data-driven behavior. Drawing on experience building real-time fraud and risk models at Mastercard—operating over billions of transactions with strict latency constraints—this keynote explores how requirements, testing, deployment, and operations fundamentally change when we ship models, not just code. I will share how industry teams are adapting the software engineering lifecycle to handle uncertainty, continuous learning, and production feedback loops at scale. Finally, I will outline key gaps and research opportunities for the software engineering community as AI becomes a first-class engineering concern.
SIGSOFT Distinguished Paper Invited Speakers
Dr. Nian-Ze Lee
Dr. Nian-Ze Lee is an Assistant Professor in the Department of Electrical Engineering at National Taiwan University (NTUEE), a position he has held since February 2025, and a Guest Professor ("Gastprofessor") at the Institute of Informatics, LMU Munich, Germany. He earned his Ph.D. in Electronics Engineering from NTU in 2021, where he was selected as an honorary member of the Phi Tau Phi Scholastic Honor Society. His dissertation on stochastic Boolean satisfiability received the prestigious Lam Research Thesis Award. From 2021 to 2024, Dr. Lee was a Postdoctoral Researcher at LMU Munich, Germany, focusing on formal methods and their practical applications in software engineering and EDA. His work has been recognized at top-tier international conferences and earned several awards, including an ACM SIGSOFT Distinguished Paper Award and a Best Artifact Award at FSE 2024, a Best Paper Award at SPIN 2024, and a Distinguished Artifact Award at TACAS 2024. As of 2025, he leads multiple research projects as a principal investigator, including a DFG-funded research project and an Intel-funded collaboration. From 2025 to 2028, he holds the Garmin Scholar Fellowship at NTU.
Keynote Talk & Abstract:
Title: A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification
Abstract
Click to view Abstract
Assuring the correctness of computing systems is fundamental to our society and economy, and formal verification is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, Craig interpolation has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) Interpolation-Sequence-Based Model Checking (Vizel and Grumberg, 2009) and (2) Intertwined Forward-Backward Reachability Analysis Using Interpolants (Vizel, Grumberg, and Shoham, 2013), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms..
Profiles:
• NTUEE Faculty
• LMU Munich Profile
• Website
Saikat Chakraborty
Senior Researcher Research in Software Engineering Microsoft Research, Redmond, WA, USA.
Saikat Chakraborty is a Senior Researcher at Microsoft Research whose work centers on building trustworthy AI for software engineering. His research integrates large language models, formal verification methodologies, and proof-oriented programming to develop AI systems capable of both code generation and comprehensive justification and validation of their outputs. Saikat leads projects on reinforcement learning through verification, AI-assisted specification and invariant discovery, and proof-carrying code for real-world software stacks. He collaborates closely with product teams to translate advances in verification-aware AI into practical developer tools, targeting tasks such as automatic bug detection, patch validation, and test generation at scale. Saikat’s work has appeared in leading venues such as the International Conference on Software Engineering (ICSE 2025), where he focuses on making formal reasoning usable by everyday developers. Ultimately, his objective is to make AI assisted coding safer, more secure and more reliable – with the help of AI, perhaps. He earned his Ph.D. from Columbia University, where he worked on Programming Language Processing, aiming at automated code editing with AI.
Keynote Talk & Abstract:
Title: Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Click to view Abstract
Abstract: Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem producing a definition given a formal specification expressed as an F* type. We provide a program fragment checker that queries F* to check the correctness of candidate solutions. We also report on an extended version of our dataset containing a total of 940K lines of programs and proofs, with a total of 54k top-level F* definitions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate the use of AI to synthesize programs and their proofs in F*, with promising results. Our main finding in that the performance of fine-tuned smaller language models (such as Phi-2 or StarCoder) compare favorably with large language models (such as GPT-4), at a much lower computational cost. We also identify various type-based retrieval augmentation techniques and find that they boost performance significantly. With detailed error analysis and case studies, we identify potential strengths and weaknesses of models and techniques and suggest directions for future improvements.
Profiles:
• LinkedIn Profile
ISEC Test of time award Paper Invited Speaker
Dr. Muthukumaran K
Assistant Professor (Senior Grade 2), VIT Chennai, Tamil Nadu, India
Dr. Muthukumaran Kasinathan is currently working as an Assistant professor (senior) in School of Computer Science & Engineering at VIT Chennai. He received his Ph.D. in Computer Science and Engineering from BITS Pilani. His thesis is titled “Prediction and Probability Distribution of Defects in Software Systems”. His research primarily focuses on improving developer’s productivity and software quality. His research interests include Empirical Software Engineering, Mining Software Repositories, Search-based Software Engineering and Robotics. His teaching spans core areas of computer science and robotics, including data structures & algorithms, software engineering, robot programming, robot simulation & modeling and robotic perception.
Test of Time awardee Talk & Abstract:
Title: Impact of Feature Selection Techniques on Bug Prediction Models.
Click to view Abstract
Abstract: Several change metrics and source code metrics have been introduced and proved to be effective features in building bug prediction models. Researchers performed comparative studies of bug prediction models built using the individual metrics as well as combination of these metrics. In this paper, we investigate whether the prediction accuracy of bug prediction models is improved by applying feature selection techniques. We explore if there is one algorithm amongst ten popular feature selection algorithms that consistently fares better than others across sixteen bench marked open source projects. We also discuss whether the metrics in best feature subset are consistent across projects.
Profiles:
• LinkedIn Profile >
• Website