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.
2009. Recovering Views of Inter-System Interaction Behaviors. Reverse Engineering, Working Conference on. :53-61.
2009. Validating Automotive Control Software Using Instrumentation-Based Verification. Automated Software Engineering, International Conference on. :15-25.
2009. Using formal specifications to support testing. ACM Computing Surveys. 41:1-76.
2008. Executable Specifications for Real-Time Distributed Systems. Electronic Notes in Theoretical Computer Science. 203(4):3-17.
2008. Model Based Design Verification: A Monitor Based Approach. 2008-01-0741
2008. An instrumentation-based approach to controller model validation. Model-Driven Development of Reliable Automotive Services. :84-97.
2007. Priority and abstraction in process algebra. Information and Computation. 205(9):1426-1458.
2006. High-confidence medical device software and systems. Computer. 39(4):33-38.
2006. A Software Architectural Approach to Security by Design. Computer Software and Applications Conference, 2006. COMPSAC '06. 30th Annual International. 2:83-86.
2006. Probabilistic I/O automata: Theories of two equivalences. CONCUR 2006–Concurrency Theory. :343-357.
2006. Model based verification and validation of distributed control architectures. Proceedings of Convergence Convergence International Congress and Exposition on Transportation Electronics, Detroit, USA.
2005. Fast on-the-fly parametric real-time model checking. Real-Time Systems Symposium, 2005. RTSS 2005. 26th IEEE International. :10–pp-10–pp.
2005. Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science. 342(2-3):316-350.
2005. An integrated framework for scenarios and state machines. Integrated Formal Methods. :366-385.
2005. Efficient temporal-logic query checking for presburger systems. Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering. :24-33.
2005. Fast generic model-checking for data-based systems. Formal Techniques for Networked and Distributed Systems-FORTE 2005. :83-97.
2005. Secure requirements elicitation through triggered message sequence charts. Distributed Computing and Internet Technology. :273-282.
2005. Executable requirements specifications using triggered message sequence charts. Distributed Computing and Internet Technology. :482-493.
2005. An Algebraic Theory Of Boundary Crossing Transitions. Electronic Notes in Theoretical Computer Science. 115:69-88.
2004. Distributed prototyping from validated specifications. Journal of Systems and Software. 70(3):275-298.
2004. Formal Modeling Of Middleware-based Distributed Systems. Electronic Notes in Theoretical Computer Science. 108:21-37.
2004. Unit verification: the CARA experience. International Journal on Software Tools for Technology Transfer (STTT). 5(4):351-369.
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.
2003. Architectural Interaction Diagrams: AIDs for System Modeling. Software Engineering, International Conference on. :396-396.
2003. A process-algebraic language for probabilistic I/O automata. CONCUR 2003-Concurrency Theory. :193-207.
2003. TRIM: A tool for triggered message sequence charts. Computer Aided Verification. :106-109.
2003. Towards formal but flexible scenarios. 2nd International Workshop on Scenarios and State Machines: Models, Algorithms and Tools.
2002. Generic tools for verifying concurrent systems. Science of Computer Programming. 42(1):39-47.
2002. Evidence-based model checking. Computer Aided Verification. :641-680.
2002. Triggered message sequence charts. ACM SIGSOFT Software Engineering Notes. 27:167-167.
2001. Equivalence and preorder checking for finite-state systems. Handbook of Process Algebra. :391-424.
2001. Simulation revisited. Tools and Algorithms for the Construction and Analysis of Systems. :480-495.
2001. Automated Validation of Software Models. Automated Software Engineering, International Conference on. :91-91.
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. A semantic theory for heterogeneous system design. FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. :312-324.
2000. GCCS: A graphical coordination language for system specification. Coordination Languages and Models. :207-212.
1999. On the evolution of reactive components: A process-algebraic approach. Lecture notes in computer science. :161-175.
1999. A practical approach to implementing real-time semantics. Annals of Software Engineering. 7(1):127-155.
1999. Statecharts via process algebra. CONCUR'99: concurrency theory: 10th International Conference, Eindhoven, the Netherlands, August 24-27, 1999: proceedings. :399-399.
1999. Local model checking and protocol analysis. International Journal on Software Tools for Technology Transfer (STTT). 2(3):219-241.
1999. A Theory of Efficiency for Markovian Processes. University of Bologna.
1998. Probabilistic resource failure in real-time process algebra. CONCUR'98 Concurrency Theory. :465-472.
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. An algebraic theory of multiple clocks. CONCUR'97: Concurrency Theory. :166-180.
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. Efficient model checking via the equational μ-calculus. , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings. :304-312.
1996. Efficient local model-checking for fragments of the modal $\mu$-calculus. Tools and Algorithms for the Construction and Analysis of Systems. :107-126.
1996. Modeling and verifying distributed systems using priorities: A case study. Software - Concepts and Tools. 17(2):50-62.
1996. An algebraic theory of process efficiency. , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings. :63-72.
1996. Predictability of real-time systems: a process-algebraic approach. Real-Time Systems Symposium, IEEE International. :82-82.
1996. The NCSU concurrency workbench. Computer Aided Verification. :394-397.
1996. A process algebra with distributed priorities. CONCUR'96: Concurrency Theory. :34-49.
1996. Priorities for modeling and verifying distributed systems. Tools and Algorithms for the Construction and Analysis of Systems. :278-297.
1996. Verification of an active control system using temporal process algebra. Engineering with computers. 12(1):46-61.
1996. Semantic theories and system design. ACM Computing Surveys (CSUR). 28(4es):41-41.
1996. The Concurrency Factory: A development environment for concurrent systems. Computer Aided Verification. :398-401.
1995. Generating diagnostic information for behavioral preorders. Distributed computing. 9(2):61-75.
1995. Optimality in abstractions of model checking. Static Analysis. :51-63.
1995. Efficient on-the-fly model checking for CTL. , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. :388-397.
1995. Divergence and fair testing. Automata, Languages and Programming. :648-659.
1995. A front-end generator for verification tools. Tools and Algorithms for the Construction and Analysis of Systems. :153-173.
1994. Verifying an intelligent structural control system: a case study. Real-Time Systems Symposium, 1994., Proceedings.. :271-275.
1994. Fully abstract characterizations of testing preorders for probabilistic processes. CONCUR'94: Concurrency Theory. :497-512.
1994. An operational framework for value-passing processes. Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. :326-338.
1993. A generalized approach to real-time schedulability analysis. IEEE Real-Time Systems Newsletter. 9(1-2):98-103.
1993. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal methods in system design. 2(2):121-147.
1993. Analyzing concurrent systems using the Concurrency Workbench. Functional Programming, Concurrency, Simulation and Automated Reasoning. :129-144.
1993. The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems. 15:36-72.
1993. RTSL: a language for real-time schedulability analysis. Real-Time Systems Symposium, 1993., Proceedings.. :274-283.