Title: A Logical Framework for Developing and Mechanizing Set Theories
Abstract: We describe a framework for formalizing mathematics whichis based on the usual set theoretical foundations of mathematics. Its most important feature is that it reflects real mathematical practice in making an extensive use of statically defined abstract set terms, in the same way they are used in ordinary mathematical discourse. We also show how large portions of scientifically applicable mathematics can be developed in this framework in a straightforward way, using just rather weak set theories which are predicatively acceptable. The key property of those theories is that every object which is used in it is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented interpretation. However,the development is not committed to such interpretation, and can easily be extended for handling stronger set theories, including ZF itself.
Short Biography: Arnon Avron got his Ph.D. in mathematics from Tel Aviv University in 1985. After finishing his thesis,he spent his pot-doc period at the laboratory for the foundationsof computer science (LFCS) at Edinburgh university, where he belonged to the original LF team- the first computerized logical framework. In 1988 he joined the computer science department of Tel Aviv University, where he is a full professor. Avron is on the editorial boards of TheoreticalComputer Science, Journal of Logic and Computation, and Logica Universalis. Most of his research is in logic-related areas, like proof systems, automated reasoning (especially the mechanization of mathematics), nonclassical logics, logical frameworks, and foundations of logic and of mathematics (where he is mainly interested in the predicativist approach). However, he made contributions also to geometry and to graph theory.
Title: Verification of differential private computations
Abstract: Differential privacy is a statistical notion of privacy which achieves compelling trade-offs between input privacy and accuracy (of outputs). Differential privacy is also an attractive target for verification: despite their apparent simplicity, recently proposed algorithms have intricate privacy and accuracy proofs. We present two program logics for reasoning about privacy and accuracy properties of probabilistic computations. The accuracy logic captures reasoning about the union bound, a simple but effective tool from probablility theory, whereasthe privacy logic captures fine-grained reasoning about probabilistic couplings, a powerful tool for studying Markov chains. We illustrate the strengths of our program logics with novel and elegant proofs of challenging examples from differential privacy. Finally, we discuss the relationship between our approach and general-purpose frameworks for the verification of probabilistic programs.
Short Biography: Gilles Barthe is a research professor at the IMDEA Software Institute. His research interests include logic, formal verification, programming languages, and security. His current work focuses on verification and synthesis methods for cryptography and differential privacy. He is a member of the editorial boards of the Journal of Automated Reasoningand Journal of Computer Security.Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in 1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004.
Title: Programming by Examples: Applications, Algorithms, and Ambiguity Resolution
Abstract: 99% of computer end users do not know programming, and struggle with repetitive tasks. Programming by Examples (PBE) can revolutionize this landscape by enabling users to synthesize intended programs from example based specifications.A key technical challenge in PBE is to search for programs that are consistent with the examples provided by the user. Our efficient search methodology is based on two key ideas: (i) Restriction of the search space to an appropriate domain-specific language that offers balanced expressivity and readability (ii) A divide-and-conquer based deductive search paradigm that inductively reduces the problem of synthesizing a program of a certain kind that satisfies a given specification into sub-problems that refer to sub-programs or sub-specifications.Another challenge in PBE is to resolve the ambiguity in the example based specification. We will discuss two complementary approaches: (a) machine learning based ranking techniques that can pick an intended program from among those that satisfy the specification, and (b) active-learning based user interaction models.The above concepts will be illustrated using FlashFill, FlashExtract, and FlashRelate---PBE technologies for data manipulation domains. These technologies, which have been released inside various Microsoft products, are useful for data scientists who spend 80% of their time wrangling with data. The Microsoft PROSE SDK allows easy construction of such technologies.
Short Biography: Sumit Gulwani is a Research manager and a Principal researcher at Microsoft, and an affiliate faculty in the Computer Science Department at UW. He has expertise in formal methods and automated program analysis and synthesis techniques. His recent research interests lie in the cross-disciplinary areas of automating end-user programming, and building intelligent tutoring systems (for various subject domains including programming, math, logic, and automata). His programming-by-example work led to the Flash Fill feature of Microsoft Excel 2013 that is used by hundreds of millions of people. He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014. He obtained his PhD in Computer Science from UC-Berkeley in 2005, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in Computer Science and Engineering from IIT Kanpur in 2000, and was awarded the President's Gold Medal.
Abstract: Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which 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 highlights some of the most fascinating aspects of cyber-physical systems and their dynamical systems models, such as hybrid systems combining discrete transitions and continuous evolution along differential equations. Because of the impact that they can have on the real world, CPSs deserve proof as safety evidence.We take the view of multi-dynamical systems, which understand complex systems as a combination of multiple elementary dynamical aspects to tame their complexity by compositionality. This compositionality is achieved in the family of differential dynamic logics, which provide compositional logics, programming languages, and reasoning principles for CPS.Differential dynamic logics, as implemented in the theorem prover KeYmaera X, have 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 robotic system for skull-base surgery. This combination of strong theoretical foundations with practical theorem proving challenges and relevant applications makes logic for CPS a very rewarding research area.
Short Biography: André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes.André Platzer has a Ph.D. from the University of Oldenburg in Germany and received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER award. He received best paper awards at TABLEAUX'07 and FM'09 and was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI's 10 to Watch by the IEEE Intelligent Systems Magazine.
