Processes, Tasks, and Monitors: A Comparative Study of Concurrent Programming Primitives. - Peter Wegner; Scott A. Smolka (IEEE Trans. Software Eng., 1983)

On the Existence and Construction of Robust Communication Protocals for Unreliable Channels. - Saumya K. Debray; Ariel J. Frank; Scott A. Smolka (FSTTCS, 1984)

Polynomial-Time Analysis for a Class of Communicating processes. - Scott A. Smolka (Symposium on Programming, 1984)

Testing Protocol Robustness the CCS Way. - Scott A. Smolka; Ariel J. Frank; Saumya K. Debray (PSTV, 1984)

Report on the 6th international symposium on programming. - Scott A. Smolka (ACM SIGPLAN Notices, 1984)

A CCS semantics for NIL. - Scott A. Smolka; Robert E. Strom (Formal Description of Programming Concepts, 1987)

Fundamental Results for the Verification of Observational Equivalence: A Survey. - Tommaso Bolognesi; Scott A. Smolka (PSTV, 1987)

Distributed Algorithms for Tree Pattern Matching. - Gurdip Singh; Scott A. Smolka; I. V. Ramakrishnan (WDAG, 1987)

Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems. - Jawahar Malhotra; Robert M. Shapiro; Scott A. Smolka; Alessandro Giacalone (Specification and Verification of Concurrent Systems, 1988)

The Complexity of Reachability in Distributed Communicating Processes. - John H. Reif; Scott A. Smolka (Acta Informatica, 1988)

On the Analysis of Cooperation and Antagonism in Networks of Communicating Processes. - Paris C. Kanellakis; Scott A. Smolka (Algorithmica, 1988)

Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems. - Alessandro Giacalone; Scott A. Smolka (IEEE Trans. Software Eng., 1988)

Equivalences, Congruences, and Complete Axiomatizations for Probabilistic Processes. - Chi-Chang Jou; Scott A. Smolka (CONCUR, 1990)

A Completely Distributed and Message-Efficient Implementation of Synchronous Multiprocess Communication. - Yuh-Jzer Joung; Scott A. Smolka (ICPP (3), 1990)

Algebraic Reasoning for Probabilistic Concurrent Systems. - Alessandro Giacalone; Chi-Chang Jou; Scott A. Smolka (Programming Concepts and Methods, 1990)

Reactive, Generative, and Stratified Models of Probabilistic Processes - Rob J. van Glabbeek; Scott A. Smolka; Bernhard Steffen; Chris M. N. Tofts (LICS, 1990)

Data flow analysis of distributed communicating processes. - John H. Reif; Scott A. Smolka (Int. J. Parallel Program., 1990)

CCS Expressions, Finite State Processes, and Three Problems of Equivalence - Paris C. Kanellakis; Scott A. Smolka (Inf. Comput., 1990)

Axiomization Probabilistic Processes: ACP with Generative Probabililties (Extended Abstract). - Jos C. M. Baeten; Jan A. Bergstra; Scott A. Smolka (CONCUR, 1992)

Towards efficient parallelization of equivalence checking algorithms. - Shipei Zhang; Scott A. Smolka (FORTE, 1992)

Testing Preorders for Probabilistic Processes. - Rance Cleaveland; Scott A. Smolka; Amy E. Zwarico (ICALP, 1992)

OSP: An Environment for Operating System Projects. - Michael Kifer; Scott A. Smolka (ACM SIGOPS Oper. Syst. Rev., 1992)

Incremental Model Checking in the Modal Mu-Calculus. - Oleg Sokolsky; Scott A. Smolka (CAV, 1994)

A Compositional Semantics for Statecharts using Labeled Transition Systems. - Andrew C. Uselton; Scott A. Smolka (CONCUR, 1994)

Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes. - Shoji Yuen; Rance Cleaveland; Zeynep Dayar; Scott A. Smolka (CONCUR, 1994)

The Concurrency Factory - Practical Tools for Specification, Stimulation, Verification, and Implementation of Concurrent Systems. - Rance Cleaveland; Jayesh N. Gada; Philip M. Lewis; Scott A. Smolka; Oleg Sokolsky; Shipei Zhang (Specification of Parallel Algorithms, 1994)

On the Parallel Complexity of Model Checking in the Modal Mu-Calculus - Shipei Zhang; Oleg Sokolsky; Scott A. Smolka (LICS, 1994)

A Process Algebraic Semantics for Statecharts via State Refinement. - Andrew C. Uselton; Scott A. Smolka (PROCOMET, 1994)

On Randomization in Sequential and Distributed Algorithms. - Rajiv Gupta 002; Scott A. Smolka; Shaji Bhaskar (ACM Comput. Surv., 1994)

Coordinating First-Order Multiparty Interactions. - Yuh-Jzer Joung; Scott A. Smolka (ACM Trans. Program. Lang. Syst., 1994)

Local Model Checking for Real-Time Systems (Extended Abstract). - Oleg Sokolsky; Scott A. Smolka (CAV, 1995)

On the Computational Complexity of Bisimulation. - Faron Moller; Scott A. Smolka (ACM Comput. Surv., 1995)

Reactive, Generative and Stratified Models of Probabilistic Processes - Rob J. van Glabbeek; Scott A. Smolka; Bernhard Steffen (Inf. Comput., 1995)

Axiomatizing Probabilistic Processes: ACP with Generative Probabilities - Jos C. M. Baeten; Jan A. Bergstra; Scott A. Smolka (Inf. Comput., 1995)

