Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) are announcing a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. We believe this effort will yield a number of useful tools and artifacts, and can lay the foundation for the future of principled and formally rigorous smart contract development.
Runtime Verification Inc. is going to be presenting an exciting tutorial at the RV'16 conference, featuring all of our current tools and technologies and their practical and creative uses and applications.
If you are new (or a veteran) to runtime verification technology, we invite you to join and learn about what RV Inc.'s tools can do for your codebase, today. We look forward to seeing you in sunny, beautiful Madrid!