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

Corina Pasareanu is an ACM Distinguished Scientist, 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.