Rance Cleaveland

Professor
5160 Iribe Center
(301) 405-2739
Academic Web Page
Education: 
Ph.D., Cornell University (Computer Science)
Special Awards/Honors: 
ONR Young Investigator Award
National Science Foundation (NSF) National Young Investigator
Biography: 

Rance Cleaveland is a professor of computer science.

His research focuses on the area of formal methods for desciption and analysis of concurrent and distributed systems. Specifically, Cleaveland's work includes processing algebra, temporal logic, analysis algorithms for finite-state systems, automatic verification tools, semantic models of system behavior, and operational semantics.

He is the executive and scientific director of the Fraunhofer USA Center for Experimental Software Engineering.

Cleaveland received his doctorate in computer science from Cornell University. Before coming to the University of Maryland, he was a member of the computer science faculty at the State University of New York at Stony Brook.

Go here to view Cleaveland‘s academic publications on Google Scholar.

Publications

2009


Ackermann C, Lindvall M, Cleaveland R.  2009.  Recovering Views of Inter-System Interaction Behaviors. Reverse Engineering, Working Conference on. :53-61.

Ray A, Morschhaeuser I, Ackermann C, Cleaveland R, Shelton C, Martin C.  2009.  Validating Automotive Control Software Using Instrumentation-Based Verification. Automated Software Engineering, International Conference on. :15-25.

Hierons RM, Krause P, Lüttgen G, Simons AJH, Vilkomir S, Woodward MR, Zedan H, Bogdanov K, Bowen JP, Cleaveland R et al..  2009.  Using formal specifications to support testing. ACM Computing Surveys. 41:1-76.

2008


Ray A, Cleaveland R.  2008.  Executable Specifications for Real-Time Distributed Systems. Electronic Notes in Theoretical Computer Science. 203(4):3-17.

Ackermann C, Ray A, Cleaveland R, Heit J, Martin C, Shelton C.  2008.  Model Based Design Verification: A Monitor Based Approach. 2008-01-0741

Cleaveland R, Smolka S, Sims S.  2008.  An instrumentation-based approach to controller model validation. Model-Driven Development of Reliable Automotive Services. :84-97.

2007


Cleaveland R, Lüttgen G, Natarajan V.  2007.  Priority and abstraction in process algebra. Information and Computation. 205(9):1426-1458.

2006


Lee I, Pappas GJ, Cleaveland R, Hatcliff J, Krogh BH, Lee P, Rubin H, Sha L.  2006.  High-confidence medical device software and systems. Computer. 39(4):33-38.

Ray A, Cleaveland R.  2006.  A Software Architectural Approach to Security by Design. Computer Software and Applications Conference, 2006. COMPSAC '06. 30th Annual International. 2:83-86.

Stark E, Cleaveland R, Smolka S.  2006.  Probabilistic I/O automata: Theories of two equivalences. CONCUR 2006–Concurrency Theory. :343-357.

Ray A, Cleaveland R, Jiang S, Fuhrman T.  2006.  Model based verification and validation of distributed control architectures. Proceedings of Convergence Convergence International Congress and Exposition on Transportation Electronics, Detroit, USA.

2005


Zhang D, Cleaveland R.  2005.  Fast on-the-fly parametric real-time model checking. Real-Time Systems Symposium, 2005. RTSS 2005. 26th IEEE International. :10–pp-10–pp.

Cleaveland R, Iyer PS, Narasimha M.  2005.  Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science. 342(2-3):316-350.

Sengupta B, Cleaveland R.  2005.  An integrated framework for scenarios and state machines. Integrated Formal Methods. :366-385.

Zhang D, Cleaveland R.  2005.  Efficient temporal-logic query checking for presburger systems. Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering. :24-33.

Zhang D, Cleaveland R.  2005.  Fast generic model-checking for data-based systems. Formal Techniques for Networked and Distributed Systems-FORTE 2005. :83-97.

Ray A, Sengupta B, Cleaveland R.  2005.  Secure requirements elicitation through triggered message sequence charts. Distributed Computing and Internet Technology. :273-282.

Sengupta B, Cleaveland R.  2005.  Executable requirements specifications using triggered message sequence charts. Distributed Computing and Internet Technology. :482-493.

