Scott A. Smolka Career Highlights
---------------------------------
+ Joined Stony Brook's Computer Science Department in 1982, 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.
+ More than 184 publications, generating more than 6,900 citations.
+ PI/Co-PI on grants totaling more than $22M.
+ Lead PI on recently awarded $5M NSF multi-institutional grant on
Compositional, Approximate, and Quantitative Reasoning for Medical
Cyber-Physical Systems.
+ Lead PI on a recently submitted $50M NSF Science and Technology
preproposal involving 30 PIs from 14 institutions on Computational
Modeling and Analysis for Complex Systems.
+ 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.