Prof. Cliff Jones

General lessons from a rely/guarantee development

Abstract:

Decomposing the design (or documentation) of large systems is a practical necessity; this prompts the need for a notion of compositional development methods; finding such methods for concurrent software is technically challenging because of the interference that characterises concurrency. This paper outlines the development of a difficult example in order to draw out lessons about such development methods. Although the “rely/guarantee” approach is employed in the example, the intuitions are more general.

Biography:

Cliff Jones is Professor of Computing Science at Newcastle University. He is best known for his research into "formal methods" for the design and verification of computer systems; under this heading, current topics of research include concurrency, support systems and logics. He is also currently applying research on formal methods to wider issues of dependability. Running up to 2007 his major research involvement was the five university IRC on "Dependability of Computer-Based Systems" of which he was overall Project Director - this was followed by a Platform Grant "Trustworthy Ambient Systems" (TrAmS) (Cliff was PI - funding from EPSRC) and is now CI on TrAmS-2. He also coordinated the three work packages on methodology in the DEPLOY project; was PI on an EPSRC-funded AI4FM project; is currently PI on Taming Concurrency; and is "Partner Investigator" on the Australian funded project "Understanding concurrent programs using rely-guarantee thinking" (ARC grant DP130102901).

As well as his academic career, Cliff has spent over twenty years in industry (which might explain why "applicability" is an issue in most of his research). His fifteen years in IBM saw, among other things, the creation -with colleagues in the Vienna Lab- of VDM which is one of the better known "formal methods". Under Tony Hoare, Cliff wrote his Oxford doctoral thesis in two years (and enjoyed the family atmosphere of Wolfson College). From Oxford, he moved directly to a chair at Manchester University where he built a world-class Formal Methods group which -among other projects- was the academic lead in the largest Software Engineering project funded by the Alvey programme (IPSE 2.5 created the "mural" (Formal Method) Support Systems theorem proving assistant).

During his time at Manchester, Cliff had a 5-year Senior Fellowship from the research council and later spent a sabbatical at Cambridge for the whole of the Newton Institute event on "Semantics" (and there appreciated the hospitality of a Visiting Fellowship at Gonville & Caius College. Much of his research at this time focused on formal (compositional) development methods for concurrent systems.

In 1996 he moved to Harlequin, directing some fifty developers on Information Management projects and finally became overall Technical Director before leaving to re-join academia in 1999.

Cliff is a Fellow of the Royal Academy of Engineering (FREng), ACM, BCS, and IET.

He has been a member of IFIP Working Group 2.3 (Programming Methodology) since 1973 (and was Chair from 1987-96).

Prof. Rupak Majumdar

Formal Methods for Building a Multi-Robot Task Server

Abstract:

In this talk, I will talk about synthesis challenges that arose in our attempts to build Antlab, an end-to-end system that takes streams of user task requests and executes them using collections of robots. In Antlab, each request is specified declaratively in linear temporal logic extended with quantifiers over robots. The user does not program robots individually, nor know how many robots are available at any time or the precise state of the robots. The Antlab runtime system manages the set of robots, schedules robots to perform tasks, automatically synthesizes robot motion plans from the task specification, and manages the coordinated execution of the plan.

We are using Antlab as an end-to-end application of formal methods in cyber-physical systems. I will describe techniques to bridge the gap between continuous and discrete worlds, and hierarchical synthesis tools based on repeated re-planning and dynamic conflict resolution. On the theoretical side, I will describe compositional synthesis for continuous systems and some new classes of synthesis problems. On the practical side, I will describe ongoing work in using natural language for declarative specifications of tasks.

This talk represents joint work with Brendon Boldt, Eva Darulova, Rayna Dimitrova, Ivan Gavran, Kaushik Mallik, Vinayak Prabhu, Indranil Saha, Anne-Kathrin Schmuck, Sadegh Soudjani, and Damien Zufferey.

Biography:

Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT, Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, "Most Influential Paper" awards from PLDI and POPL, and several best paper awards (including from SIGBED, EAPLS, and SIGDA). He received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur and the Ph.D. degree in Computer Science from the University of California at Berkeley.

Prof. Sanjit Seshia

Towards Verified Artificial Intelligence

Abstract:

The deployment of artificial intelligence (AI), particularly of systems that learn from data and experience, is rapidly expanding in our society. Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements. In this talk, I will consider Verified AI from a formal methods perspective. I will describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges. I will illustrate these challenges and principles with examples and sample results, particularly from the domain of autonomous vehicles.

Biography:

Sanjit A. Seshia is a 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, cyber-physical 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), 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.

Prof. Jean-Pierre Talpin

Compositional Methods for CPS Design

Abstract:

Logic and proof theory are probably have proved to be the most effective mathematical tools to help modularly engineering correct software, and this since the introduction of type inference, upto fantastic progresses of SAT-SMT solvers and provers.

In this talk, I will focus on past experience of my former project-team ESPRESSO in manipulating such tools in the design, implementation, proof and test-case of Polychrony: an open-source synchronous modeling environment hosted on the Polarsys industry working group of the Eclipse foundation.

I will highlight the compositionality and scalability of its concepts by considering two major case studies (with Polychrony and its commercial implementation, RT-Builder) in developing functional and real-time simulators, in avionics and automotive, and the integration of these concepts in the AADL standard.

Before concluding, I will hint on broader perspectives undertaken by my new project-team, TEA, toward logic-focused, compositional and scalable, models of concurrent, timed, cyber and physical systems, and the challenges to build new ADLs from such concepts.

Biography:

Jean-Pierre Talpin has a Master in Theoretical Computer Science from University Paris VI. He did his PhD Thesis at Ecole des Mines de Paris under the advisory of Pierre Jouvelot. He worked three years at the European Computer-Industry Research Centre in Munich. He joined INRIA in 1995, in the EPART project-team of Paul Le Guernic. He led INRIA project-team ESPRESSO from 2000 to 2012. I lead INRIA project-team TEA since 2015.

He is recipient of both the 2004 ACM SIGPLAN Award for the most influential POPL paper, with Mads Tofte, and of the 2012 ACM-IEEE LICS "Test of Time" Award, with Pierre Jouvelot. He also received the 2014 ITEA Award of Excellence for his contribution as work-package leader in the ITEA2 project OPEES (2010-2012) which, led by Gael Blondel, started the Polarsys Industry Working Group of the Eclipse foundation.