Welcoming Grigore Rosu as Advisor to Elrond
When taking into consideration recent developments and current market conditions, some might get discouraged about what the future holds. For, this is the best time to double down, focus, and give the best we have. Thus, it is with great pleasure that we strengthen our project by on-boarding yet another experienced advisor.
After looking closely into Runtime Verification’s work, we understood that Grigore Rosu can bring to the team the best expertise we could possibly get in terms of smart contract language design and formal verification. He is working closely with our team on adapting existing smart contract languages such as IELE, Solidity and Wasm to operate on the Elrond VM.
About Grigore Rosu:
Grigore Rosu is a professor in the Department of Computer Science at the Universy of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the founder and president of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages.
Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean’s award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005.
He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper that helped shape the runtime verification field), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002. He was ranked a UIUC excellent teacher in Spring 2013, Fall 2012, Spring 2008 and Fall 2004.
Short chat with Grigore
Q: What was it about Elrond that captured your interest?
First and foremost was the fact that it has very high ambitions: performance, correctness, scalability, generality. I love challenges and feel most attracted by projects that seem close to impossible to achieve, yet they can be achieved if you do things just right. You need a very strong team and a thorough understanding of the underlying technology, though.
Second, the fact that it was located in Romania. I grew up and got my college and M.S. degrees at the University of Bucharest, Romania. I know how talented people are in Romania and how they can do magic if they are given the right cause and the resources to unleash their creativity.
In fact, my company Runtime Verification has also just started a subsidiary in Romania, for the exact same reason. Third, because this advisory collaboration with Elrond can grow into something bigger, where our companies can collaborate on a larger scale offering the most secure and formally correct, yet efficient blockchain technology on the market.
Q: Tell us a bit about your experience at NASA
I started working at NASA in 2000, right after completing my PhD at the University of California. As a research scientist in formal methods, my mission was to develop formal approaches to complex system specification and verification. I first worked on program synthesis for navigation software, where the idea was to generate the spacecraft navigation programs directly from their formal specification, correct by construction.
That was when I learned that you cannot have everything, automatically: if you want correct-by-construction software synthesis, then you need to restrict the domain. Sometimes more than you want. Then I worked on program verification, specifically model checking and a bit on deductive verification. That is, you are given a program and a formal specification, and you have to prove that all program’s behaviors meet the specification. That was when I learned that fully fledged program verification does not scale: you either have a state explosion problem, or you need a human expert to guide the verification process by proposing helping lemmas.
Finally, I also worked on dynamic analysis of concurrency errors, which are notoriously hard to detect statically. There I learned that dynamic analysis can actually be quite useful if done properly, in particular if combined with the other two topics I’ve been exposed to at NASA, namely synthesis and verification. The idea was to automatically synthesize monitors for the safety properties of interest, then to verify the properties dynamically, using the monitors. If you also provide provably correct backup for how to steer the system when properties are violated, you end up with a provably correct system while avoiding the hard problem of verifying it directly.
This idea led to a novel formal verification approach, which my NASA colleague Klaus Havelund and I called “runtime verification” back in 2001. In the meanwhile the term we coined got traction, now having its own annual international conference called Runtime Verification (RV) and tracks in, many formal methods, software engineering and programming language conferences. Klaus and I recently got two awards for papers that proposed the approach: one Most Influential Paper award in 2017 for a paper published in the ASE 2001 conference, and one Test of Time award in 2018 for a paper published in RV 2001.
The runtime verification area evolved significantly since its inception in 2001, and my homonymous startup company is incorporating into its products and technologies the most successful and feasible ideas proposed by the runtime verification comunity. I am very grateful to NASA and my colleague Klaus Havelund for the opportunity to work on real-world problems and the experience that came with it. It was a very good decision to work at NASA before joining academia again as a professor. I looked at research and science differently ever since.
Q: What other passions do you have?
I love building things with my hands, and the more challenging they are the better I feel about it. For example, I am currently building a four-seater airplane in my garage (a Velocity canard airplane). I also like flying airplanes; I am a private pilot, VFR certified. Back in college I was also enrolled in an aerobatics camp, where I flew Zlin Czech airplanes, as well as in the Romanian Alpine Club, but I gave up both of these passions in order to focus on mathematics, which was my first love, always. I also like playing Go; I am a 2-dan amateur player.
And I like grilling steak and the red wine that comes with it. But at the essence of everything I do is a desire for perfection. I like formal methods and formal design of programming languages and virtual machines, as well as formal verification of programs and in particular of smart contracts, because all of these have a mathematically rigorous definition for what “correct” means. So you can approach the problem on a very rigorous basis, where absolute correctness is possible.
We’re delighted to have Grigore as advisor and we’re looking forward to continue developing great technology together.
Elrond’s official outlets:
- Elrond Community Platform: https://community.elrond.com
- Twitter: https://twitter.com/elrondnetwork
- Official website: www.elrond.com
- Elrond Github: https://github.com/ElrondNetwork