The Concurrency Factory: A Development Environment for Concurrent Systems. - Rance Cleaveland; Philip M. Lewis; Scott A. Smolka; Oleg Sokolsky (CAV, 1996)

A Theory of Testing for Soft Real-Time Processes. - Rance Cleaveland; Insup Lee 001; Philip M. Lewis; Scott A. Smolka (SEKE, 1996)

The Concurrency Factory Software Development Environment. - Rance Cleaveland; Philip M. Lewis; Scott A. Smolka; Oleg Sokolsky (TACAS, 1996)

Strategic Directions in Concurrency Research. - Rance Cleaveland; Scott A. Smolka (ACM Comput. Surv., 1996)

Concurrency: Theory and Practice. - Rocco De Nicola; Scott A. Smolka (ACM Comput. Surv., 1996)

Strategic Directions in Computing Research-Concurrency Working Group Report. - Rance Cleaveland; Scott A. Smolka (Bull. EATCS, 1996)

Priority as Extremal Probability. - Scott A. Smolka; Bernhard Steffen (Formal Aspects Comput., 1996)

A Comprehensive Study of the Complexity of Multiparty Interaction. - Yuh-Jzer Joung; Scott A. Smolka (J. ACM, 1996)

Software Design, Specification, and Verification: Lessons Learned from the Rether Case Study. - Xiaoqun Du; Kevin T. McDonnell; Evangelos Nanos; Y. S. Ramakrishna; Scott A. Smolka (AMAST, 1997)

Efficient Model Checking Using Tabled Resolution. - Y. S. Ramakrishna; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka; Terrance Swift; David Scott Warren (CAV, 1997)

Partial-Order Reduction in the Weak Modal Mu-Calculus. - Y. S. Ramakrishna; Scott A. Smolka (CONCUR, 1997)

Composition and Behaviors of Probabilistic I/O Automata. - Sue-Hwey Wu; Scott A. Smolka; Eugene W. Stark (Theor. Comput. Sci., 1997)

Praobabilistic Resource Failure in Real-Time Process Algebra. - Anna Philippou; Rance Cleaveland; Insup Lee 001; Scott A. Smolka; Oleg Sokolsky (CONCUR, 1998)

Infinite Probabilistic and Nonprobabilistic Testing. - K. Narayan Kumar; Rance Cleaveland; Scott A. Smolka (FSTTCS, 1998)

Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract). - Xinxin Liu; Scott A. Smolka (ICALP, 1998)

Compositional Analysis of Expected Delays in Networks of Probabilistic I/O Automata. - Eugene W. Stark; Scott A. Smolka (LICS, 1998)

Logic Programming and Model Checking. - Baoqiu Cui; Yifei Dong; Xiaoqun Du; K. Narayan Kumar; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Abhik Roychoudhury; Scott A. Smolka; David Scott Warren (PLILP/ALP, 1998)

Fully Local and Efficient Evaluation of Alternating Fixed Points (Extended Abstract). - Xinxin Liu; C. R. Ramakrishnan 001; Scott A. Smolka (TACAS, 1998)

Tabulation-based Induction Proofs with Application to Automated Verification. - Abhik Roychoudhury; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka (TAPD, 1998)

Strong Interaction Fairness Via Randomization. - Yuh-Jzer Joung; Scott A. Smolka (IEEE Trans. Parallel Distributed Syst., 1998)

Faster Model Checking for Open Systems. - Madhavan Mukund; K. Narayan Kumar; Scott A. Smolka (ASIAN, 1999)

Practical Considerations in Protocol Verification: The E-2C Case Study. - Yifei Dong; Scott A. Smolka; Eugene W. Stark; Stephanie M. White (ICECCS, 1999)

Model Checking the Secure Electronic Transaction (SET) Protocol. - Shiyong Lu; Scott A. Smolka (MASCOTS, 1999)

Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. - Yifei Dong; Xiaoqun Du; Y. S. Ramakrishna; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka; Oleg Sokolsky; Eugene W. Stark; David Scott Warren (TACAS, 1999)

Testing Preorders for Probabilistic Processes. - Rance Cleaveland; Zeynep Dayar; Scott A. Smolka; Shoji Yuen (Inf. Comput., 1999)

Local Model Checking and Protocol Analysis. - Xiaoqun Du; Scott A. Smolka; Rance Cleaveland (Int. J. Softw. Tools Technol. Transf., 1999)

A complete axiom system for finite-state probabilistic processes. - Eugene W. Stark; Scott A. Smolka (Proof, Language, and Interaction, 2000)

XMC: A Logic-Programming-Based Verification Toolset. - C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka; Yifei Dong; Xiaoqun Du; Abhik Roychoudhury; V. N. Venkatakrishnan (CAV, 2000)

GCCS: A Graphical Coordination Language for System Specification. - Rance Cleaveland; Xiaoqun Du; Scott A. Smolka (COORDINATION, 2000)

Model Checking the Java Meta-Locking Algorithm. - Samik Basu 001; Scott A. Smolka; Orson R. Ward (ECBS, 2000)

Tabled Resolution + Constraints: A Recipe for Model Checking Real-Time Systems. - Xiaoqun Du; C. R. Ramakrishnan 001; Scott A. Smolka (RTSS, 2000)

Verification of Parameterized Systems Using Logic Program Transformations. - Abhik Roychoudhury; K. Narayan Kumar; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka (TACAS, 2000)

Real-Time Verification Techniques for Untimed Systems. - Xiaoqun Du; C. R. Ramakrishnan 001; Scott A. Smolka (MTCS, 2000)