Ray A, Cleaveland R, Skou A.  2005.  An Algebraic Theory Of Boundary Crossing Transitions. Electronic Notes in Theoretical Computer Science. 115:69-88.

2004


Hansel D, Cleaveland R, Smolka SA.  2004.  Distributed prototyping from validated specifications. Journal of Systems and Software. 70(3):275-298.

Ray A, Cleaveland R.  2004.  Formal Modeling Of Middleware-based Distributed Systems. Electronic Notes in Theoretical Computer Science. 108:21-37.

Ray A, Cleaveland R.  2004.  Unit verification: the CARA experience. International Journal on Software Tools for Technology Transfer (STTT). 5(4):351-369.

2003


Zhang D, Cleaveland R, Stark EW.  2003.  The integrated CWB-NC/PIOAtool for functional verification and performance analysis of concurrent systems. Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems. :431-436.

Ray A, Cleaveland R.  2003.  Architectural Interaction Diagrams: AIDs for System Modeling. Software Engineering, International Conference on. :396-396.

Stark EW, Cleaveland R, Smolka SA.  2003.  A process-algebraic language for probabilistic I/O automata. CONCUR 2003-Concurrency Theory. :193-207.

Sengupta B, Cleaveland R.  2003.  TRIM: A tool for triggered message sequence charts. Computer Aided Verification. :106-109.

Sengupta B, Cleaveland R.  2003.  Towards formal but flexible scenarios. 2nd International Workshop on Scenarios and State Machines: Models, Algorithms and Tools.

2002


Cleaveland R, Sims ST.  2002.  Generic tools for verifying concurrent systems. Science of Computer Programming. 42(1):39-47.

Tan L, Cleaveland R.  2002.  Evidence-based model checking. Computer Aided Verification. :641-680.

Sengupta B, Cleaveland R.  2002.  Triggered message sequence charts. ACM SIGSOFT Software Engineering Notes. 27:167-167.

2001


Cleaveland R, Sokolsky O.  2001.  Equivalence and preorder checking for finite-state systems. Handbook of Process Algebra. :391-424.

Tan L, Cleaveland R.  2001.  Simulation revisited. Tools and Algorithms for the Construction and Analysis of Systems. :480-495.

Sims S, Cleaveland R, Butts K, Ranville S.  2001.  Automated Validation of Software Models. Automated Software Engineering, International Conference on. :91-91.

Bhat GS, Cleaveland R, Groce A.  2001.  Efficient Model Checking Via Buchi Tableau Automata⋆. Computer aided verification: 13th International conference, CAV 2001, Paris, France, July 18-22, 2001: proceedings. 2102:38-38.

2000


L\üttgen G, Von Der Beeck M, Cleaveland R.  2000.  A compositional approach to statecharts semantics. 25

Cleaveland R, L\üttgen G.  2000.  A semantic theory for heterogeneous system design. FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. :312-324.

Cleaveland R, Du X, Smolka S.  2000.  GCCS: A graphical coordination language for system specification. Coordination Languages and Models. :207-212.

1999


M\üller-Olm M, Steffen B, Cleaveland R.  1999.  On the evolution of reactive components: A process-algebraic approach. Lecture notes in computer science. :161-175.

Bhat G, Cleaveland R, L\üttgen G.  1999.  A practical approach to implementing real-time semantics. Annals of Software Engineering. 7(1):127-155.

Liittgen G, Cleaveland R.  1999.  Statecharts via process algebra. CONCUR'99: concurrency theory: 10th International Conference, Eindhoven, the Netherlands, August 24-27, 1999: proceedings. :399-399.

Du X, Smolka SA, Cleaveland R.  1999.  Local model checking and protocol analysis. International Journal on Software Tools for Technology Transfer (STTT). 2(3):219-241.

Bernardo M, Cleaveland R.  1999.  A Theory of Efficiency for Markovian Processes. University of Bologna.

1998


Philippou A, Cleaveland R, Lee I, Smolka S, Sokolsky O.  1998.  Probabilistic resource failure in real-time process algebra. CONCUR'98 Concurrency Theory. :465-472.

