This year, SEFM is happy to feature the following two high-class keynote speakers.
Satisfiability Checking: Theory and Applications
Erika Ábrahám, RWTH Aachen University, Germany
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. For propositional logic, in the late ’90s impressive progress was made towards practically applicable solutions, resulting in powerful SAT solvers. Driven by this success, a new line of research started to enrich propositional SAT solving with solver modules for different theories. Nowadays, sophisticated SAT-modulo-theories (SMT) solvers are available for, e.g., equality logic with uninterpreted functions, bit-vector arithmetic, array theory, floating point arithmetic, and real and integer arithmetic. SAT and SMT solvers are now at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas.
In this talk we give an introduction to the theoretical foundations of satisfiability checking and discuss the efficient embedding of SAT and SMT solvers in different software technologies.
Biography:
Erika Ábrahám graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Currently she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.
Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems
Gul Agha, University of Illinois at Urbana-Champaign, USA
The growth of mobile and cloud computing, cyberphysical systems and the internet of things has arguably made scalable concurrency the dominant form of computing. I will describe the state of the art in models of concurrency, programming abstractions and analysis tools. I will then summarize how actor languages and frameworks have been widely adopted to address scalability, and how new tools that combine static and dyamic analysis are making software safer. However, as we scale up cyberphysical applications and build the internet of things, a key limitation of current languages and tools becomes apparent: the difficulty of representing quantitative and probabilistic properties and reasoning about them. While considerable research has been done in this area, many open problems remain. I will conclude by prioritizing problems that need to be addressed before we can build more complex scalable concurrent applications.
Biography:
Gul Agha is Professor of Computer Science at the University of Illinois at Urbana-Champaign. Agha is a Fellow of the IEEE and a recipient of the IEEE Computer Society Meritorious Service Award. He served as Editor-in-Chief of IEEE Concurrency: Parallel, Distributed and Mobile Computing (1994-98), and of ACM Computing Surveys (2000-2007). While Agha is best known for his work on the formalization of the Actor Model and the development of actor languages, he has also led his research group in pioneering research on statistical model checking, concolic testing, computational learning for verification, and in developing a computational model for energy complexity of parallel algorithms. Agha is the co-director of the interdisciplinary Illinois Structural Health Monitoring Project which has developed sensor networks to monitor civil infrastructure, and a co-founder of Embedor Technologies which is using actor inspired distributed computing to enable continuous monitoring of bridges for improved maintenance and anomaly detection.