Practical techniques for the design, specification, verification, and implementation of concurrent systems. - Rance Cleaveland; Philip M. Lewis; Scott A. Smolka (ACM SIGSOFT Softw. Eng. Notes, 2000)

Specification and evaluation of logic-based model checking. - C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka; David Scott Warren (ACM SIGSOFT Softw. Eng. Notes, 2000)

Finite-State Analysis of the CAN Bus Protocol. - Michiel van Osch; Scott A. Smolka (HASE, 2001)

Alternating Fixed Points in Boolean Equation Systems as Preferred Stable Models. - K. Narayan Kumar; C. R. Ramakrishnan 001; Scott A. Smolka (ICLP, 2001)

Automated Software Engineering Using Concurrent Class Machines. - Radu Grosu; Yanhong A. Liu; Scott A. Smolka; Scott D. Stoller; Jingyu Yan (ASE, 2001)

Model-Carrying Code (MCC): a new paradigm for mobile-code security. - R. Sekar 001; C. R. Ramakrishnan 001; I. V. Ramakrishnan; Scott A. Smolka (NSPW, 2001)

Turing Machines, Transition Systems, and Interaction. - Dina Q. Goldin; Scott A. Smolka; Peter Wegner (EXPRESS, 2001)

Hiding resources that can fail: An axiomatic perspective. - Anna Philippou; Oleg Sokolsky; Insup Lee 001; Rance Cleaveland; Scott A. Smolka (Inf. Process. Lett., 2001)

Vacuity Checking in the Modal Mu-Calculus. - Yifei Dong; Beata Sarna-Starosta; C. R. Ramakrishnan 001; Scott A. Smolka (AMAST, 2002)

High-confidence operating systems. - Radu Grosu; Erez Zadok; Scott A. Smolka; Rance Cleaveland; Yanhong A. Liu (ACM SIGOPS European Workshop, 2002)

On the Computational Complexity of Bisimulation, Redux. - Faron Moller; Scott A. Smolka (PCK50, 2003)

Evidence Explorer: A Tool for Exploring Model-Checking Proofs. - Yifei Dong; C. R. Ramakrishnan 001; Scott A. Smolka (CAV, 2003)

A Process-Algebraic Language for Probabilistic I/O Automata. - Eugene W. Stark; Rance Cleaveland; Scott A. Smolka (CONCUR, 2003)

Model Checking and Evidence Exploration. - Yifei Dong; C. R. Ramakrishnan 001; Scott A. Smolka (ECBS, 2003)

Generation of All Counter-Examples for Push-Down Systems. - Samik Basu 001; Diptikalyan Saha; Yow-Jian Lin; Scott A. Smolka (FORTE, 2003)

Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking. - Yifei Dong; Xiaoqun Du; Gerard J. Holzmann; Scott A. Smolka (Int. J. Softw. Tools Technol. Transf., 2003)

Localizing Program Errors for Cimple Debugging. - Samik Basu 001; Diptikalyan Saha; Scott A. Smolka (FORTE, 2004)

Quantitative Model checking. - Radu Grosu; Scott A. Smolka (ISoLA (Preliminary proceedings), 2004)

Turing machines, transition systems, and interaction. - Dina Q. Goldin; Scott A. Smolka; Paul C. Attie; Elaine L. Sonderegger (Inf. Comput., 2004)

On the computational complexity of bisimulation, redux. - Faron Moller; Scott A. Smolka; Jirí Srba (Inf. Comput., 2004)

Distributed prototyping from validated specifications. - David Hansel; Rance Cleaveland; Scott A. Smolka (J. Syst. Softw., 2004)

A logical encoding of the pi-calculus: model checking mobile processes using tabled resolution. - Ping Yang 002; C. R. Ramakrishnan 001; Scott A. Smolka (Int. J. Softw. Tools Technol. Transf., 2004)

Safety-Liveness Semantics for UML 2.0 Sequence Diagrams. - Radu Grosu; Scott A. Smolka (ACSD, 2005)

A Provably Correct Compiler for Efficient Model Checking of Mobile Processes. - Ping Yang 002; Yifei Dong; C. R. Ramakrishnan 001; Scott A. Smolka (PADL, 2005)

Monte Carlo Model Checking. - Radu Grosu; Scott A. Smolka (TACAS, 2005)

FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. - Curtis W. Keller; Diptikalyan Saha; Samik Basu 001; Scott A. Smolka (TACAS, 2005)

Open-Source Model Checking. - Radu Grosu; Xiaowan Huang; Sumit Jain; Scott A. Smolka (SoftMC@CAV, 2005)

Monte Carlo Methods for Process Algebra. - Radu Grosu; Scott A. Smolka (APC 25, 2005)

Preface. - Jirí Srba; Scott A. Smolka (INFINITY, 2005)

An Instrumentation-Based Approach to Controller Model Validation. - Rance Cleaveland; Scott A. Smolka; Steve Sims (ASWSD, 2006)

Probabilistic I/O Automata: Theories of Two Equivalences. - Eugene W. Stark; Rance Cleaveland; Scott A. Smolka (CONCUR, 2006)

Efficient Event-Driven Simulation of Excitable Hybrid Automata. - Mike R. True; Emilia Entcheva; Scott A. Smolka; Pei Ye; Radu Grosu (EMBC, 2006)

A Cycle-Linear Approach to Modeling Action Potentials. - Pei Ye; Emilia Entcheva; Scott A. Smolka; Mike R. True; Radu Grosu (EMBC, 2006)

