About

Scott A. Smolka is a Distinguished Professor in the Department of Computer Science at Stony Brook University. He earned his Ph.D. in Computer Science from Brown University in 1984, and holds both M.A. and B.A. degrees in Mathematics from Boston University, obtained in 1977 and 1975 respectively. His research interests include model checking, semantics of concurrency, CASE tools for safety-critical systems, and distributed languages and algorithms. Throughout his career, Smolka has received several awards recognizing his contributions to the field. He is a Fellow of the European Association of Theoretical Computer Science since 2016. Other notable honors include the Research Excellence Award from the Department of Computer Science at Stony Brook University in 2012, the Best Paper Award at the Second International Conference on Runtime Verification in 2011, and the President/Chancellor’s Award for Excellence in Scholarship and Creative Activities in 2009. Additionally, he received a Certificate of Appreciation from the department for his leadership role in celebrating the department’s 35th anniversary. His research projects encompass the Logic-Programming-Based Model Checking, High-Confidence Operating Systems (HCOS), the Center for Cyber-Security, and the Monte Carlo Software Model Checker, among others. Smolka is actively involved in teaching various courses within the computer science curriculum and contributes to the AI Innovation Institute at Stony Brook University.

Research topics

• Computer Science
• Parallel computing
• Algorithm

Selected publications

• Cumulative-Time Signal Temporal Logic

  ArXiv.org · 2025-04-14

  preprintOpen access

  Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and response time. However, STL's expressivity is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) that operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all time steps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove both their soundness and completeness properties. We provide an efficient online monitoring algorithm for both semantics. Finally, we show the applicability of CT-STL in two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.

  PublisherOA PDFDOI

• Enhanced File System Testing through Input and Output Coverage

  2025-08-28

  article

  Effective file system testing relies on coverage to detect bugs and enhance reliability. We analyzed real file system bugs and found a weak correlation between code coverage, the most commonly used metric, and test effectiveness; many bugs were in covered code but remained undetected. Our study also showed that covering diverse file system inputs and outputs---system call arguments and return values---can be key to detecting the majority of observed bugs.

  PublisherDOI

• Cumulative-Time Signal Temporal Logic

  ACM Transactions on Embedded Computing Systems · 2025-08-25 · 1 citations

  articleOpen access

  Signal Temporal Logic (STL) is a widely adopted specification language for Cyber-Physical Systems that can be used to express critical temporal requirements, such as system safety and response time. STL’s expressivity, however, is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) which operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all timesteps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove the soundness and completeness of the robustness semantics. We also provide an efficient online monitoring algorithm for both semantics. We demonstrate the utility of CT-STL via two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.

  PublisherOA PDFDOI

• An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems

  ArXiv.org · 2025-12-14

  preprintOpen accessSenior author

  Resiliency is the ability of a system to quickly recover from a violation (recoverability) and avoid future violations for as long as possible (durability). In the spatial setting, recoverability and durability (now known as persistency) are measured in units of distance. Like its temporal counterpart, spatial resiliency is of fundamental importance for Cyber-Physical Systems (CPS) and yet, to date, there is no widely agreed-upon formal treatment of spatial resiliency. We present a formal framework for reasoning about spatial resiliency in CPS. Our framework is based on the spatial fragment of STREL, which we refer to as SREL. In this framework, spatial resiliency is given a syntactic characterization in the form of a Spatial Resiliency Specification (SpaRS). An atomic predicate of SpaRS is called an S-atom. Given an arbitrary SREL formula $φ$, distance bounds $d_1, d_2$, the S-atom of $φ$, $S_{d_1, d_2} (φ)$, is the SREL formula $\negφR_{[0,d_1]} (φR_{[d_2, +\infty)}φ)$, specifying that recovery from a violation of $φ$ occurs within distance $d_1$ (recoverability), and subsequently that $φ$ be maintained along a route for a distance greater than $d_2$ (persistency). S-atoms can be combined using spatial STREL operators, allowing one to express composite resiliency specifications. We define a quantitative semantics for SpaRS in the form of a Spatial Resilience Value (SpaRV) function $σ$ and prove its soundness and completeness w.r.t. SREL's Boolean semantics. The $σ$-value for $S_{d_1,d_2}(φ)$ is a set of non-dominated (rec, per) pairs, quantifying recoverability and persistency, given that some routes may offer better recoverability while others better persistency. In addition, we design algorithms to evaluate SpaRV for SpaRS formulas. Finally, two case studies demonstrate the practical utility of our approach.

  PublisherOA PDFDOI

