- Keynote Speakers
- Accepted Papers
- Call for Papers (PDF)
- Conference Topics
- General Information
- Poster Instructions
- Satellite Workshops
- Previous PSI Editions
Professor of Carnegie Mellon University, Pittsburgh, USA.
Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia in 1967, a M.A. degree in mathematics from Duke University in 1968, and a Ph.D. degree in computer science from Cornell in 1976. He taught at Duke University from 1976-1978 and at Harvard University from 1978-1982. Since 1982 he has been on the faculty in the Computer Science Department at Carnegie-Mellon University. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008.
Dr. Clarke's interests include software and hardware verification and automatic theorem proving. In 1981 he and a graduate student, Allen Emerson, first proposed the use of Model Checking as a verification technique for finite state concurrent systems. His research group pioneered the use of Model Checking for hardware and software verification. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of CounterExample-Guided-Abstraction-Refinement (CEGAR). In addition, Clarke and his students developed the first parallel general resolution theorem prover (Parthenon), and the first theorem prover to be based on a symbolic computation system (Analytica).
Dr. Clarke is co-founder of the conference on Computer Aided Verification (CAV) and served on its steering committee for many years. He is the former editor-in-chief of Formal Methods in Systems Design. He served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. In 1995 he received a Technical Excellence Award from the Semiconductor Research Corporation. He was a co-recipient of the ACM Kanellakis Award in 1998. In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department.
In 2004 Dr. Clarke received the IEEE Harry H. Goode Memorial Award. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was a co-recipient of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award. In 2011 he was elected to the American Academy of Arts and Sciences. He received an Honorary Doctorate from the Vienna University of Technology in 2012. The Chinese Academy of Sciences awarded him an Einstein Professorship in 2013. He received the Franklin Institute 2014 Bower Award and Prize for Achievement in Science for his leading role in the conception and development of techniques for verification of computer systems. Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.
Emeritus Professor of Computing, Oxford University Computing Laboratory Senior Researcher with Microsoft Research in Cambridge.
Tony Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.
On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including Jill, his wife-to-be) in the design and delivery of the first commercial compiler for the programming language Algol 60.
In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model.
Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.
Bertrand Meyer is Professor of Software Engineering at ETH Zurich, the Swiss Federal Institute of Technology, research professor at ITMO (State University of Saint Petersburg) and Chief Architect of Eiffel Software (based in California).
He is the initial designer of the Eiffel method and language and has continued to participate in its evolution. He also directed the development of the EiffelStudio environment, compiler, tools and libraries through their successive versions.
His latest book, Touch of Class: Learning to Program Well, Using Object Technology and Contracts, is based on several years of teaching introductory programming at ETH and was published in 2009 by Springer Verlag.
Earlier books include Object-Oriented Software Construction (a general presentation of object technology, winner of the Jolt Award); Eiffel: The Language (description of the Eiffel language); Object Success (a discussion of object technology for managers); Reusable Software (a discussion of reuse issues and solutions); and Introduction to the Theory of Programming Languages. He has also authored numerous articles and edited or co-edited several dozen conference proceedings, including the 2005 "Verified Software".
Other activities include: chair of the TOOLS conference series (running since 1989, hosted at ETH since 2007); director of the LASER summer school on software engineering (taking place every year since 2004 in early September on Elba Island, Italy); member and chair, since 2009, of the IFIP TC2 committee (Software Technology); member of the IFIP Working Group 2.3 on Programming Methodology; member of the French Academy of Technologies. He is also active as a consultant (object-oriented system design, architectural reviews, technology assessment, patents and software litigation), trainer in object technology and other software topics, and conference speaker. Awards include ACM Software System Award, Fellow of the ACM, Dahl-Nygaard Prize, Harlan D. Mills Prize, and honorary doctorate from the Technical University (ITMO) of Saint Petersburg. Since 2011 he has been an adjunct research professor at ITMO, as holder of a newly created chair on Software Engineering and Verification.
At ETH Zurich and ITMO he pursues research on the construction of high-quality software.
Professor Vladimiro Sassone studied in the University of Pisa, and after appointments in industry, and in academia in Denmark, Italy, London and Sussex, is now Professor in ECS and Director of the CyberSecurity Centre at Southampton. His interests have led to a career in the foundations of computing, with a particular focus on seamless computing, or what is becoming known as ubiquitous global computing across places and devices. Issues of trust and privacy are paramount in such a context, providing a critical link in the Centre to represent the interplay between man and machine.
Vladimiro holds several notable roles, including the roles of Editor in Chief of Springer's ARCOSS (Advanced Research in Computing and Software Science) series and of ACM's Selected Readings, president of the European association ETAPS eV for Theory and Practice of Software, and a member of the Council of the European Association for Theoretical Computer Science. He is an elected member of the Academia Europaea, of the UKCRC, and a Fellow of the British Computer Society. As Director of the Centre of Excellence at Southampton, he brings together a diverse set of colleagues dedicated to pushing boundaries in research and education in CyberSecurity.
In addition to this, Vladimiro is Editor of Logical Methods in Computer Science, of Theoretical Computer Science, of Electronic Proceedings in Theoretical Computer Science and Associated Editor of The Computer Journal. Also, he is Member of the London Mathematical Society's Computer Science Committee, of the EATCS Council, of Presburger Award Committee, of IFIP Technical Committee 1 (UK representative), of IFIP Working Group 1.3 and of EPSRC College.
Vladimiro’s current research activity concerns the foundations of mobile, distributed systems, and aims at underpinning the development of robust, high-level paradigms for global ubiquitous computing. His interests include semantics, type theory, logics, formal methods and, in general, the foundations of computer science, with main focus on languages and models for concurrency. Among his favourite early themes therein has been the study of abstract models for concurrency, their categorical formalisation, properties, and mutual relationships. His present research activity spans over trust, anonymity, security, access control, typing, coordination and behavioural equivalences for (mobile) processes.
Vadim E. Kotov
Corresponding Member of the Russian Academy of Sciences, Silicon Valley, California, USA.
Dr. Vadim Kotov retired from Carnegie-Mellon University, Silicon Valley Campus, USA, where he was Director of Engineering in the NASA-sponsored High Dependability Computing Program.
He holds a Ph.D. in Computer Science from the Russian Academy of Sciences, and M.S. in Electrical Engineering from the National Research University of Nuclear Physics ("MIFI"), in Moscow, Russia.
From 1963 to 1991, Vadim Kotov worked in the Siberian Division of the Russian Academy of Science (Institute of Mathematics, Computing Center, Institute of Informatics Systems). His main research interests were in parallel programming, theory of concurrency, and architecture of multiprocessor and distributed systems. He researched the complexity of automatic parallelization of sequential programs and developed a compositional approach to the specification of concurrency, used as a semantic basis for the control structures in parallel programming languages. He also taught courses in Computer Architecture, Parallel Programming, and Theoretical Computer Science at Novosibirsk University. Vadim Kotov was the first director of the Institute of Informatics Systems of the Russian Academy of Sciences and the head of the Russian Fifth Generation Computing Consortium, START. The consortium combined efforts of several leading academic and industrial (computers, electronics, space, and avionics) organizations with the goal of designing high-performance, scalable, and highly programmable computer systems.
In 1991-2002, he initiated and led several research projects at Hewlett-Packard Laboratories in Silicon Valley, USA, in the area of the large-scale IT systems design: MADE (Modeling, Analysis and Design Environment for concurrent and distributed systems); Systems of Systems (architecture for global enterprise systems); System Factory (a system integration environment); Self-Organizing Services (management of globally distributed service-oriented systems). Those researches were done in cooperation with large corporations, such as FedEx, Boeing, and other Hewlett-Packard customers, in order to help them optimize their enterprise IT infrastructures.
In 2002-2008, Vadim Kotov was Director of Engineering in NASA-funded High Dependability Computing Program, a multi-disciplinary, multi-institutional (Carnegie-Mellon University, MIT, University of South California, Washington University) effort to improve NASA’s capability to create dependable mission-critical ground and flight software for future Mars rovers, Integrated System Health Management for the International Space Station, air-traffic management, and the Deep Space observation network.
Dr. Kotov was a member of the editorial boards of Theoretical Computer Science, Information Processing Letters, Parallel Programming, and Parallel and Distributed Computing Practices. He is the holder of the IFIP Silver Core Award in appreciation of his contributions to computer science. He delivered invited talks at several international conferences including the World Computer Congresses. Vadim Kotov is a Corresponding Member of the Russian Academy of Sciences.