Keynotes

Abstract: Software complexity is a challenging concept. The goal is to come up with a metric that can be computed in a scalable manner, and that enables us to predict a property of the software. If we want to predict the difficulty of symbolically executing or randomly testing software, what complexity metrics can we use? I will discuss two concepts called path complexity and branch selectivity as potential metrics for software complexity within this context.

Bio: Tevfik Bultan is a Professor in the Department of Computer Science at the University of California, Santa Barbara (UCSB). His research interests are in software verification, program analysis, software engineering, and computer security. He co-chaired the program committees of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), the 20th International Symposium on the Foundations of Software Engineering (FSE 2012), the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013), and the 41st ACM/IEEE International Conference on Software Engineering (ICSE 2019). He was the general chair of the 2017 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017). He served as the chair (2019-2023) and vice chair (2005-2009) of the Department of Computer Science at UCSB. Tevfik Bultan is the recipient of a NATO Science Fellowship from the Scientific and Technical Research Council of Turkey (TUBITAK), a Regents’ Junior Faculty Fellowship from the University of California, Santa Barbara, a Faculty Early Career Development (CAREER) Award from the National Science Foundation, two ACM SIGSOFT Distinguished Paper Awards, a Best Paper Award from International Conference on Automated Software Engineering (ASE), and the UCSB Academic Senate Outstanding Graduate Mentor Award. He was recognized as an ACM Distinguished Scientist in 2016.

Abstract: Over the last decades, dynamic symbolic execution (symbex) emerged as one of promising automated approaches to software testing and analysis. It has been applied to automatically test system-level software, software patches, network stacks, verify functional equivalence, and more. Tools based on flavors of symbex were even successfully used to test Microsoft Office and in the prestigious DARPA’s Cyber Grand Challenge competition. However, scalability limitations attributed to symbex, as well as the complex nature of the technique have been clipping its wings and limiting its wider adoption. At the same time, over the last decade fuzzing has been booming and became a de-facto standard for automated testing. Why has symbex not seen the success and widespread adoption similar to fuzzing? Why a technique with stronger guarantees and reasoning power is not the first choice for testing in industry? In this keynote we share some thoughts and lessons learned on how to help symbolic execution SOAR by making it Selective, Open-source, Approachable and Real-world. We showcase several research projects in which we enhanced symbex to achieve greater scalability and fitness for the purpose. Furthermore, we discuss how different perspectives in academia and industry affect the way techniques are developed, evaluated and used. Finally we try to estimate where symbex stands on the road to becoming commonplace.

Bio: Tomasz Kuchta is a computer scientist striving to make computer systems reliable and secure. He is a member of Samsung’s Mobile Security Team in Warsaw where he works on research, development of automation tools and security assessment of the latest flagship devices. In the past, Tomasz helped secure mobile products at Qualcomm and built base stations control software at Motorola. He holds a PhD in computing from Imperial College London. His research spans novel applications of symbolic execution, software reliability and easier testing of complex software systems.

Abstract: Symbolic PathFinder is a symbolic execution tool for java bytecode developed at NASA Ames. I will give an overview of the tool, highlighting some of its key features, such as handling of recursive data structures and multithreading, and describe some of its applications, e.g., to quantify information leakage for side-channel analysis and to estimate worst-case complexity analysis of software. I will also discuss future research directions and opportunities to enhance the tool, through the use of machine learning technologies

Bio: Corina Pasareanu is an ACM Fellow, working at NASA Ames. She is affiliated with KBR and 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). She has been serving as Program/General Chair for several conferences including: ICSE 2025, SEFM 2021, FM 2021, ICST 2020, ISSTA 2020, ESEC/FSE 2018, CAV 2015, ISSTA 2014, ASE 2011, and NFM 2009. She is on the steering committees for ICSE, ESEC/FSE and ISSTA conferences. She is currently an associate editor for IEEE TSE and for STTT, Springer Nature.