Rance Cleaveland passed away on March 27, 2024. He will be missed

 
My friend and colleague Rance Cleaveland passed away on March 27, 2024 at the age of 62.  He was a professor at The University of Maryland at College Park in the Computer Science Department. He worked in Software Engineering. He did program verification and model checking. He had his own company, so he did both theoretical and practical work.

He joined UMCP in 2005. I had known him and some of his work before then so we got together for lunch about once a month to talk about the department(he was new to the dept. so I filled him in on things) and about computer science.He would probably be considered a theorist in Europe, though he was considered a Software Engineer in America.

The department's announcement is here

Below is

 
1) A note from Rance's Grad student Peter Fontana, who got his PhD in 2014.

2) An email that Jeroen Keiren sent to the concurrency mailinglist.

3) A picture of Peter, Jeroen, and Rance in that order left to right. 

-------------------------------------------

Peter Fontana's Note:

PERSONAL:

I’m truly shocked and saddened to hear that Rance Cleaveland passed away. Rance advised me (as a Ph.D. student of his at UMCP) in model checking (also called formal verification).

Rance was an extremely kind advisor and extremely skilled in leadership and communication. He also had all of the swiftness, communication, and people understanding of a skilled manager. He always encouraged us to find the simplest example possible to illustrate a nuanced corner-case of a property we wanted to prove or disprove. The simplicity made complicated things clearer. He was also an extremely clear communicator and extremely skilled with people. Rance was always patient and kind, eager to guide rather than to chastise.  I will truly miss him.

COMPUTER SCIENCE

Model checking involves the following:

(1) abstracting a programs as a state machine (automaton) with labels,

(2) writing a desirable property (such as “bad event X will never happen”) as a formula in a logic,

(3) using a computer to automatically show (over all possible cases) that the specified property is true or false.  This is model checking.

Theorists will note that this process of model checking is asking if state q of a machine satisfy a property phi, which is the model checking problem. If you are in the world of boolean formulas and propositions, the NP-complete satisfiability problem (SAT) asks: does there exists a boolean assignment q that s satisfy formula \phi? The analogous model checking problem is: given boolean assignment q (each proposition is either T or F), does q satisfy \phi? For boolean assignments, the model-checking problem is in P.

While Rance worked in a variety of areas related to formal verification that spanned process algebras, different logics, different automata types, and cyber-physical systems, with me we improved the art of timed automata model checking using a timed modal-mu calculus (timed logic). Timed automata and timed logics extend state machines by introducing a finite number of clocks. These clocks all advance (like time advancing) and can reset, and timed logics now have timing constraints (“within T time” is the most common constraint). We worked on extending the state of the art of what we could model-check on timed automata, both with theoretical proofs and by implementing a model checker (in C++) to model-check these richer timed properties. It turns out that this model checking work is decidable (model checking the simplest formulas in timed automata was previously shown to be PSPACE HARD).  I inherited work started by others, enhanced it, and passed it on; that work is currently being enhanced by others today. Our approach was novel in that we used a proof system of predicates and were able to model check more expressive formulas on timed automata with this enhanced system (See this paper). For details see my PhD thesis here.

----------------------------------------------------------------------------------------------

Jeroen Keiren's message to the concurrency mailinglist

Dear colleagues,

It is with great sadness that I share the news of the sudden and unexpected passing of
our colleague Rance Cleaveland on 27 March 2024.

My thoughts are with his family, friends and loved ones during this sad time.

I am convinced that those of us that interacted with Rance throughout his career will remember him as a friendly person. He was always happy to discuss research, but also dwell on more personal topics or give his honest, yet in my experience always constructive, advice.

Rance obtained his PhD at Cornell, and held academic positions at Sussex, NC State and Stony Brook, before accepting his current position at the University of Maryland, College Park in 2005. UMD shared an obituary for Rance here.

Rance was not only interested in the theoretical foundations of our field, witnessed by over 150 scientific publications. He also had a strong focus on building the tools (for instance the Concurrency Workbench), and commercializing it (through his company Reactis).

Rance was also an active member of our community. He was one of the co-founders of TACAS, for which he was still serving on the steering committee, as well as one of the co-founders of the Springer journal Software Tools for Technology Transfer.

In the words of his wife “For Rance, the concurrency community was truly his intellectual home and he appreciated working with colleagues in Europe and the US - and around the world.”

I’m sorry to bring this news.

With kind regards,

Jeroen Keiren
Assistant professor, Formal System Analysis group
Eindhoven University of Technology, The Netherlands

------------------------------------

A Picture of Peter, Jeroen, and Rance, left to right: