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.
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.