Abstract: Formal inductive synthesis refers to the synthesis of artifacts from examples/observations so as to satisfy a formal specification. In this lecture, we will study a theory of formal inductive synthesis and its applications to the specification, verification, and design of systems, with a particular focus on cyber-physical systems. We will also discuss interesting connections between machine learning and formal methods that provide promising directions for research.

Bio: Sanjit A. Seshia is an Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in cyber-physical systems, computer security, electronic design automation, and synthetic biology. His Ph.D. thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a widely-used textbook on embedded systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE) from the White House, an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.

Abstract: Sequential Equivalence Checking has emerged as a widely used application of formal technologies over the last decade, significantly enhancing the quality of hardware design and verification. In this tutorial, we will look at the multitude of applications of sequential equivalence checking, ranging from enabling design closure, validating against high-level reference models to enabling sequential synthesis, technology mapping and import of design IP. We will spend some time immersing ourselves into setting up of sequential equivalence checking testbenches. Finally, we will whet our appetite for algorithms by diving into illuminating details of scalable sequential redundancy identification.

Bio: Hari Mony is the Technical Team Lead for IBM's formal verification and sequential equivalence checking tool, RuleBase-SixthSense. He received an M.S. and Ph.D. in Computer Engineering from University of Texas at Austin, and a B.Tech. in Electrical Engineering from the Indian Institute of Technology, Kharagpur. His Ph.D. thesis work on scalable sequential redundancy identification is the basis for the core sequential equivalence checking engines in RuleBase-SixthSense. He is currently focused on enabling widespread application of formal technologies for hardware design and verification at IBM. He is designated as a Master Inventor @ IBM and has been issued 88 US patents.

Abstract: And again, the world of HW & SW engineering is re-inventing itself. This time it is about safety. As computers move out of the virtual world and begin participating in the real world (driving cars, controlling plants, controlling cities and traffic jams, etc,) the demands for safety grow dramatically. What is needed is Trustworthiness, defined[*] as the sum of Safety, Reliability, Availability Resilience and Security. This tutorial will discuss how to ensure Trustworthiness, taking the Automotive industry as an example. We will show how the Automotive standard (ISO-26262) goes through five stages of protection:
* Identifying potential risks
* Preventing preventable risks
* Assessing remaining risks
* Detecting materializing hazards
* Responding safely to detected hazards

http://www.uk-tsi.org/trustworthiness.

Bio: Amir Rahat is the VP of R&D at Optima Design Automation Ltd., a Nazareth-based start-up that solves the Functional Safety (FuSA) problem for VLSI chips that need protection from soft-error and hard-error faults. Before joining Optima DA, Amir worked for 27 years in Intel's internal CAD organization, where he held senior technical and managerial roles across a wide range of EDA domains. Amir received his BSc and MSc degrees in CS from the Technion in Israel.

Abstract: Dynamic symbolic execution has gathered a lot of attention in recent years as an effective technique for generating high-coverage test suites and finding deep errors in complex software applications. In this tutorial, I will introduce the main concepts and challenges of dynamic symbolic execution and illustrate them via concrete examples and demos in the context of our KLEE symbolic execution infrastructure. The talk is primarily targeted to those who have no direct experience with dynamic symbolic execution and KLEE, but it will also include parts of interest to a more specialist audience.

Bio: Cristian Cadar is a Reader (Associate Professor) in the Department of Computing at Imperial College London, where he leads the Software Reliability Group. His research interests span the areas of software engineering, computer systems and security, with an emphasis on building practical techniques and tools for improving the reliability and security of software systems, such as the symbolic execution engine KLEE being presented in this talk. He was elected as a Fellow of the British Computer Society in 2016, awarded the EuroSys Jochen Liedtke Young Researcher Award in 2015, an EPSRC Early-Career Fellowship in 2013, and artifact or paper awards at ICST 2016, ISSTA 2014, ESEC/FSE 2013 and OSDI 2008. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.