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


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

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

2007


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

2006


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.

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.

2005


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.

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.

2004


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.

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

2003


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.

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.

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


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.

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.

2000


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.

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

1999


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.

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.

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


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.

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.

1995


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.

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.

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


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.

Cleaveland R.  1993.  An operational semantics of value passing. Proceedings 2nd North American Process Algebra Workshop, Ithaca, New York.

Pages