Scott A. Smolka Career Highlights --------------------------------- + Joined Stony Brook's Computer Science Department in 1983, reaching rank of Full Professor in 1995. + Fundamental research contributions in a number of areas, including process algebra, model checking, probabilistic processes, flocking behavior, and modeling and analysis of cardiac cells and neural circuits. + Perhaps best known for the algorithm he and Paris Kanellakis invented for deciding bisimulation. This algorithm, which has come to be known as the K-S Relational Coarsest Partitioning algorithm, can be used to efficiently decide bisimulation equivalence, a cornerstone of Milner's CCS and other process-algebraic formalisms, in polynomial time. + Co-recipient, with Paris Kanellakis, of the 2021 Edsger W. Dijkstra Prize in Distributed Computing for the paper: CCS Expressions, Finite State Processes, and Three Problems of Equivalence, Information and Computation, Volume 86, Issue 1, pages 43-68, 1990. Further details are available from https://www.podc.org/2021-edsger-w-dijkstra-prize-in-distributed-computing/ + More than 200 publications, generating more than 10,000 citations. + PI/Co-PI on grants totaling more than $25M. + Lead PI on $5M NSF multi-institutional grant on Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems (2015-2022). Smolka is the Lead PI and Director of this CyberCardia NSF CPS Frontiers project. + President/Chancellor's Award for Excellence in Scholarship and Creative Activities; Computer Science Department Research Excellence Award; Best Paper award from 2011 Runtime Verification conference; Most Practical Paper Award from 2005 International Symposium on Practical Aspects of Declarative Languages. + Developed efficient algorithms for model checking, including: 1994 CAV paper with Oleg Sokolsky on first incremental algorithm for model checking; 1995 CAV paper with Sokolsky and on first local model-checking algorithm for real-time systems; 1994 LICS paper, with Sokolsky and Shipei Zhang were first on parallel complexity of model checking; 2005 TACAS paper with Radu Grosu describing first randomized, Monte Carlo algorithm for model checking; 2011 TACAS paper that introduced the problem of Model Repair for probabilistic systems. + Fundamental contributions in the areas of probabilistic process algebra and models of probabilistic processes, including: 1990 IFIP Conference paper with Giacalone & Jou on first probabilistic process algebra, PCCS, and associated notions of "epsilon bisimulation" and its metric space; 1995 I&C paper with Baeten & Jan Bergstra on first probabilistic version of ACP process algebra, including complete axiomatization of probabilistic bisimulation for finite-state processes; 1999 I&C paper with Cleaveland & Zwarico on testing preorder for probabilistic processes based on probability with which a process passes a tests; highly cite 1995 I&C paper with van Glabbeek & Steffen on Reactive, Generative, and Stratified Models of Probabilistic Processes; 1997 TCS paper with Wu & Stark on Probabilistic I/O Automata model of probabilistic processes. + Modeling and Analysis of Cardiac Cells and Neural Circuits: with Grosu et al. (2008 Journal of Systems Biology, 2009 TCS, 2007-2008 HSCC), introduced an efficient modeling framework for excitable cells based on Cycle-Linear Hybrid Automata: a new form of HA that exhibit linear behavior on a per-cycle basis, but whose overall behavior is nonlinear; in 2009 CACM paper, introduced spatial-logic model checking to specify and detect emergent behavior e.g. spiral waves; in CAV 2011, performed first automated formal analysis of a realistic cardiac cell model; in HSCC 2014-2015, used compositional reasoning in feedback-based biological setting, showing how the sodium & potassium channels of a detailed cardiac-cell model can be replaced with a much simpler approximately bisimilar Hodgkin-Huxley abstractions. Currently using model checking to formally verify experimentally observed properties of C. Elegans (roundworm) neural circuit for Tap Withdrawal.