Hybrid Automata as a Unifying Framework for Modeling Excitable Cells. - Pei Ye; Emilia Entcheva; Scott A. Smolka; Mike R. True; Radu Grosu (EMBC, 2006)

Compiler-assisted software verification using plug-ins. - Sean Callanan; Radu Grosu; Xiaowan Huang; Scott A. Smolka; Erez Zadok (IPDPS, 2006)

Deep Random Search for Efficient Model Checking of Timed Automata. - Radu Grosu; Xiaowan Huang; Scott A. Smolka; Wenkai Tan; Stavros Tripakis (Monterey Workshop, 2006)

Runtime Verification for High-Confidence Systems: A Monte Carlo Approach. - Sean Callanan; Radu Grosu; Abhishek Rai; Scott A. Smolka; Mike R. True; Erez Zadok (MBT, 2006)

Learning Cycle-Linear Hybrid Automata for Excitable Cells. - Radu Grosu; Sayan Mitra; Pei Ye; Emilia Entcheva; I. V. Ramakrishnan; Scott A. Smolka (HSCC, 2007)

Model Predictive Control for Memory Profiling. - Sean Callanan; Radu Grosu; Justin Seyster; Scott A. Smolka; Erez Zadok (IPDPS, 2007)

Spatial Networks of Hybrid I/O Automata for Modeling Excitable Tissue. - Ezio Bartocci; Flavio Corradini; Maria Rita Di Berardini; Emilia Entcheva; Radu Grosu; Scott A. Smolka (FBTC@CONCUR, 2007)

Model checking the Java metalocking algorithm. - Samik Basu 001; Scott A. Smolka (ACM Trans. Softw. Eng. Methodol., 2007)

Introduction to Operating System Design and Implementation - The OSP 2 Approach. - Michael Kifer; Scott A. Smolka (Springer, 2007)

StonyCam: A Formal Framework for Modeling, Analyzing and Regulating Cardiac Myocytes. - Ezio Bartocci; Flavio Corradini; Radu Grosu; Emanuela Merelli; Oliviero Riganelli; Scott A. Smolka (Concurrency, Graphs and Models, 2008)

Formal Analysis of Abnormal Excitation in Cardiac Tissue. - Pei Ye; Radu Grosu; Scott A. Smolka; Emilia Entcheva (CMSB, 2008)

Power Optimization in Fault-Tolerant Mobile Ad Hoc Networks. - Oliviero Riganelli; Radu Grosu; Samir R. Das; C. R. Ramakrishnan 001; Scott A. Smolka (HASE, 2008)

Software monitoring with bounded overhead. - Sean Callanan; David J. Dean; Michael Gorbovitski; Radu Grosu; Justin Seyster; Scott A. Smolka; Scott D. Stoller; Erez Zadok (IPDPS, 2008)

Power Optimization in Fault-Tolerant MANETs. - Oliviero Riganelli; Radu Grosu; Scott A. Smolka (MASCOTS, 2008)

CellExcite: an efficient simulation environment for excitable cells. - Ezio Bartocci; Flavio Corradini; Emilia Entcheva; Radu Grosu; Scott A. Smolka (BMC Bioinform., 2008)

Query-Based Model Checking of Ad Hoc Network Protocols. - Anu Singh; C. R. Ramakrishnan 001; Scott A. Smolka (CONCUR, 2009)

Dynamic Path Reduction for Software Model Checking. - Zijiang Yang 006; Bashar Al-Rawi; Karem A. Sakallah; Xiaowan Huang; Scott A. Smolka; Radu Grosu (IFM, 2009)

Learning and detecting emergent behavior in networks of cardiac myocytes. - Radu Grosu; Scott A. Smolka; Flavio Corradini; Anita Wasilewska; Emilia Entcheva; Ezio Bartocci (Commun. ACM, 2009)

Modeling and simulation of cardiac tissue using hybrid I/O automata. - Ezio Bartocci; Flavio Corradini; Maria Rita Di Berardini; Emilia Entcheva; Scott A. Smolka; Radu Grosu (Theor. Comput. Sci., 2009)

Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking. - Nikolaos Alexiou 001; Stylianos Basagiannis; Panagiotis Katsaros; Tushar Deshpande; Scott A. Smolka (HASE, 2010)

Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol. - Xiaowan Huang; Anu Singh; Scott A. Smolka (NASA Formal Methods, 2010)

Aspect-Oriented Instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (RV, 2010)

A process calculus for Mobile Ad Hoc Networks. - Anu Singh; C. R. Ramakrishnan 001; Scott A. Smolka (Sci. Comput. Program., 2010)

From Cardiac Cells to Genetic Regulatory Networks. - Radu Grosu; Grégory Batt; Flavio H. Fenton; James Glimm; Colas Le Guernic; Scott A. Smolka; Ezio Bartocci (CAV, 2011)

Toward real-time simulation of cardiac dynamics. - Ezio Bartocci; Elizabeth Cherry; James Glimm; Radu Grosu; Scott A. Smolka; Flavio H. Fenton (CMSB, 2011)

Curvature analysis of cardiac excitation wavefronts. - Abhishek Murthy; Ezio Bartocci; Flavio H. Fenton; James Glimm; Richard A. Gray; Scott A. Smolka; Radu Grosu (CMSB, 2011)

Model discovery for energy-aware computing systems: An experimental evaluation. - Zhichao Li; Radu Grosu; Koundinya Muppalla; Scott A. Smolka; Scott D. Stoller; Erez Zadok (IGCC, 2011)

Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking. - Tushar Deshpande; Panagiotis Katsaros; Stylianos Basagiannis; Scott A. Smolka (HASE, 2011)

