| 2024 | ECOOP | Qafny: A Quantum-Program Verifier. | Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu |
| 2020 | FMICS | Temporal-Logic Query Checking over Finite Data Streams. | Samuel Huang, Rance Cleaveland |
| 2018 | ISoLA | Programming Is Modeling. | Rance Cleaveland |
| 2018 | SEFM | Automated Specification Extraction and Analysis with Specstractor. | Christoph Schulze, Rance Cleaveland, Mikael Lindvall |
| 2017 | FMICS | Query Checking for Linear Temporal Logic. | Samuel Huang, Rance Cleaveland |
| 2016 | ISSRE | Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus. | Dharmalingam Ganesan, Mikael Lindvall, Stefan Hafsteinsson, Rance Cleaveland, Susanne L. Strege, Walter Moleski |
| 2015 | MODELS | UML-VT: A Formal Verification Environment for UML Activity Diagrams. | Zamira Daw, John Mangino, Rance Cleaveland |
| 2015 | SEFM | An Extensible Operational Semantics for UML Activity Diagrams. | Zamira Daw, Rance Cleaveland |
| 2014 | FOSSACS | Generalized Synchronization Trees. | James Ferlez, Rance Cleaveland, Steven I. Marcus |
| 2014 | ICSE | Assessing model-based testing: an empirical study conducted in industry. | Christoph Schulze, Dharmalingam Ganesan, Mikael Lindvall, Rance Cleaveland, Daniel Goldman |
| 2014 | ISoLA | 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 |
| 2013 | ICSE | Constructing safety assurance cases for medical devices. | Arnab Ray, Rance Cleaveland |
| 2011 | FMCAD | Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems. | Peter Fontana, Rance Cleaveland |
| 2010 | RV | Automatic Requirement Extraction from Test Cases. | Christopher Ackermann, Rance Cleaveland, Samuel Huang, Arnab Ray, Charles P. Shelton, Elizabeth Latronico |
| 2009 | ISSRE | Towards Behavioral Reflexion Models. | Christopher Ackermann, Mikael Lindvall, Rance Cleaveland |
| 2008 | FMICS | Model-Based Verification of Automotive Control Software. | Rance Cleaveland |
| 2007 | TACAS | THERE AND BACK AGAIN: Lessons Learned on the Way to the Market. | Rance Cleaveland |
| 2006 | COMPSAC | A Software Architectural Approach to Security by Design. | Arnab Ray, Rance Cleaveland |
| 2006 | CONCUR | Probabilistic I/O Automata: Theories of Two Equivalences. | Eugene W. Stark, Rance Cleaveland, Scott A. Smolka |
| 2005 | FORTE | Fast Generic Model-Checking for Data-Based Systems. | Dezhuang Zhang, Rance Cleaveland |
| 2005 | ICDCIT | Executable Requirements Specifications Using Triggered Message Sequence Charts. | Bikram Sengupta, Rance Cleaveland |
| 2005 | IFM | An Integrated Framework for Scenarios and State Machines. | Bikram Sengupta, Rance Cleaveland |
| 2005 | RTSS | Fast On-the-Fly Parametric Real-Time Model Checking. | Dezhuang Zhang, Rance Cleaveland |
| 2004 | ICDCIT | Secure Requirements Elicitation Through Triggered Message Sequence Charts. | Arnab Ray, Bikram Sengupta, Rance Cleaveland |
| 2003 | CAV | TRIM: A Tool for Triggered Message Sequence Charts. | Bikram Sengupta, Rance Cleaveland |
| 2003 | CONCUR | A Process-Algebraic Language for Probabilistic I/O Automata. | Eugene W. Stark, Rance Cleaveland, Scott A. Smolka |
| 2003 | ICSE | Architectural Interaction Diagrams: AIDs for System Modeling. | Arnab Ray, Rance Cleaveland |
| 2003 | RE | Refinement-Based Requirements Modeling Using TriggeredMessage Sequence Charts. | Bikram Sengupta, Rance Cleaveland |
| 2003 | TACAS | The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. | Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark |
| 2002 | CAV | Evidence-Based Model Checking. | Li Tan, Rance Cleaveland |
| 2001 | CAV | Efficient Model Checking Via Bchi Tableau Automata. | Girish Bhat, Rance Cleaveland, Alex Groce |
| 2001 | RSP | Distributed Prototyping from Validated Specifications. | David Hansel, Rance Cleaveland, Scott A. Smolka |
| 2001 | TACAS | Simulation Revisited. | Li Tan, Rance Cleaveland |
| 2000 | CONCUR | A Theory of Testing for Markovian Processes. | Marco Bernardo, Rance Cleaveland |
| 2000 | Coordination | GCCS: A Graphical Coordination Language for System Specification. | Rance Cleaveland, Xiaoqun Du, Scott A. Smolka |
| 2000 | ICALP | Branching-Time Probalistic Model Checking. | Rance Cleaveland, S. Purushothaman Iyer |
| 1999 | CONCUR | Temporal Process Logic (Abstract). | Rance Cleaveland |
| 1999 | CONCUR | Statecharts Via Process Algebra. | Gerald Lttgen, Michael von der Beeck, Rance Cleaveland |
| 1999 | FASE | On the Evolution of Reactive Components: A Process-Algebraic Approach. | Markus Mller-Olm, Bernhard Steffen, Rance Cleaveland |
| 1999 | FOSSACS | Probabilistic Temporal Logics via the Modal Mu-Calculus. | Murali Narasimha, Rance Cleaveland, S. Purushothaman Iyer |
| 1998 | CONCUR | Praobabilistic Resource Failure in Real-Time Process Algebra. | Anna Philippou, Rance Cleaveland, Insup Lee, Scott A. Smolka, Oleg Sokolsky |
| 1998 | FORTE | TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems. | Marco Bernardo, Rance Cleaveland, Steve Sims, W. Stewart |
| 1997 | CONCUR | An Algebraic Theory of Multiple Clocks. | Rance Cleaveland, Gerald Lttgen, Michael Mendler |
| 1997 | FORTE | Dynamic Priorities for Modeling Real-Time. | Girish Bhat, Rance Cleaveland, Gerald Lttgen |
| 1996 | CAV | The Concurrency Factory: A Development Environment for Concurrent Systems. | Rance Cleaveland, Philip M. Lewis, Scott A. Smolka, Oleg Sokolsky |
| 1996 | CAV | The NCSU Concurrency Workbench. | Rance Cleaveland, Steve Sims |
| 1996 | CONCUR | A Process Algebra with Distributed Priorities. | Rance Cleaveland, Gerald Lttgen, V. Natarajan |
| 1996 | LICS | Efficient Model Checking via the Equational µ-Calculus. | Girish Bhat, Rance Cleaveland |
| 1996 | LICS | An Algebraic Theory of Process Efficiency. | V. Natarajan, Rance Cleaveland |
| 1996 | SEKE | A Theory of Testing for Soft Real-Time Processes. | Rance Cleaveland, Insup Lee, Philip M. Lewis, Scott A. Smolka |
| 1996 | RTSS | Predictability of real-time systems: a process-algebraic approach. | V. Natarajan, Rance Cleaveland |
| 1996 | TACAS | Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus. | Girish Bhat, Rance Cleaveland |
| 1996 | TACAS | Priorities for Modeling and Verifying Distributed Systems. | Rance Cleaveland, Gerald Lttgen, V. Natarajan, Steve Sims |
| 1996 | TACAS | The Concurrency Factory Software Development Environment. | Rance Cleaveland, Philip M. Lewis, Scott A. Smolka, Oleg Sokolsky |
| 1995 | ICALP | Divergence and Fair Testing. | V. Natarajan, Rance Cleaveland |
| 1995 | ICECCS | A tool for modeling and verifying real-time systems. | Wael M. Elseaidy, Rance Cleaveland |
| 1995 | LICS | Efficient On-the-Fly Model Checking for CTL* | Girish Bhat, Rance Cleaveland, Orna Grumberg |
| 1995 | SAS | Optimality in Abstractions of Model Checking | Rance Cleaveland, S. Purushothaman Iyer, Daniel Yankelevich |
| 1995 | TACAS | A Front-End Generator for Verification Tools. | Rance Cleaveland, Eric Madelaine, Steve Sims |
| 1994 | CONCUR | Testing-Based Abstractions for Value-Passing Systems. | Rance Cleaveland, James Riely |
| 1994 | CONCUR | Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes. | Shoji Yuen, Rance Cleaveland, Zeynep Dayar, Scott A. Smolka |
| 1994 | POPL | An Operational Framework for Value-Passing Processes. | Rance Cleaveland, Daniel Yankelevich |
| 1994 | RTSS | Verifying an Intelligent Structural Control System: A Case Study. | Wael M. Elseaidy, Rance Cleaveland, John W. Baugh Jr. |
| 1993 | RTSS | RTSL: a language for real-time schedulability analysis. | Andre N. Fredette, Rance Cleaveland |
| 1992 | CAV | Generating Diagnostic Information for Behavioral Preorders. | Ufuk Celikkan, Rance Cleaveland |
| 1992 | CAV | Faster Model Checking for the Modal Mu-Calculus. | Rance Cleaveland, Marion Klein, Bernhard Steffen |
| 1992 | ICALP | Testing Preorders for Probabilistic Processes. | Rance Cleaveland, Scott A. Smolka, Amy E. Zwarico |
| 1991 | CAV | A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. | Rance Cleaveland, Bernhard Steffen |
| 1991 | ICALP | Computing Behavioural Relations, Logically. | Rance Cleaveland, Bernhard Steffen |
| 1991 | LICS | A Theory of Testing for Real-Time | Rance Cleaveland, Amy E. Zwarico |
| 1990 | CAV | On Automatically Explaining Bisimulation Inequivalence. | Rance Cleaveland |
| 1990 | CONCUR | A Preorder for Partial Process Specifications. | Rance Cleaveland, Bernhard Steffen |
| 1990 | LICS | When is "Partial" Adequate? A Logic-Based Proof Technique Using Partial Specifications | Rance Cleaveland, Bernhard Steffen |
| 1988 | LICS | Priorities in Process Algebras | Rance Cleaveland, Matthew Hennessy |