Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

Type theory and concurrency. - Rance Cleaveland; Prakash Panangaden (Int. J. Parallel Program., 1988)

The Concurrency Workbench. - Rance Cleaveland; Joachim Parrow; Bernhard Steffen (Automatic Verification Methods for Finite State Systems, 1989)

A Semantics Based Verification Tool for Finite State Systems. - Rance Cleaveland; Joachim Parrow; Bernhard Steffen (PSTV, 1989)

On Automatically Explaining Bisimulation Inequivalence. - Rance Cleaveland (CAV, 1990)

A Preorder for Partial Process Specifications. - Rance Cleaveland; Bernhard Steffen (CONCUR, 1990)

On Automatically Distinguishing Inequivalent Processes. - Rance Cleaveland (CAV (DIMACS/AMS volume), 1990)

When is "Partial" Adequate? A Logic-Based Proof Technique Using Partial Specifications - Rance Cleaveland; Bernhard Steffen (LICS, 1990)

Tableau-Based Model Checking in the Propositional Mu-Calculus. - Rance Cleaveland (Acta Informatica, 1990)

Priorities in Process Algebras - Rance Cleaveland; Matthew Hennessy (Inf. Comput., 1990)

Computing Behavioural Relations, Logically. - Rance Cleaveland; Bernhard Steffen (ICALP, 1991)

A Theory of Testing for Real-Time - Rance Cleaveland; Amy E. Zwarico (LICS, 1991)

Faster Model Checking for the Modal Mu-Calculus. - Rance Cleaveland; Marion Klein; Bernhard Steffen (CAV, 1992)

GDR: A Visualization Tool for Graph Algorithms. - Matthias F. Stallmann; Rance Cleaveland; Prashant Hebbar (Computational Support for Discrete Mathematics, 1992)

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

Computing Diagnostic Test for Incorrect Processes. - Ufuk Celikkan; Rance Cleaveland (PSTV, 1992)

Analysing Concurrent Systems Using the Concurrency Workbench. - Rance Cleaveland (Functional Programming, Concurrency, Simulation and Automated Reasoning, 1993)

RTSL: a language for real-time schedulability analysis. - Andre N. Fredette; Rance Cleaveland (RTSS, 1993)

Testing Equivalence as a Bisimulation Equivalence. - Rance Cleaveland; Matthew Hennessy (Formal Aspects Comput., 1993)

A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. - Rance Cleaveland; Bernhard Steffen (Formal Methods Syst. Des., 1993)

The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems. - Rance Cleaveland; Joachim Parrow; Bernhard Steffen (ACM Trans. Program. Lang. Syst., 1993)

Testing-Based Abstractions for Value-Passing Systems. - Rance Cleaveland; James Riely (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)

Priority and Abstraction in Process Algebra. - V. Natarajan 001; Ivan Christoff; Linda Christoff; Rance Cleaveland (FSTTCS, 1994)

An Operational Framework for Value-Passing Processes. - Rance Cleaveland; Daniel Yankelevich (POPL, 1994)

Verifying an Intelligent Structural Control System: A Case Study. - Wael M. Elseaidy; Rance Cleaveland; John W. Baugh Jr. (RTSS, 1994)

Divergence and Fair Testing. - V. Natarajan 001; Rance Cleaveland (ICALP, 1995)

A tool for modeling and verifying real-time systems. - Wael M. Elseaidy; Rance Cleaveland (ICECCS, 1995)

Efficient On-the-Fly Model Checking for CTL* - Girish Bhat; Rance Cleaveland; Orna Grumberg (LICS, 1995)

Optimality in Abstractions of Model Checking - Rance Cleaveland; S. Purushothaman Iyer; Daniel Yankelevich (SAS, 1995)

A Front-End Generator for Verification Tools. - Rance Cleaveland; Eric Madelaine; Steve Sims (TACAS, 1995)

Generating Diagnostic Information for Behavioral Preorders. - Ufuk Celikkan; Rance Cleaveland (Distributed Comput., 1995)

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

The NCSU Concurrency Workbench. - Rance Cleaveland; Steve Sims (CAV, 1996)