Runtime Verification with State Estimation. - Scott D. Stoller; Ezio Bartocci; Justin Seyster; Radu Grosu; Klaus Havelund; Scott A. Smolka; Erez Zadok (RV, 2011)

A Change of Perspective Yields Formal Analysis. - Radu Grosu; Flavio H. Fenton; Scott A. Smolka; Ezio Bartocci (SEW, 2011)

On the energy consumption and performance of systems software. - Zhichao Li; Radu Grosu; Priya Sehgal; Scott A. Smolka; Scott D. Stoller; Erez Zadok (SYSTOR, 2011)

Model Repair for Probabilistic Systems. - Ezio Bartocci; Radu Grosu; Panagiotis Katsaros; C. R. Ramakrishnan 001; Scott A. Smolka (TACAS, 2011)

Using integer clocks to verify clock-synchronization protocols. - Xiaowan Huang; Anu Singh; Scott A. Smolka (Innov. Syst. Softw. Eng., 2011)

On Temporal Logic and Signal Processing. - Alexandre Donzé; Oded Maler; Ezio Bartocci; Dejan Nickovic; Radu Grosu; Scott A. Smolka (ATVA, 2012)

Approximate Bisimulations for Sodium Channel Dynamics. - Abhishek Murthy; Md. Ariful Islam; Ezio Bartocci; Elizabeth Cherry; Flavio H. Fenton; James Glimm; Scott A. Smolka; Radu Grosu (CMSB, 2012)

Adaptive Runtime Verification. - Ezio Bartocci; Radu Grosu; Atul Karmarkar; Scott A. Smolka; Scott D. Stoller; Erez Zadok; Justin Seyster (RV, 2012)

InterAspect: aspect-oriented instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (Formal Methods Syst. Des., 2012)

Software monitoring with controllable overhead. - Xiaowan Huang; Justin Seyster; Sean Callanan; Ketan Dixit; Radu Grosu; Scott A. Smolka; Scott D. Stoller; Erez Zadok (Int. J. Softw. Tools Technol. Transf., 2012)

Model checking with probabilistic tabled logic programming. - Andrey Gorlin; C. R. Ramakrishnan 001; Scott A. Smolka (Theory Pract. Log. Program., 2012)

Runtime Verification with Particle Filtering. - Kenan Kalajdzic; Ezio Bartocci; Scott A. Smolka; Scott D. Stoller; Radu Grosu (RV, 2013)

Curvature Analysis of Cardiac Excitation Wavefronts. - Abhishek Murthy; Ezio Bartocci; Flavio H. Fenton; James Glimm; Richard A. Gray; Elizabeth Cherry; Scott A. Smolka; Radu Grosu (IEEE ACM Trans. Comput. Biol. Bioinform., 2013)

Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking. - Tushar Deshpande; Panagiotis Katsaros; Scott A. Smolka; Scott D. Stoller (EDCC, 2014)

Compositional Branching-Time Measurements. - Radu Grosu; Doron A. Peled; C. R. Ramakrishnan 001; Scott A. Smolka; Scott D. Stoller; Junxing Yang (FPS@ETAPS, 2014)

Compositionality results for cardiac cell dynamics. - Md. Ariful Islam; Abhishek Murthy; Antoine Girard; Scott A. Smolka; Radu Grosu (HSCC, 2014)

Medical Cyber-Physical Systems - (Track Introduction). - Ezio Bartocci; Sicun Gao; Scott A. Smolka (ISoLA (2), 2014)

Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices. - Radu Grosu; Elizabeth Cherry; Edmund M. Clarke; Rance Cleaveland; Sanjay Dixit; Flavio H. Fenton; Sicun Gao; James Glimm; Richard A. Gray; Rahul Mangharam; Arnab Ray; Scott A. Smolka (ISoLA (2), 2014)

Using Statistical Model Checking for Measuring Systems. - Radu Grosu; Doron A. Peled; C. R. Ramakrishnan 001; Scott A. Smolka; Scott D. Stoller; Junxing Yang (ISoLA (2), 2014)

Towards a GPGPU-parallel SPIN model checker. - Ezio Bartocci; Richard DeFrancisco; Scott A. Smolka (SPIN, 2014)

Hybrid Systems and Biology. - Ezio Bartocci; Luca Bortolussi; Scott A. Smolka (Inf. Comput., 2014)

Neural Programming: Towards adaptive control in Cyber-Physical Systems. - Konstantin Selyunin; Denise Ratasich; Ezio Bartocci; Md. Ariful Islam; Scott A. Smolka; Radu Grosu (CDC, 2015)

Model Checking Tap Withdrawal in C. Elegans. - Md. Ariful Islam; Richard DeFrancisco; Chuchu Fan; Radu Grosu; Sayan Mitra; Scott A. Smolka (HSB, 2015)

Computing bisimulation functions using SOS optimization and δ-decidability over the reals. - Abhishek Murthy; Md. Ariful Islam; Scott A. Smolka; Radu Grosu (HSCC, 2015)

Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information About the Environment. - Dung T. Phan; Junxing Yang; Denise Ratasich; Radu Grosu; Scott A. Smolka; Scott D. Stoller (RV, 2015)

Abstract Model Repair. - George Chatzieleftheriou; Borzoo Bonakdarpour; Panagiotis Katsaros; Scott A. Smolka (Log. Methods Comput. Sci., 2015)