Kumar KN, Cleaveland R, Smolka SA.  1998.  Infinite Probabilistic and Nonprobabilistic Testing⋆. Foundations of software technology and theoretical computer science: 18th Conference, Chennai, India, December 17-19, 1998: proceedings. :209-209.

1997


Cleaveland R, L\üttgen G, Mendler M.  1997.  An algebraic theory of multiple clocks. CONCUR'97: Concurrency Theory. :166-180.

Bhat G, Cleaveland R, L\üttgen G.  1997.  Dynamic priorities for modeling real-time. Proc. of the Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE X/PSTV XVII’97). :321-336.

1996


Bhat G, Cleaveland R.  1996.  Efficient model checking via the equational μ-calculus. , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings. :304-312.

Bhat G, Cleaveland R.  1996.  Efficient local model-checking for fragments of the modal $\mu$-calculus. Tools and Algorithms for the Construction and Analysis of Systems. :107-126.

Cleaveland R, Natarajan V, Sims S, Luettgen G.  1996.  Modeling and verifying distributed systems using priorities: A case study. Software - Concepts and Tools. 17(2):50-62.

Natarajan V, Cleaveland R.  1996.  An algebraic theory of process efficiency. , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings. :63-72.

Natarajan V, Cleaveland R.  1996.  Predictability of real-time systems: a process-algebraic approach. Real-Time Systems Symposium, IEEE International. :82-82.

Cleaveland R, Sims S.  1996.  The NCSU concurrency workbench. Computer Aided Verification. :394-397.

Cleaveland R, L\üttgen G, Natarajan V.  1996.  A process algebra with distributed priorities. CONCUR'96: Concurrency Theory. :34-49.

Cleaveland R, L\üttgen G, Natarajan V, Sims S.  1996.  Priorities for modeling and verifying distributed systems. Tools and Algorithms for the Construction and Analysis of Systems. :278-297.

Elseaidy WM, Baugh JW, Cleaveland R.  1996.  Verification of an active control system using temporal process algebra. Engineering with computers. 12(1):46-61.

Cleaveland R.  1996.  Semantic theories and system design. ACM Computing Surveys (CSUR). 28(4es):41-41.

Cleaveland R, Lewis P, Smolka S, Sokolsky O.  1996.  The Concurrency Factory: A development environment for concurrent systems. Computer Aided Verification. :398-401.

1995


Celikkan U, Cleaveland R.  1995.  Generating diagnostic information for behavioral preorders. Distributed computing. 9(2):61-75.

Cleaveland R, Iyer P, Yankelevich D.  1995.  Optimality in abstractions of model checking. Static Analysis. :51-63.

Bhat G, Cleaveland R, Grumberg O.  1995.  Efficient on-the-fly model checking for CTL. , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. :388-397.

Natarajan V, Cleaveland R.  1995.  Divergence and fair testing. Automata, Languages and Programming. :648-659.

Cleaveland R, Madelaine E, Sims S.  1995.  A front-end generator for verification tools. Tools and Algorithms for the Construction and Analysis of Systems. :153-173.

1994


Elseaidy WM, Cleaveland R, Baugh JW.  1994.  Verifying an intelligent structural control system: a case study. Real-Time Systems Symposium, 1994., Proceedings.. :271-275.

Yuen S, Cleaveland R, Dayar Z, Smolka S.  1994.  Fully abstract characterizations of testing preorders for probabilistic processes. CONCUR'94: Concurrency Theory. :497-512.

Cleaveland R, Yankelevich D.  1994.  An operational framework for value-passing processes. Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. :326-338.

1993


Fredette AN, Cleaveland R.  1993.  A generalized approach to real-time schedulability analysis. IEEE Real-Time Systems Newsletter. 9(1-2):98-103.

Cleaveland R, Steffen B.  1993.  A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal methods in system design. 2(2):121-147.

Cleaveland R.  1993.  Analyzing concurrent systems using the Concurrency Workbench. Functional Programming, Concurrency, Simulation and Automated Reasoning. :129-144.

Cleaveland R, Parrow J, Steffen B.  1993.  The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems. 15:36-72.

Fredette AN, Cleaveland R.  1993.  RTSL: a language for real-time schedulability analysis. Real-Time Systems Symposium, 1993., Proceedings.. :274-283.

Pages