Efficient Model Checking via the Equational µ-Calculus. - Girish Bhat; Rance Cleaveland (LICS, 1996)

An Algebraic Theory of Process Efficiency. - V. Natarajan 001; Rance Cleaveland (LICS, 1996)

Predictability of real-time systems: a process-algebraic approach. - V. Natarajan 001; Rance Cleaveland (RTSS, 1996)

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

Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus. - Girish Bhat; Rance Cleaveland (TACAS, 1996)

Priorities for Modeling and Verifying Distributed Systems. - Rance Cleaveland; Gerald Lüttgen; V. Natarajan 001; Steve Sims (TACAS, 1996)

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

Semantic Theories and System Design. - Rance Cleaveland (ACM Comput. Surv., 1996)

Formality and Software Design. - Rance Cleaveland (ACM Comput. Surv., 1996)

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

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

Modeling and Verifying Distributed Systems Using Priorities: A Case Study. - Rance Cleaveland; V. Natarajan 001; Steve Sims; Gerald Lüttgen (Softw. Concepts Tools, 1996)

An Algebraic Theory of Multiple Clocks. - Rance Cleaveland; Gerald Lüttgen; Michael Mendler (CONCUR, 1997)

Dynamic Priorities for Modeling Real-Time. - Girish Bhat; Rance Cleaveland; Gerald Lüttgen (FORTE, 1997)

Preface. - Rance Cleaveland; Michael W. Mislove; Philip S. Mulry (US-Brazil Joint Workshops on the Formal Foundations of Software Systems, 1997)

Modeling and Verifying Active Structural Control Systems. - Wael M. Elseaidy; Rance Cleaveland; John W. Baugh Jr. (Sci. Comput. Program., 1997)

Editorial. - Rance Cleaveland; Tiziana Margaria; Bernhard Steffen (Int. J. Softw. Tools Technol. Transf., 1997)

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

TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems. - Marco Bernardo 001; Rance Cleaveland; Steve Sims; W. Stewart (FORTE, 1998)

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

The role of observations in probabilistic open systems. - Murali Narasimha; Rance Cleaveland; S. Purushothaman Iyer (Monterey Workshop, 1998)

A Process Algebra with Distributed Priorities. - Rance Cleaveland; Gerald Lüttgen; V. Natarajan 001 (Theor. Comput. Sci., 1998)

Temporal Process Logic (Abstract). - Rance Cleaveland (CONCUR, 1999)

Statecharts Via Process Algebra. - Gerald Lüttgen; Michael von der Beeck; Rance Cleaveland (CONCUR, 1999)

On the Evolution of Reactive Components: A Process-Algebraic Approach. - Markus Müller-Olm; Bernhard Steffen; Rance Cleaveland (FASE, 1999)

A Practical Approach to Implementing Real-Time Semantics. - Girish Bhat; Rance Cleaveland; Gerald Lüttgen (Ann. Softw. Eng., 1999)

Guest Editorial. - Rance Cleaveland; Daniel Jackson 001 (Autom. Softw. Eng., 1999)

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

Pragmatics of Model Checking: An STTT Special Section. - Rance Cleaveland (Int. J. Softw. Tools Technol. Transf., 1999)

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

A Theory of Testing for Markovian Processes. - Marco Bernardo 001; Rance Cleaveland (CONCUR, 2000)

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

A Semantic Theory for Heterogeneous System Design. - Rance Cleaveland; Gerald Lüttgen (FSTTCS, 2000)

Branching-Time Probalistic Model Checking. - Rance Cleaveland; S. Purushothaman Iyer (ICALP Satellite Workshops, 2000)

A compositional approach to statecharts semantics. - Gerald Lüttgen; Michael von der Beeck; Rance Cleaveland (SIGSOFT FSE, 2000)

Specification formalisms for component-based concurrent systems. - Rance Cleaveland (ACM SIGSOFT Softw. Eng. Notes, 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)

Priority in Process Algebra. - Rance Cleaveland; Gerald Lüttgen; V. Natarajan 001 (Handbook of Process Algebra, 2001)

Equivalence and Preorder Checking for Finite-State Systems. - Rance Cleaveland; Oleg Sokolsky (Handbook of Process Algebra, 2001)