A survey on unmanned aerial vehicle collision avoidance systems. - Hung Pham; Scott A. Smolka; Scott D. Stoller; Dung T. Phan; Junxing Yang (CoRR, 2015)

Model-order reduction of ion channel dynamics using approximate bisimulation. - Md. Ariful Islam; Abhishek Murthy; Ezio Bartocci; Elizabeth Cherry; Flavio H. Fenton; James Glimm; Scott A. Smolka; Radu Grosu (Theor. Comput. Sci., 2015)

CyberCardia project: Modeling, verification and validation of implantable cardiac devices. - Md. Ariful Islam; Hyun-Kyung Lim; Nicola Paoletti; Houssam Abbas; Zhihao Jiang; Jacek Cyranka; Rance Cleaveland; Sicun Gao; Edmund M. Clarke; Radu Grosu; Rahul Mangharam; Elizabeth Cherry; et al. (BIBM, 2016)

Bifurcation Analysis of Cardiac Alternans Using delta -Decidability. - Md. Ariful Islam; Greg Byrne; Soonho Kong; Edmund M. Clarke; Rance Cleaveland; Flavio H. Fenton; Radu Grosu; Paul L. Jones; Scott A. Smolka (CMSB, 2016)

Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control. - Junxing Yang; Radu Grosu; Scott A. Smolka; Ashish Tiwari 001 (CONCUR, 2016)

Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans. - Md. Ariful Islam; Qinsi Wang; Ramin M. Hasani; Ondrej Balun; Edmund M. Clarke; Radu Grosu; Scott A. Smolka (HLDVT, 2016)

Feedback Control for Statistical Model Checking of Cyber-Physical Systems. - Kenan Kalajdzic; Cyrille Jégourel; Anna Lukina; Ezio Bartocci; Axel Legay; Scott A. Smolka; Radu Grosu (ISoLA (1), 2016)

Regular Expressions for Irregular Rhythms. - Houssam Abbas; Alëna Rodionova; Ezio Bartocci; Scott A. Smolka; Radu Grosu (CoRR, 2016)

EATCS Fellows' Advice to the Young Theoretical Computer Scientist. - Luca Aceto; Mariangiola Dezani-Ciancaglini; Yuri Gurevich; David Harel; Monika Henzinger; Giuseppe F. Italiano; Scott A. Smolka; Paul G. Spirakis; Wolfgang Thomas (Bull. EATCS, 2016)

A Component-Based Simplex Architecture for High-Assurance Cyber-Physical Systems. - Dung T. Phan; Junxing Yang; Matthew Clark; Radu Grosu; John D. Schierman; Scott A. Smolka; Scott D. Stoller (ACSD, 2017)

Attacking the V: On the Resiliency of Adaptive-Horizon MPC. - Ashish Tiwari 001; Scott A. Smolka; Lukas Esterle; Anna Lukina; Junxing Yang; Radu Grosu (ATVA, 2017)

Lagrangian Reachabililty. - Jacek Cyranka; Md. Ariful Islam; Greg Byrne; Paul L. Jones; Scott A. Smolka; Radu Grosu (CAV (1), 2017)

Quantitative Regular Expressions for Arrhythmia Detection Algorithms. - Houssam Abbas; Alëna Rodionova; Ezio Bartocci; Scott A. Smolka; Radu Grosu (CMSB, 2017)

Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties. - Nicola Paoletti; Kin Sum Liu; Scott A. Smolka; Shan Lin 001 (CMSB, 2017)

SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems. - Fedor Shmarov; Nicola Paoletti; Ezio Bartocci; Shan Lin 001; Scott A. Smolka; Paolo Zuliani (Haifa Verification Conference, 2017)

A Simplex Architecture for Hybrid Systems Using Barrier Certificates. - Junxing Yang; Md. Ariful Islam; Abhishek Murthy; Scott A. Smolka; Scott D. Stoller (SAFECOMP, 2017)

ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - Anna Lukina; Lukas Esterle; Christian Hirsch; Ezio Bartocci; Junxing Yang; Ashish Tiwari 001; Scott A. Smolka; Radu Grosu (TACAS (2), 2017)

Model Checking Cyber-Physical Systems using Particle Swarm Optimization. - Dung T. Phan; Scott A. Smolka; Radu Grosu; Usama Mehmood; Scott D. Stoller; Junxing Yang (CoRR, 2017)

Automated Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems. - Fedor Shmarov; Nicola Paoletti; Ezio Bartocci; Shan Lin 001; Scott A. Smolka; Paolo Zuliani (CoRR, 2017)

How to Learn a Model Checker. - Dung T. Phan; Radu Grosu; Nicola Paoletti; Scott A. Smolka; Scott D. Stoller (CoRR, 2017)

Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles. - Dung T. Phan; Junxing Yang; Radu Grosu; Scott A. Smolka; Scott D. Stoller (Formal Methods Syst. Des., 2017)

Tight Continuous-Time Reachtubes for Lagrangian Reachability. - Jacek Cyranka; Md. Ariful Islam; Scott A. Smolka; Sicun Gao; Radu Grosu (CDC, 2018)

Resilient Control and Safety for Cyber-Physical Systems. - Anna Lukina; Ashish Tiwari 001; Scott A. Smolka; Lukas Esterle; Junxing Yang; Radu Grosu (MT@CPSWeek, 2018)

