Keynote Speakers
Robert de Simone, INRIA
Multiform Logical Time for Me/Mo-codesign
There is now a consistent corpus of models and methods for software/hardware codesign (scope of MeMoCoDe). Still, while success is quite established at both ends of the spectrum (High-Level hardware Synthesis, and System Engineering), the adoption of such Software modeling approach inside mainstream Software Engineering communities could easily be improved. This is certainly so because some of the principles of application modeling do not exactly match, or elsewhere do not focus upon the same concerns, as traditional coding style. Putting forth the relevant important concepts for application modeling, while investigating their relevance to traditional engineering experience, is certainly a way to counter confusion. We view the notion of Multiform Logical Time as such a fundamental concept. In a first part of the talk we consider the premises of Multiform Logical Time in Embedded Design (its origin, its relevance at places of design flows); in a second part we introduce a small declarative language to express logical time properties, study its expressiveness and its associated analysis techniques.
Sriram Rajamani, Microsoft Research
Trusted Cloud: How to make the cloud more secure.
Cloud computing is growing because of cost advantages and convenience it offers to customers. However, security and privacy continue to be major concerns. We wish to guard against a powerful adversary who can compromise the CloudOS, and uses all privileges of the CloudOS to compromise the integrity and confidentiality of user applications. Secure hardware and/or small trusted hypervisors are the main weapons in our arsenal to guard against such powerful adversaries. Secure hardware (such as Intel SGX) enables user mode applications to package code and data into regions that are isolated from all other software running on the machine. Isolated regions can also be implemented with a small trusted hypervisor. However, it is an open research question as to how entire cloud services can be built using trusted hardware as a primitive, while maintaining a small TCB, providing good performance and end-to-end security guarantees. The Trusted Cloud project at Microsoft Research explores ways to answer this question, and it builds on techniques spanning hardware, OS, compilers and verification tools. In this talk, I will describe our efforts on architecting trusted and more secure cloud services using these principles.
André Platzer, Carnegie Mellon University
How to Prove Hybrid Systems
Hybrid systems combine discrete dynamics with continuous dynamics along differential equations. They arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one? This talk describes how hybrid systems can be proved using differential dynamic logic. Differential dynamic logic (dL) provides compositional logics, programming languages, and reasoning principles for hybrid systems. As implemented in the theorem prover KeYmaera X, dL has been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robot system for skull-base surgery.