Efficient Model Checking Via Büchi Tableau Automata. - Girish Bhat; Rance Cleaveland; Alex Groce (CAV, 2001)

Automated Validation of Software Models. - Steve Sims; Rance Cleaveland; Ken Butts; Scott Ranville (ASE, 2001)

Simulation Revisited. - Li Tan; Rance Cleaveland (TACAS, 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)

Alternative Approaches to Symbolic Verification - Preface by the Section Editor. - Rance Cleaveland (Int. J. Softw. Tools Technol. Transf., 2001)

Evidence-Based Model Checking. - Li Tan; Rance Cleaveland (CAV, 2002)

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

Foreword. - Rance Cleaveland; Hubert Garavel (FMICS, 2002)

A Logical Process Calculus. - Rance Cleaveland; Gerald Lüttgen (EXPRESS, 2002)

Generic tools for verifying concurrent systems. - Rance Cleaveland; Steve Sims (Sci. Comput. Program., 2002)

TRIM: A Tool for Triggered Message Sequence Charts. - Bikram Sengupta; Rance Cleaveland (CAV, 2003)

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

Architectural Interaction Diagrams: AIDs for System Modeling. - Arnab Ray; Rance Cleaveland (ICSE, 2003)

Refinement-Based Requirements Modeling Using TriggeredMessage Sequence Charts. - Bikram Sengupta; Rance Cleaveland (RE, 2003)

The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. - Dezhuang Zhang; Rance Cleaveland; Eugene W. Stark (TACAS, 2003)

Secure Requirements Elicitation Through Triggered Message Sequence Charts. - Arnab Ray; Bikram Sengupta; Rance Cleaveland (ICDCIT, 2004)

Formal Modeling Of Middleware-based Distributed Systems. - Arnab Ray; Rance Cleaveland (FESCA@ETAPS, 2004)

An Algebraic Theory Of Boundary Crossing Transitions. - Arnab Ray; Rance Cleaveland; Arne Skou (SFEDL@ETAPS, 2004)

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

Unit verification: the CARA experience. - Arnab Ray; Rance Cleaveland (Int. J. Softw. Tools Technol. Transf., 2004)

Fast Generic Model-Checking for Data-Based Systems. - Dezhuang Zhang; Rance Cleaveland (FORTE, 2005)

Executable Requirements Specifications Using Triggered Message Sequence Charts. - Bikram Sengupta; Rance Cleaveland (ICDCIT, 2005)

An Integrated Framework for Scenarios and State Machines. - Bikram Sengupta; Rance Cleaveland (IFM, 2005)

Efficient temporal-logic query checking for presburger systems. - Dezhuang Zhang; Rance Cleaveland (ASE, 2005)

Fast On-the-Fly Parametric Real-Time Model Checking. - Dezhuang Zhang; Rance Cleaveland (RTSS, 2005)

Probabilistic temporal logics via the modal mu-calculus. - Rance Cleaveland; S. Purushothaman Iyer; Murali Narasimha (Theor. Comput. Sci., 2005)

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

A Software Architectural Approach to Security by Design. - Arnab Ray; Rance Cleaveland (COMPSAC (2), 2006)

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

High-Confidence Medical Device Software and Systems. - Insup Lee 001; George J. Pappas; Rance Cleaveland; John Hatcliff; Bruce H. Krogh; Peter Lee 001; Harvey Rubin; Lui Sha (Computer, 2006)

Triggered Message Sequence Charts. - Bikram Sengupta; Rance Cleaveland (IEEE Trans. Software Eng., 2006)

THERE AND BACK AGAIN: Lessons Learned on the Way to the Market. - Rance Cleaveland (TACAS, 2007)

Executable Specifications for Real-Time Distributed Systems. - Arnab Ray; Rance Cleaveland (SLA++P@ETAPS, 2007)

Priority and abstraction in process algebra. - Rance Cleaveland; Gerald Lüttgen; V. Natarajan 001 (Inf. Comput., 2007)

Model-Based Verification of Automotive Control Software. - Rance Cleaveland (FMICS, 2008)

Towards Behavioral Reflexion Models. - Christopher Ackermann; Mikael Lindvall; Rance Cleaveland (ISSRE, 2009)