Declarative vs rule-based control for flocking dynamics. - Usama Mehmood; Nicola Paoletti; Dung T. Phan; Radu Grosu; Shan Lin 001; Scott D. Stoller; Ashish Tiwari 001; Junxing Yang; Scott A. Smolka (SAC, 2018)

Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems. - Anna Lukina; Ashish Tiwari 001; Scott A. Smolka; Radu Grosu (CoRR, 2018)

Process Algebra and Model Checking. - Rance Cleaveland; A. W. Roscoe 001; Scott A. Smolka (Handbook of Model Checking, 2018)

Committed Moving Horizon Estimation for Meal Detection and Estimation in Type 1 Diabetes. - Hongkai Chen 001; Nicola Paoletti; Scott A. Smolka; Shan Lin 001 (ACC, 2019)

Under the Hood of a Stand-Alone Lagrangian Reachability Tool. - Sophie Gruenbacher; Jacek Cyranka; Md. Ariful Islam; Max Tschaikowski; Scott A. Smolka; Radu Grosu (ARCH@CPSIoTWeek, 2019)

Synthesizing stealthy reprogramming attacks on cardiac devices. - Nicola Paoletti; Zhihao Jiang; Md. Ariful Islam; Houssam Abbas; Rahul Mangharam; Shan Lin 001; Zachary Gruber; Scott A. Smolka (ICCPS, 2019)

Neural Predictive Monitoring. - Luca Bortolussi; Francesca Cairoli; Nicola Paoletti; Scott A. Smolka; Scott D. Stoller (RV, 2019)

Distributed adaptive-neighborhood control for stochastic reachability in multi-agent systems. - Anna Lukina; Ashish Tiwari 001; Scott A. Smolka; Radu Grosu (SAC, 2019)

Neural state classification for hybrid systems. - Dung T. Phan; Nicola Paoletti; Timothy Zhang; Radu Grosu; Scott A. Smolka; Scott D. Stoller (SNR, 2019)

Quantitative Regular Expressions for Arrhythmia Detection. - Houssam Abbas; Alëna Rodionova; Konstantinos Mamouras; Ezio Bartocci; Scott A. Smolka; Radu Grosu (IEEE ACM Trans. Comput. Biol. Bioinform., 2019)

Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans. - Md. Ariful Islam; Rance Cleaveland; Flavio H. Fenton; Radu Grosu; Paul L. Jones; Scott A. Smolka (Theor. Comput. Sci., 2019)

Statistical Model Checking. - Axel Legay; Anna Lukina; Louis-Marie Traonouez; Junxing Yang; Scott A. Smolka; Radu Grosu (Computing and Software Science, 2019)

Learning Distributed Controllers for V-Formation. - Shouvik Roy; Usama Mehmood; Radu Grosu; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001 (ACSOS, 2020)

Lagrangian Reachtubes: The Next Generation. - Sophie Gruenbacher; Jacek Cyranka; Mathias Lechner; Md. Ariful Islam; Scott A. Smolka; Radu Grosu (CDC, 2020)

Neural Flocking: MPC-Based Supervised Learning of Flocking Controllers. - Usama Mehmood; Shouvik Roy; Radu Grosu; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001 (FoSSaCS, 2020)

Neural Simplex Architecture. - Dung T. Phan; Radu Grosu; Nils Jansen 001; Nicola Paoletti; Scott A. Smolka; Scott D. Stoller (NFM, 2020)

Bayesian Neural Predictive Monitoring. - Luca Bortolussi; Francesca Cairoli; Nicola Paoletti; Scott A. Smolka; Scott D. Stoller (OVERLAY, 2020)

Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems. - Fedor Shmarov; Sadegh Soudjani; Nicola Paoletti; Ezio Bartocci; Shan Lin 001; Scott A. Smolka; Paolo Zuliani (IEEE Access, 2020)

V-Formation via Model Predictive Control. - Radu Grosu; Anna Lukina; Scott A. Smolka; Ashish Tiwari 001; Vasudha Varadarajan; Xingfang Wang (CoRR, 2020)

MPC-guided Imitation Learning of Neural Network Policies for the Artificial Pancreas. - Hongkai Chen 001; Nicola Paoletti; Scott A. Smolka; Shan Lin 001 (CoRR, 2020)

Swarm model checking on the GPU. - Richard DeFrancisco; Shenghsun Cho; Michael Ferdman; Scott A. Smolka (Int. J. Softw. Tools Technol. Transf., 2020)

Data-Driven Robust Control for a Closed-Loop Artificial Pancreas. - Nicola Paoletti; Kin Sum Liu; Hongkai Chen 001; Scott A. Smolka; Shan Lin 001 (IEEE ACM Trans. Comput. Biol. Bioinform., 2020)

On the Verification of Neural ODEs with Stochastic Guarantees. - Sophie Gruenbacher; Ramin M. Hasani; Mathias Lechner; Jacek Cyranka; Scott A. Smolka; Radu Grosu (AAAI, 2021)

Distributed Control for Flocking Maneuvers via Acceleration-Weighted Neighborhooding. - Shouvik Roy; Usama Mehmood; Radu Grosu; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001 (ACC, 2021)

Collision-Free 3D Flocking Using the Distributed Simplex Architecture. - Usama Mehmood; Scott D. Stoller; Radu Grosu; Scott A. Smolka (Formal Methods in Outer Space, 2021)

MPC-guided Imitation Learning of Bayesian Neural Network Policies for the Artificial Pancreas. - Hongkai Chen 001; Nicola Paoletti; Scott A. Smolka; Shan Lin 001 (CDC, 2021)