• Handling Open-Vocabulary Constructs in Formalizing Specifications: Retrieval-Augmented Parsing with Expert Knowledge

  ArXiv.org · 2025-09-10

  preprintOpen access

  We study the problem of Open-Vocabulary Constructs(OVCs) -- ones not known beforehand -- in the context of converting natural language (NL) specifications into formal languages (e.g., temporal logic or code). Models fare poorly on OVCs due to a lack of necessary knowledge a priori. In such situations, a domain expert can provide correct constructs at inference time based on their preferences or domain knowledge. Our goal is to effectively reuse this inference-time, expert-provided knowledge for future parses without retraining the model. We present dynamic knowledge-augmented parsing(DKAP), where in addition to the input sentence, the model receives (dynamically growing) expert knowledge as a key-value lexicon that associates NL phrases with correct OVC constructs. We propose ROLex, a retrieval-augmented parsing approach that uses this lexicon. A retriever and a generator are trained to find and use the key-value store to produce the correct parse. A key challenge lies in curating data for this retrieval-augmented parser. We utilize synthetic data generation and the data augmentation techniques on annotated (NL sentence, FL statement) pairs to train the augmented parser. To improve training effectiveness, we propose multiple strategies to teach models to focus on the relevant subset of retrieved knowledge. Finally, we introduce a new evaluation paradigm modeled after the DKAP problem and simulate the scenario across three formalization tasks (NL2LTL, NL2Code, and NL2CMD). Our evaluations show that DKAP is a difficult challenge, and ROLex helps improve the performance of baseline models by using dynamic expert knowledge effectively.

  PublisherOA PDFDOI

• In Situ Resilience Quantification for Microgrids

  2024-01-18

  other

  This chapter presents a formal method for quantifying the in situ resilience of a microgrid under disturbances. The key innovation is a Signal Temporal Logic-based approach to monitoring the microgrid state against operational specifications. The method does not require knowledge of the system topology and uses locally available data for in situ resilience quantification under varying operating conditions. Case studies verify the applicability of the in situ resilience analysis approach in real time and its superiority over existing methods.

  PublisherDOI

• Two Decades of Industrializing Formal Verification: The Reactis Story

  Lecture notes in computer science · 2024-10-12

  book-chapterSenior author
  PublisherDOI

• AI‐Grid: AI‐Enabled, Smart Programmable Microgrids

  2024-01-18

  otherOpen access

  This chapter introduces AI-Grid: Artificial Intelligence (AI) enabled, provably resilient networked microgrids. We present a programmable platform that integrates reliable AI modeling under uncertainty, reachability analysis, formal control, high-assurance software architectures, and cybersecurity technologies to enable scalable, autonomic, and ultra-resilient microgrids and networked microgrids. This platform has been developed in collaboration with the power industry and the defense sector and is being demonstrated in real-world microgrids.

  PublisherOA PDFDOI

• The black-box simplex architecture for runtime assurance of multi-agent CPS

  Innovations in Systems and Software Engineering · 2024-03-21 · 3 citations

  article
  PublisherDOI

• Flock-Formation Control of Multi-Agent Systems using Imperfect Relative Distance Measurements

  2024-05-13 · 1 citations

  article

  We present distributed distance-based control (DDC), a novel approach for controlling a multi-agent system, such that it achieves a desired formation, in a resource-constrained setting. Our controller is fully distributed and only requires local state-estimation and scalar measurements of inter-agent distances. It does not require an external localization system or inter-agent exchange of state information. Our approach uses spatial-predictive control (SPC), to optimize a cost function given strictly in terms of inter-agent distances and the distance to the target location. In DDC, each agent continuously learns and updates a very abstract model of the actual system, in the form of a dictionary of three independent key-value pairs $(\Delta \vec s,\Delta d)$, where ∆d is the partial derivative of the distance measurements along a spatial direction $\Delta \vec s$. This is sufficient for an agent to choose the best next action. We validate our approach by using DDC to control a collection of Crazyflie drones to achieve formation flight and reach a target while maintaining flock formation.

  PublisherDOI

Recent grants

• Collaborative Research: Next-Generation Model Checking and Abstract Interpretation With a Focus on Embedded Control and Systems Biology

  NSF · $1.9M · 2009–2015

• CPS: Frontier: Collaborative Research: Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems

  NSF · $1.1M · 2015–2024

• Closed-Loop Formal Verification of ICDs Using Cardiac Electrophysiological Models

  NSF · $162k · 2014–2019

Frequent coauthors

• Radu Grosu

  TU Wien

  133 shared

• Scott D. Stoller

  Stony Brook University

  53 shared

• C. R. Ramakrishnan

  52 shared

• Ezio Bartocci

  43 shared

• Rance Cleaveland

  University of Maryland, College Park

  34 shared

• Nicola Paoletti

  34 shared

• Michael Kifer

  Coherent (United States)

  33 shared

• Ashish Tiwari

  26 shared

Awards & honors

• Fellow of the European Association of Theoretical Computer S…
• Research Excellence Award, Department of Computer Science, S…
• Best Paper Award, Second International Conference on Runtime…
• 2008-2009 President/Chancellor’s Award for Excellence in Sch…
• Computer Science Department Certificate of Appreciation for…