Validating Automotive Control Software Using Instrumentation-Based Verification. - Arnab Ray; Iris Morschhaeuser; Christopher Ackermann; Rance Cleaveland; Charles P. Shelton; Chris Martin (ASE, 2009)

Recovering Views of Inter-System Interaction Behaviors. - Christopher Ackermann; Mikael Lindvall; Rance Cleaveland (WCRE, 2009)

Using formal specifications to support testing. - Robert M. Hierons; Kirill Bogdanov 002; Jonathan P. Bowen; Rance Cleaveland; John Derrick; Jeremy Dick; Marian Gheorghe 001; Mark Harman; Kalpesh Kapoor; Paul J. Krause; Gerald Lüttgen; Anthony J. H. Simons; et al. (ACM Comput. Surv., 2009)

Automatic Requirement Extraction from Test Cases. - Christopher Ackermann; Rance Cleaveland; Samuel Huang 001; Arnab Ray; Charles P. Shelton; Elizabeth Latronico (RV, 2010)

Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems. - Peter Fontana; Rance Cleaveland (DIFTS@FMCAD, 2011)

Architecture Reconstruction and Analysis of Medical Device Software. - Dharmalingam Ganesan; Mikael Lindvall; Rance Cleaveland; Raoul Praful Jetley; Paul L. Jones; Yi Zhang 051 (WICSA, 2011)

Functional and Nonfunctional Design Verification for Embedded Software Systems. - Arnab Ray; Christopher Ackermann; Rance Cleaveland; Charles P. Shelton; Chris Martin (Adv. Comput., 2011)

Constructing safety assurance cases for medical devices. - Arnab Ray; Rance Cleaveland (ASSURE@ICSE, 2013)

Integrating model checking and UML based model-driven development for embedded systems. - Zamira Daw; Rance Cleaveland; Marcus Vetter (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

The Power of Proofs: New Algorithms for Timed Automata Model Checking. - Peter Fontana; Rance Cleaveland (FORMATS, 2014)

Generalized Synchronization Trees. - James Ferlez; Rance Cleaveland; Steven I. Marcus (FoSSaCS, 2014)

An analysis method for medical device security. - Arnab Ray; Rance Cleaveland (HotSoS, 2014)

Assessing model-based testing: an empirical study conducted in industry. - Christoph Schulze 001; Dharmalingam Ganesan; Mikael Lindvall; Rance Cleaveland; Daniel Goldman (ICSE Companion, 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)

Formal verification of software-based medical devices considering medical guidelines. - Zamira Daw; Rance Cleaveland; Marcus Vetter (Int. J. Comput. Assist. Radiol. Surg., 2014)

The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix). - Peter Fontana; Rance Cleaveland (CoRR, 2014)

A menagerie of timed automata. - Peter Fontana; Rance Cleaveland (ACM Comput. Surv., 2014)

UML-VT: A Formal Verification Environment for UML Activity Diagrams. - Zamira Daw; John Mangino; Rance Cleaveland (P&D@MoDELS, 2015)

An Extensible Operational Semantics for UML Activity Diagrams. - Zamira Daw; Rance Cleaveland (SEFM, 2015)

Security Assurance Cases for Medical Cyber-Physical Systems. - Arnab Ray; Rance Cleaveland (IEEE Des. Test, 2015)

Comparing model checkers for timed UML activity diagrams. - Zamira Daw; Rance Cleaveland (Sci. Comput. Program., 2015)

A framework for decentralized opacity in linear systems. - Bhaskar Ramasubramanian; Rance Cleaveland; Steven I. Marcus (Allerton, 2016)

A framework for opacity in linear systems. - Bhaskar Ramasubramanian; Rance Cleaveland; Steven I. Marcus (ACC, 2016)

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)

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 (ISSRE, 2016)

An extensible formal semantics for UML activity diagrams. - Zamira Daw; Rance Cleaveland (CoRR, 2016)

Opacity for switched linear systems: Notions and characterization. - Bhaskar Ramasubramanian; Rance Cleaveland; Steven I. Marcus (CDC, 2017)

