Keynote Speakers
Edward A. Lee (UC Berkely)
Title: Deterministic Concurrency in Cyber-Physical Systems
Popular frameworks based on publish-and-subscribe, service-oriented architectures, and actor networks have simplified the development of parallel and distributed software. Most of these, however, are intrinsically nondeterministic. This talk will examine some of the risks that this introduces to applications, particularly cyber-physical applications. I will then introduce an international collaboration that aims to fix the problem through a polyglot coordination language called Lingua Franca (LF). I will show that deterministic concurrency does not automatically imply a cost in performance. Finally, I will focus on how LF enables navigating the fundamental and unavoidable tradeoff between consistency and availability in distributed systems.
Rolf Drechsler (University of Bremen)
Title: Next-Generation Automatic Human-Readable Proofs Enabling Polynomial Formal Verification
Within the past years, the complexity of digital circuits has grown significantly, resulting in an increased difficulty of their verification. Only based on formal verification techniques, the correctness of a circuit can be fully guaranteed. However, the verification of circuits using formal verification techniques generally requires exponential time and space in the worst case. During the verification process, the formal representations of functions, e.g. BDDs, can have an exponential size, resulting in an exponential verification complexity. Thus, recently the concept of Polynomial Formal Verification (PFV) has been introduced, where polynomial upper bounds are proven for the verification complexity. This has been done successfully e.g. for adders and multipliers. Polynomial upper bounds have been proven manually, but it has not been researched yet, how they can be proven automatically. Here, we present the concepts for EDA tools with support for automatic generation of human-readable proofs in the context of PFV.