Automated Specification and Verification of Web Systems
11th International Workshop
June 23rd, Oslo, Norway
affiliated with FM 2015
|
|
Automated Specification and Verification of Web Systems11th International Workshop June 23rd, Oslo, Norwayaffiliated with FM 2015 |
|
Abstract:
Many web and cloud computing systems are real-time, safety-critical systems with strong qualitative and quantitative formal requirements. They often need to be reflective and adaptive, and may be probabilistic in their algorithms and/or their operating environments. All this makes these systems quite complex and therefore hard to design, build and verify. To drastically reduce such system complexity I propose the use of formal patterns, that is, formally specified solutions to frequently occurring distributed system problems, in particular those used in web and cloud computing, that are generic, executable, and come with strong formal guarantees. I will explain the semantics of such patterns as theory transformations in rewriting logic; and will give a representative collection of useful patterns to ground all the key concepts and show their effectiveness.
Biography:
José Meseguer is Professor of Computer Science at UIUC and leads the Formal Methods and Declarative Languages Laboratory. He obtained his Ph.D. in Mathematics at the University of Zaragoza, Spain, in 1975. After post-doctoral stays at the University of Santiago de Compostela, and at the University of California at Berkeley, he joined in 1980 the Computer Science Laboratory at SRI International in Menlo Park, California, where he became a Principal Scientist and Head of the Logic and Declarative Languages Group. He joined the University of Illinois at Urbana-Champaign in 2001. He has worked on the design and implementation of several declarative languages, including the OBJ and Maude languages, on formal specification and verification techniques, on concurrency theory, on formal approaches to object-oriented specification, on parallel software and architectures for declarative languages, and on the logical foundations of computer science using equational logic, rewriting logic, and the theory of general logics.
Abstract:
For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error-free software. Available tools are often lacking in helping programmers develop more reliable and secure applications. Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging. In this talk we describe our experience in integrating a verification tool based on static analysis into the software development cycle at Facebook.
Biography:
Dino Distefano is Professor of Software Verification and Royal Academy of Engineering Research Fellow in the School of Electronic Engineering and Computer Science at Queen Mary, University of London. He was a member of the East London Massive. He was also a founder of Monoidics Ltd, a technology startup specialised in automatic verification tools. Monoidics was acquired by Facebook in July 2013. Dino received his Ph.D. from the University of Twente, in The Netherlands.