Query Checking for Linear Temporal Logic. - Samuel Huang 001; Rance Cleaveland (FMICS-AVoCS, 2017)

Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. - James Ferlez; Rance Cleaveland; Steven I. Marcus (EXPRESS/SOS, 2017)

Corrections to "A Menagerie of Timed Automata". - Jeroen J. A. Keiren; Peter Fontana; Rance Cleaveland (ACM Comput. Surv., 2017)

Improving Invariant Mining via Static Analysis. - Christoph Schulze 001; Rance Cleaveland (ACM Trans. Embed. Comput. Syst., 2017)

Bisimulation in Behavioral Dynamical Systems and Generalized Synchronization Trees. - James Ferlez; Rance Cleaveland; Steven I. Marcus (CDC, 2018)

Programming Is Modeling. - Rance Cleaveland (ISoLA (1), 2018)

Automated Specification Extraction and Analysis with Specstractor. - Christoph Schulze 001; Rance Cleaveland; Mikael Lindvall (SEFM, 2018)

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

Scott Smolka and Me. - Rance Cleaveland (From Reactive Systems to Cyber-Physical Systems, 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)

Timed Automata Benchmark Description. - Peter Fontana; Rance Cleaveland (CoRR, 2020)

Notions of Centralized and Decentralized Opacity in Linear Systems. - Bhaskar Ramasubramanian; Rance Cleaveland; Steven I. Marcus (IEEE Trans. Autom. Control., 2020)

Navigating the Seismic Shift of Post-Moore Computer Systems Design. - Anindya Banerjee 001; Sankar Basu; Erik Brunvand; Pinaki Mazumder; Rance Cleaveland; Gurdip Singh; Margaret Martonosi; Fernanda Pembleton (IEEE Micro, 2021)

Better Automata Through Process Algebra. - Rance Cleaveland (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

Resilience to denial-of-service and integrity attacks: A structured systems approach. - Bhaskar Ramasubramanian; M. A. Rajan; M. Girish Chandra; Rance Cleaveland; Steven I. Marcus (Eur. J. Control, 2022)

A tableau construction for finite linear-time temporal logic. - Samuel Huang 001; Rance Cleaveland (J. Log. Algebraic Methods Program., 2022)

Temporal-logic query checking over finite data streams. - Samuel Huang 001; Rance Cleaveland (Int. J. Softw. Tools Technol. Transf., 2022)

Expressiveness Results for Timed Modal Mu-Calculi. - Rance Cleaveland; Jeroen J. A. Keiren; Peter Fontana (CoRR, 2023)

Qafny: A Quantum-Program Verifier. - Liyi Li 002; Mingwei Zhu; Rance Cleaveland; Alexander Nicolellis; Yi Lee; Le Chang; Xiaodi Wu 001 (ECOOP, 2024)

An Expressive Timed Modal Mu-Calculus for Timed Automata. - Rance Cleaveland; Jeroen J. A. Keiren; Peter Fontana (QEST+FORMATS, 2024)

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

The Quantum Abstract Machine. - Liyi Li 002; Le Chang; Rance Cleaveland; Mingwei Zhu; Xiaodi Wu 001 (CoRR, 2024)

DisQ: A Markov Decision Process Based Language for Quantum Distributed Systems. - Le Chang; Saitej Yavvari; Rance Cleaveland; Samik Basu 001; Liyi Li 002 (CoRR, 2024)

Qafny: A Quantum-Program Verifier (Artifact). - Liyi Li 002; Mingwei Zhu; Rance Cleaveland; Alexander Nicolellis; Yi Lee; Le Chang; Xiaodi Wu 001 (Dagstuhl Artifacts Ser., 2024)

Extensible Proof Systems for Infinite-State Systems. - Rance Cleaveland; Jeroen J. A. Keiren (ACM Trans. Comput. Log., 2024)

Formal Methods in Industry. - Maurice H. ter Beek; Rod Chapman; Rance Cleaveland; Hubert Garavel; Rong Gu; Ivo ter Horst; Jeroen J. A. Keiren; Thierry Lecomte; Michael Leuschel; Kristin Yvonne Rozier; Augusto Sampaio 001; Cristina Seceleanu; et al. (Formal Aspects Comput., 2025)