Interactive 3D Human Heart Simulations on Segmented Human MRI Hearts. - John P. Berman; Abouzar Kaboudian; Ilija Uzelac; Shahriar Iravanian; Tinen L. Iles; Paul A. Iaizzo; Hyun-Kyung Lim; Scott A. Smolka; James Glimm; Elizabeth M. Cherry; Flavio H. Fenton (CinC, 2021)

Safe CPS from unsafe controllers. - Usama Mehmood; Stanley Bak; Scott A. Smolka; Scott D. Stoller (CAADCPS@CPSIoTWeek, 2021)

Model-Checking Support for File System Development. - Wei Su; Yifei Liu; Gomathi Ganesan; Gerard J. Holzmann; Scott A. Smolka; Erez Zadok; Geoff Kuenning (HotStorage, 2021)

GoTube: Scalable Stochastic Verification of Continuous-Depth Models. - Sophie Gruenbacher; Mathias Lechner; Ramin M. Hasani; Daniela Rus; Thomas A. Henzinger; Scott A. Smolka; Radu Grosu (CoRR, 2021)

Kanellakis-Smolka 1983: A Convolution of Circumstances. - Scott A. Smolka (SIGACT News, 2021)

Neural predictive monitoring and a comparison of frequentist and Bayesian approaches. - Luca Bortolussi; Francesca Cairoli; Nicola Paoletti; Scott A. Smolka; Scott D. Stoller (Int. J. Softw. Tools Technol. Transf., 2021)

GoTube: Scalable Statistical Verification of Continuous-Depth Models. - Sophie A. Gruenbacher; Mathias Lechner; Ramin M. Hasani; Daniela Rus; Thomas A. Henzinger; Scott A. Smolka; Radu Grosu (AAAI, 2022)

An STL-Based Formulation of Resilience in Cyber-Physical Systems. - Hongkai Chen 001; Shan Lin 001; Scott A. Smolka; Nicola Paoletti (FORMATS, 2022)

Towards Drone Flocking Using Relative Distance Measurements. - Andreas Brandstätter; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001; Radu Grosu (ISoLA (3), 2022)

SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications. - Sayontan Ghosh; Amanpreet Singh; Alex Merenstein; Wei Su; Scott A. Smolka; Erez Zadok; Niranjan Balasubramanian (LREC, 2022)

The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS. - Usama Mehmood; Sanaz Sheikhi; Stanley Bak; Scott A. Smolka; Scott D. Stoller (NFM, 2022)

A Barrier Certificate-Based Simplex Architecture with Application to Microgrids. - Amol Damare; Shouvik Roy; Scott A. Smolka; Scott D. Stoller (RV, 2022)

Runtime-Assured, Real-Time Neural Control of Microgrids. - Amol Damare; Shouvik Roy; Scott A. Smolka; Scott D. Stoller (CoRR, 2022)

Multi-Agent Spatial Predictive Control with Application to Drone Flocking (Extended Version). - Andreas Brandstätter; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001; Radu Grosu (CoRR, 2022)

Input and Output Coverage Needed in File System Testing. - Yifei Liu; Gautam Ahuja; Geoff Kuenning; Scott A. Smolka; Erez Zadok (HotStorage, 2023)

An STL-based Approach to Resilient Control for Cyber-Physical Systems. - Hongkai Chen 001; Scott A. Smolka; Nicola Paoletti; Shan Lin 001 (HSCC, 2023)

Multi-Agent Spatial Predictive Control with Application to Drone Flocking. - Andreas Brandstätter; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001; Radu Grosu (ICRA, 2023)

Synthesizing Pareto-Optimal Signal-Injection Attacks on ICDs. - Veena Krish; Nicola Paoletti; Scott A. Smolka; Amir Rahmati (IEEE Access, 2023)

A distributed simplex architecture for multi-agent systems. - Usama Mehmood; Shouvik Roy; Amol Damare; Radu Grosu; Scott A. Smolka; Scott D. Stoller (J. Syst. Archit., 2023)

Metis: File System Model Checking via Versatile Input and State Exploration. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (FAST, 2024)

Flock-Formation Control of Multi-Agent Systems using Imperfect Relative Distance Measurements. - Andreas Brandstätter; Scott A. Smolka; Scott D. Stoller; Ashish Tiwari 001; Radu Grosu (ICRA, 2024)

Two Decades of Industrializing Formal Verification: The Reactis Story. - Rance Cleaveland; David Hansel; Steve Sims; Scott A. Smolka (SPIN, 2024)

Biosignal Authentication Considered Harmful Today. - Veena Krish; Nicola Paoletti; Milad Kazemi; Scott A. Smolka; Amir Rahmati (USENIX Security Symposium, 2024)

Fault diagnosis of Discrete Event Systems under uncertain initial conditions. - Ali Karimoddini; Scott A. Smolka; Mohammad Karimadini (Expert Syst. Appl., 2024)

Artifact Package: the Metis File System Model Checking Framework. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (Zenodo, 2024)

Artifact Package: the RefFS Reference File System for the Metis Model Checking Framework. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (Zenodo, 2024)

Cumulative-Time Signal Temporal Logic. - Hongkai Chen 001; Zeyu Zhang; Shouvik Roy; Ezio Bartocci; Scott A. Smolka; Scott D. Stoller; Shan Lin 001 (CoRR, 2025)

The black-box simplex architecture for runtime assurance of multi-agent CPS. - Sanaz Sheikhi; Usama Mehmood; Stanley Bak; Scott A. Smolka; Scott D. Stoller (Innov. Syst. Softw. Eng., 2025)