The future of robotics raises important questions for humanity. Will robots be able to act as agents in their own right and make moral and ethical decisions? Impressive advances in artificial intelligence mean robots may become capable of replacing human beings in every task imaginable. What are the ethical implications of such a development? How do we prepare for such a future? Questions on the ethics and morality of robotics were debated by panelists specializing in ethics, law, computer...

Amazon Web Services (AWS) uses and develops tools based on formal verification to reason about the security of AWS itself, as well as the security of systems that customers build on AWS. This talk will focus on how AWS services connect customers to logic-based techniques, as well as how AWS uses formal verification internally to provide higher assurance of its security. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales;...

George Gonthier delivers a lecture at FLoc2018 Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

An invited talk by the Emeritus Hillman University Professor of Computer Science, Philosophy and Mathematical Logic at Carnegie Mellon University at FLoC2018

In this talk I will describe what is known about pseudo-deterministic algorithms in the sequential, sub-linear and parallel setting. Probabilistic algorithms for both decision and search problems can offer significant complexity improvements over deterministic algorithms. One major difference, however, is that they may output different solutions for different choices of randomness. This makes correctness amplification impossible for search algorithms and is less than desirable in setting...

Formal reasoning about programs is one of the oldest and most fundamental research directions in computer science. It has also been one of the most elusive. There has been a tremendous amount of valuable research in formal methods, but rarely have formal reasoning techniques been deployed as part of the development process of large industrial codebases. This talk describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors...