A Logical Revolution

Wednesday, August 21
09:30-10:30, Column Hall

Mathematical logic was developed in an effort to provide formal foundations for mathematics. In this quest, which ultimately failed, logic begat computer science, yielding both computers and theoretical computer science. But then logic turned out to be a disappointment as foundations for computer science, as almost all decision problems in logic are either undecidable or intractable. Starting from the mid 1970s, however, there has been a quiet revolution in logic in computer science, and problems that are theoretically undecidable or intractable were shown to be quite feasible in practice. This talk describes the rise, fall, and rise of logic in computer science, describing several modern applications of logic to computing, include databases, hardware design, and software engineering.

About the Speaker. Moshe Y. Vardi is Karen Ostrum George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology. His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum.

Producing software by integration: Challenges and research directions

Thursday, August 22
09:30-10:30, Column Hall

Software is increasingly produced according to a certain goal and by integrating existing software produced by third-parties, typically black-box, and often provided without a machine readable documentation. This implies that development processes in the next future have to explicitly deal with an inherent incompleteness of information about existing software, notably on its behavior. Therefore, on one side a software producer will less and less know the precise behavior of a third party software service, on the other side she will need to use it to build her own application. In this talk we describe an innovative development process to automatically produce dependable software systems by integrating existing services under uncertainty and according to the specified goal. Moreover, we (i) discuss important challenges that must be faced while producing the kind of systems we are targeting, (ii) give an overview of the state of art related to the identified challenges, and finally (iii) provide research directions to address those challenges.

About the Speaker. Paola Inverardi is Professor in Computer Science at University of L’Aquila where she leads the Software Engineering and Architecture Research Group. Paola Inverardi's main research area is in the application of rigorous methods to software production in order to improve software quality. In the last decade her research interests concentrated in the field of software architectures, mobile applications and adaptive systems. Inverardi serves in the editorial boards of the IEEE Transaction of Software Engineering, Springer Computing and Elsevier Computer Science Review. She has been general chair or program chair of leading conferences in software technology (i.e. ASE08, ICSE09, ESEC/FSE03). She is Chair of the ICSE Steering Committee, member of the ACM Europe Council and member of Academia Europaea. She has received a Honorary Doctorate at Mälardalen University Sweden. Paola Inverardi received the 2013 IEEE TCSE Distinguished Service Award for outstanding and sustained contributions to software engineering community http://www.cs-tcse.org/awards.

Software engineering for mathematics

Friday, August 23
09:30-10:30, Column Hall

Since Turing, we have wanted to use computers to store, process, and check mathematics. However even with the assistance of modern software tools, the formalization of research-level mathematics remains a daunting task, not least because of the talent with which working mathematicians combine diverse theories to achieve their ends. By drawing on tools and techniques from type theory, language design, and software engineering we captured enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory, which ultimately lead to the monumental Classification of finite simple groups. This involved recasting the software component concept in the setting of higher-order, higher-kinded Type Theory to create a library of mathematical components covering most of the undergraduate Algebra and graduate Group Theory syllabus. This library then allowed us to write a formal proof comparable in size and abstraction level to the 250-page textbook proof of the Odd Order theorem.

About the Speaker. Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge, which he joined in 2003, after 13 year in France at Inria. Dr. Gonthier has worked on the Esterel reactive programming language, optimal computation of functional programs, formal verification of concurrent memory management, the join calculus model of concurrency and security, concurrency analysis of the Ariane 5 flight software, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, which recently completed the formalization of the Odd Order theorem, the landmark result that ultimately lead to the Classification of Finite Simple Groups. Dr. Gonthier was awarded the EADS Grand Prize in Computer Science in 2011.