


default search action
Rance Cleaveland
Person information
- affiliation: University of Maryland, College Park, USA
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j48]Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu:
Qafny: A Quantum-Program Verifier (Artifact). Dagstuhl Artifacts Ser. 10(2): 12:1-12:2 (2024) - [j47]Rance Cleaveland
, Jeroen J. A. Keiren
:
Extensible Proof Systems for Infinite-State Systems. ACM Trans. Comput. Log. 25(1): 2:1-2:60 (2024) - [c114]Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu:
Qafny: A Quantum-Program Verifier. ECOOP 2024: 24:1-24:31 - [c113]Rance Cleaveland
, Jeroen J. A. Keiren
, Peter Fontana:
An Expressive Timed Modal Mu-Calculus for Timed Automata. QEST+FORMATS 2024: 160-178 - [c112]Rance Cleaveland
, David Hansel, Steve Sims, Scott A. Smolka
:
Two Decades of Industrializing Formal Verification: The Reactis Story. SPIN 2024: 87-105 - [i13]Liyi Li, Le Chang, Rance Cleaveland, Mingwei Zhu, Xiaodi Wu:
The Quantum Abstract Machine. CoRR abs/2402.13469 (2024) - [i12]Le Chang, Saitej Yavvari, Rance Cleaveland, Samik Basu, Liyi Li:
DisQ: A Markov Decision Process Based Language for Quantum Distributed Systems. CoRR abs/2407.09710 (2024) - 2023
- [i11]Rance Cleaveland, Jeroen J. A. Keiren, Peter Fontana:
Expressiveness Results for Timed Modal Mu-Calculi. CoRR abs/2310.04100 (2023) - 2022
- [j46]Bhaskar Ramasubramanian
, M. A. Rajan, M. Girish Chandra, Rance Cleaveland
, Steven I. Marcus
:
Resilience to denial-of-service and integrity attacks: A structured systems approach. Eur. J. Control 63: 61-69 (2022) - [j45]Samuel Huang, Rance Cleaveland
:
A tableau construction for finite linear-time temporal logic. J. Log. Algebraic Methods Program. 125: 100743 (2022) - [j44]Samuel Huang
, Rance Cleaveland
:
Temporal-logic query checking over finite data streams. Int. J. Softw. Tools Technol. Transf. 24(3): 473-492 (2022) - [c111]Rance Cleaveland
:
Better Automata Through Process Algebra. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 116-136 - [i10]Jeroen J. A. Keiren, Rance Cleaveland:
Extensible Proof Systems for Infinite-State Systems. CoRR abs/2207.12953 (2022) - 2021
- [j43]Anindya Banerjee
, Sankar Basu
, Erik Brunvand, Pinaki Mazumder, Rance Cleaveland, Gurdip Singh, Margaret Martonosi
, Fernanda Pembleton:
Navigating the Seismic Shift of Post-Moore Computer Systems Design. IEEE Micro 41(6): 162-167 (2021) - [i9]Bhaskar Ramasubramanian, M. A. Rajan, M. Girish Chandra, Rance Cleaveland, Steven I. Marcus:
Resilience to Denial-of-Service and Integrity Attacks: A Structured Systems Approach. CoRR abs/2109.01224 (2021) - 2020
- [j42]Bhaskar Ramasubramanian
, Rance Cleaveland
, Steven I. Marcus
:
Notions of Centralized and Decentralized Opacity in Linear Systems. IEEE Trans. Autom. Control. 65(4): 1442-1455 (2020) - [c110]Samuel Huang
, Rance Cleaveland
:
Temporal-Logic Query Checking over Finite Data Streams. FMICS 2020: 252-271 - [i8]Rance Cleaveland:
Better Automata through Process Algebra. CoRR abs/2002.07562 (2020) - [i7]Peter Fontana, Rance Cleaveland:
Timed Automata Benchmark Description. CoRR abs/2005.13151 (2020) - [i6]Samuel Huang, Rance Cleaveland:
Temporal-Logic Query Checking over Finite Data Streams. CoRR abs/2006.03751 (2020)
2010 – 2019
- 2019
- [j41]Md. Ariful Islam, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka:
Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans. Theor. Comput. Sci. 765: 158-169 (2019) - [c109]Rance Cleaveland:
Scott Smolka and Me. From Reactive Systems to Cyber-Physical Systems 2019: 1-6 - [e6]Ezio Bartocci, Rance Cleaveland, Radu Grosu, Oleg Sokolsky:
From Reactive Systems to Cyber-Physical Systems - Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday. Lecture Notes in Computer Science 11500, Springer 2019, ISBN 978-3-030-31513-9 [contents] - [i5]Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus:
Notions of Centralized and Decentralized Opacity in Linear Systems. CoRR abs/1903.06869 (2019) - [i4]Samuel Huang, Rance Cleaveland:
A Tableau Construction for Finite Linear-Time Temporal Logic. CoRR abs/1910.09339 (2019) - 2018
- [c108]James Ferlez
, Rance Cleaveland, Steven I. Marcus:
Bisimulation in Behavioral Dynamical Systems and Generalized Synchronization Trees. CDC 2018: 751-758 - [c107]Rance Cleaveland:
Programming Is Modeling. ISoLA (1) 2018: 150-161 - [c106]Christoph Schulze, Rance Cleaveland, Mikael Lindvall:
Automated Specification Extraction and Analysis with Specstractor. SEFM 2018: 37-53 - [p3]Rance Cleaveland, A. W. Roscoe, Scott A. Smolka:
Process Algebra and Model Checking. Handbook of Model Checking 2018: 1149-1195 - 2017
- [j40]Jeroen J. A. Keiren, Peter Fontana, Rance Cleaveland:
Corrections to "A Menagerie of Timed Automata". ACM Comput. Surv. 50(3): 42:1-42:8 (2017) - [j39]Christoph Schulze, Rance Cleaveland:
Improving Invariant Mining via Static Analysis. ACM Trans. Embed. Comput. Syst. 16(5s): 167:1-167:20 (2017) - [c105]Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus:
Opacity for switched linear systems: Notions and characterization. CDC 2017: 5310-5315 - [c104]Samuel Huang, Rance Cleaveland:
Query Checking for Linear Temporal Logic. FMICS-AVoCS 2017: 34-48 - [c103]James Ferlez
, Rance Cleaveland, Steven I. Marcus:
Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. EXPRESS/SOS 2017: 35-50 - 2016
- [c102]Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus:
A framework for decentralized opacity in linear systems. Allerton 2016: 274-280 - [c101]Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus:
A framework for opacity in linear systems. ACC 2016: 6337-6344 - [c100]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
, Flavio H. Fenton, Richard A. Gray, James Glimm, Shan Lin, Qinsi Wang, Scott A. Smolka:
CyberCardia project: Modeling, verification and validation of implantable cardiac devices. BIBM 2016: 1445-1452 - [c99]Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka:
Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability. CMSB 2016: 132-146 - [c98]Dharmalingam Ganesan, Mikael Lindvall, Stefan Hafsteinsson, Rance Cleaveland, Susanne L. Strege, Walter Moleski:
Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus. ISSRE 2016: 445-454 - [i3]Jeroen J. A. Keiren, Peter Fontana, Rance Cleaveland:
Corrections to A Menagerie of Timed Automata. CoRR abs/1602.07165 (2016) - [i2]Zamira Daw, Rance Cleaveland:
An extensible formal semantics for UML activity diagrams. CoRR abs/1604.02386 (2016) - 2015
- [j38]Arnab Ray, Rance Cleaveland:
Security Assurance Cases for Medical Cyber-Physical Systems. IEEE Des. Test 32(5): 56-65 (2015) - [j37]Zamira Daw, Rance Cleaveland:
Comparing model checkers for timed UML activity diagrams. Sci. Comput. Program. 111: 277-299 (2015) - [c97]Zamira Daw, John Mangino, Rance Cleaveland:
UML-VT: A Formal Verification Environment for UML Activity Diagrams. P&D@MoDELS 2015: 48-51 - [c96]Zamira Daw, Rance Cleaveland:
An Extensible Operational Semantics for UML Activity Diagrams. SEFM 2015: 360-368 - 2014
- [j36]Zamira Daw, Rance Cleaveland, Marcus Vetter:
Formal verification of software-based medical devices considering medical guidelines. Int. J. Comput. Assist. Radiol. Surg. 9(1): 145-153 (2014) - [j35]Peter Fontana, Rance Cleaveland:
A menagerie of timed automata. ACM Comput. Surv. 46(3): 40:1-40:56 (2014) - [c95]Peter Fontana, Rance Cleaveland:
The Power of Proofs: New Algorithms for Timed Automata Model Checking. FORMATS 2014: 115-129 - [c94]James Ferlez
, Rance Cleaveland, Steven I. Marcus:
Generalized Synchronization Trees. FoSSaCS 2014: 304-319 - [c93]Arnab Ray, Rance Cleaveland:
An analysis method for medical device security. HotSoS 2014: 16 - [c92]Christoph Schulze, Dharmalingam Ganesan, Mikael Lindvall, Rance Cleaveland, Daniel Goldman:
Assessing model-based testing: an empirical study conducted in industry. ICSE Companion 2014: 135-144 - [c91]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:
Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices. ISoLA (2) 2014: 356-364 - [i1]Peter Fontana, Rance Cleaveland:
The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix). CoRR abs/1408.6104 (2014) - 2013
- [j34]Zamira Daw, Rance Cleaveland, Marcus Vetter:
Integrating model checking and UML based model-driven development for embedded systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013) - [c90]Arnab Ray, Rance Cleaveland:
Constructing safety assurance cases for medical devices. ASSURE@ICSE 2013: 40-45 - 2011
- [j33]Arnab Ray, Christopher Ackermann, Rance Cleaveland, Charles P. Shelton, Chris Martin:
Functional and Nonfunctional Design Verification for Embedded Software Systems. Adv. Comput. 83: 277-321 (2011) - [c89]Peter Fontana, Rance Cleaveland:
Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems. DIFTS@FMCAD 2011 - [c88]Dharmalingam Ganesan, Mikael Lindvall, Rance Cleaveland, Raoul Praful Jetley, Paul L. Jones, Yi Zhang
:
Architecture Reconstruction and Analysis of Medical Device Software. WICSA 2011: 194-203 - 2010
- [c87]Christopher Ackermann, Rance Cleaveland, Samuel Huang, Arnab Ray, Charles P. Shelton, Elizabeth Latronico:
Automatic Requirement Extraction from Test Cases. RV 2010: 1-15
2000 – 2009
- 2009
- [j32]Robert M. Hierons
, Kirill Bogdanov, Jonathan P. Bowen
, Rance Cleaveland, John Derrick
, Jeremy Dick, Marian Gheorghe
, Mark Harman
, Kalpesh Kapoor, Paul J. Krause, Gerald Lüttgen, Anthony J. H. Simons
, Sergiy A. Vilkomir, Martin R. Woodward, Hussein Zedan:
Using formal specifications to support testing. ACM Comput. Surv. 41(2): 9:1-9:76 (2009) - [c86]Christopher Ackermann, Mikael Lindvall, Rance Cleaveland:
Towards Behavioral Reflexion Models. ISSRE 2009: 175-184 - [c85]Arnab Ray, Iris Morschhaeuser, Christopher Ackermann, Rance Cleaveland, Charles P. Shelton, Chris Martin:
Validating Automotive Control Software Using Instrumentation-Based Verification. ASE 2009: 15-25 - [c84]Christopher Ackermann, Mikael Lindvall, Rance Cleaveland:
Recovering Views of Inter-System Interaction Behaviors. WCRE 2009: 53-61 - 2008
- [c83]Rance Cleaveland:
Model-Based Verification of Automotive Control Software. FMICS 2008: 2 - 2007
- [j31]Rance Cleaveland, Gerald Lüttgen, V. Natarajan:
Priority and abstraction in process algebra. Inf. Comput. 205(9): 1426-1458 (2007) - [c82]Rance Cleaveland:
THERE AND BACK AGAIN: Lessons Learned on the Way to the Market. TACAS 2007: 1 - [c81]Arnab Ray, Rance Cleaveland:
Executable Specifications for Real-Time Distributed Systems. SLA++P@ETAPS 2007: 3-17 - 2006
- [j30]Insup Lee, George J. Pappas
, Rance Cleaveland, John Hatcliff, Bruce H. Krogh, Peter Lee, Harvey Rubin, Lui Sha:
High-Confidence Medical Device Software and Systems. Computer 39(4): 33-38 (2006) - [j29]Bikram Sengupta, Rance Cleaveland:
Triggered Message Sequence Charts. IEEE Trans. Software Eng. 32(8): 587-607 (2006) - [c80]Rance Cleaveland, Scott A. Smolka, Steve Sims:
An Instrumentation-Based Approach to Controller Model Validation. ASWSD 2006: 84-97 - [c79]Arnab Ray, Rance Cleaveland:
A Software Architectural Approach to Security by Design. COMPSAC (2) 2006: 83-86 - [c78]Eugene W. Stark, Rance Cleaveland, Scott A. Smolka:
Probabilistic I/O Automata: Theories of Two Equivalences. CONCUR 2006: 343-357 - 2005
- [j28]Rance Cleaveland, S. Purushothaman Iyer, Murali Narasimha:
Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci. 342(2-3): 316-350 (2005) - [c77]Dezhuang Zhang, Rance Cleaveland:
Fast Generic Model-Checking for Data-Based Systems. FORTE 2005: 83-97 - [c76]Bikram Sengupta, Rance Cleaveland:
Executable Requirements Specifications Using Triggered Message Sequence Charts. ICDCIT 2005: 482-493 - [c75]Bikram Sengupta, Rance Cleaveland:
An Integrated Framework for Scenarios and State Machines. IFM 2005: 366-385 - [c74]Dezhuang Zhang, Rance Cleaveland:
Efficient temporal-logic query checking for presburger systems. ASE 2005: 24-33 - [c73]Dezhuang Zhang, Rance Cleaveland:
Fast On-the-Fly Parametric Real-Time Model Checking. RTSS 2005: 157-166 - 2004
- [j27]David Hansel, Rance Cleaveland, Scott A. Smolka:
Distributed prototyping from validated specifications. J. Syst. Softw. 70(3): 275-298 (2004) - [j26]Arnab Ray, Rance Cleaveland:
Unit verification: the CARA experience. Int. J. Softw. Tools Technol. Transf. 5(4): 351-369 (2004) - [c72]Arnab Ray, Bikram Sengupta, Rance Cleaveland:
Secure Requirements Elicitation Through Triggered Message Sequence Charts. ICDCIT 2004: 273-282 - [c71]Arnab Ray, Rance Cleaveland:
Formal Modeling Of Middleware-based Distributed Systems. FESCA@ETAPS 2004: 21-37 - [c70]Arnab Ray, Rance Cleaveland, Arne Skou
:
An Algebraic Theory Of Boundary Crossing Transitions. SFEDL@ETAPS 2004: 69-88 - 2003
- [c69]Bikram Sengupta, Rance Cleaveland:
TRIM: A Tool for Triggered Message Sequence Charts. CAV 2003: 106-109 - [c68]Eugene W. Stark, Rance Cleaveland, Scott A. Smolka:
A Process-Algebraic Language for Probabilistic I/O Automata. CONCUR 2003: 189-203 - [c67]Arnab Ray, Rance Cleaveland:
Architectural Interaction Diagrams: AIDs for System Modeling. ICSE 2003: 396-407 - [c66]Bikram Sengupta, Rance Cleaveland:
Refinement-Based Requirements Modeling Using TriggeredMessage Sequence Charts. RE 2003: 95-104 - [c65]Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark:
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. TACAS 2003: 431-436 - 2002
- [j25]Rance Cleaveland, Steve Sims:
Generic tools for verifying concurrent systems. Sci. Comput. Program. 42(1): 39-47 (2002) - [c64]Li Tan, Rance Cleaveland:
Evidence-Based Model Checking. CAV 2002: 455-470 - [c63]Radu Grosu, Erez Zadok, Scott A. Smolka, Rance Cleaveland, Yanhong A. Liu:
High-confidence operating systems. ACM SIGOPS European Workshop 2002: 205-208 - [c62]Bikram Sengupta, Rance Cleaveland:
Triggered message sequence charts. SIGSOFT FSE 2002: 167-176 - [c61]Rance Cleaveland, Gerald Lüttgen:
A Logical Process Calculus. EXPRESS 2002: 33-50 - [c60]Rance Cleaveland, Hubert Garavel:
Foreword. FMICS 2002: 211-213 - [e5]Rance Cleaveland, Hubert Garavel:
7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems, FMICS 2002, ICALP 2002 Satellite Workshop, Málaga, Spain, July 12-13, 2002. Electronic Notes in Theoretical Computer Science 66(2), Elsevier 2002 [contents] - 2001
- [j24]Anna Philippou, Oleg Sokolsky, Insup Lee, Rance Cleaveland, Scott A. Smolka:
Hiding resources that can fail: An axiomatic perspective. Inf. Process. Lett. 80(1): 3-13 (2001) - [j23]Rance Cleaveland:
Alternative Approaches to Symbolic Verification - Preface by the Section Editor. Int. J. Softw. Tools Technol. Transf. 3(3): 247-249 (2001) - [c59]Girish Bhat, Rance Cleaveland, Alex Groce:
Efficient Model Checking Via Büchi Tableau Automata. CAV 2001: 38-52 - [c58]Steve Sims, Rance Cleaveland, Ken Butts, Scott Ranville:
Automated Validation of Software Models. ASE 2001: 91- - [c57]David Hansel, Rance Cleaveland, Scott A. Smolka:
Distributed Prototyping from Validated Specifications. IEEE International Workshop on Rapid System Prototyping 2001: 97-102 - [c56]Li Tan, Rance Cleaveland:
Simulation Revisited. TACAS 2001: 480-495 - [p2]Rance Cleaveland, Oleg Sokolsky
:
Equivalence and Preorder Checking for Finite-State Systems. Handbook of Process Algebra 2001: 391-424 - [p1]Rance Cleaveland, Gerald Lüttgen, V. Natarajan:
Priority in Process Algebra. Handbook of Process Algebra 2001: 711-765 - 2000
- [j22]Rance Cleaveland:
Specification formalisms for component-based concurrent systems. ACM SIGSOFT Softw. Eng. Notes 25(1): 42-43 (2000) - [j21]Rance Cleaveland, Philip M. Lewis, Scott A. Smolka:
Practical techniques for the design, specification, verification, and implementation of concurrent systems. ACM SIGSOFT Softw. Eng. Notes 25(1): 43-44 (2000) - [c55]Marco Bernardo, Rance Cleaveland:
A Theory of Testing for Markovian Processes. CONCUR 2000: 305-319 - [c54]Rance Cleaveland, Xiaoqun Du, Scott A. Smolka:
GCCS: A Graphical Coordination Language for System Specification. COORDINATION 2000: 284-298 - [c53]Rance Cleaveland, Gerald Lüttgen:
A Semantic Theory for Heterogeneous System Design. FSTTCS 2000: 312-324 - [c52]Rance Cleaveland, S. Purushothaman Iyer:
Branching-Time Probalistic Model Checking. ICALP Satellite Workshops 2000: 487-500 - [c51]Gerald Lüttgen, Michael von der Beeck, Rance Cleaveland:
A compositional approach to statecharts semantics. SIGSOFT FSE 2000: 120-129
1990 – 1999
- 1999
- [j20]Girish Bhat, Rance Cleaveland, Gerald Lüttgen:
A Practical Approach to Implementing Real-Time Semantics. Ann. Softw. Eng. 7: 127-155 (1999) - [j19]Rance Cleaveland, Daniel Jackson:
Guest Editorial. Autom. Softw. Eng. 6(1): 5-6 (1999) - [j18]Rance Cleaveland, Zeynep Dayar, Scott A. Smolka, Shoji Yuen:
Testing Preorders for Probabilistic Processes. Inf. Comput. 154(2): 93-148 (1999) - [j17]Rance Cleaveland:
Pragmatics of Model Checking: An STTT Special Section. Int. J. Softw. Tools Technol. Transf. 2(3): 208-218 (1999) - [j16]Xiaoqun Du, Scott A. Smolka, Rance Cleaveland:
Local Model Checking and Protocol Analysis. Int. J. Softw. Tools Technol. Transf. 2(3): 219-241 (1999) - [c50]Rance Cleaveland:
Temporal Process Logic (Abstract). CONCUR 1999: 1 - [c49]Gerald Lüttgen, Michael von der Beeck, Rance Cleaveland:
Statecharts Via Process Algebra. CONCUR 1999: 399-414 - [c48]Markus Müller-Olm, Bernhard Steffen, Rance Cleaveland:
On the Evolution of Reactive Components: A Process-Algebraic Approach. FASE 1999: 161-175 - [c47]Murali Narasimha, Rance Cleaveland, S. Purushothaman Iyer:
Probabilistic Temporal Logics via the Modal Mu-Calculus. FoSSaCS 1999: 288-305 - [e4]