We are currently undergoing an unprecedented integration of previously disconnected computer system components, resulting in systems that are distributed, heterogeneous, highly dynamic, and often safety-critical. Our goal is to master this complexity while at the same time increase the productivity of users and the robustness of infrastructure.
Research in programming languages and formal methods at EPFL develops languages, theory, algorithms, and tools to support the construction and validation of software systems for all computational devices – from embedded systems and smart phones to data centers and distributed systems. We introduce declarative and domain-specific approaches that increase development productivity and, at the same time, develop practical solutions that benefit existing infrastructure. Our research develops mechanisms and tools for reliable software in the form of type systems, model checking, correctness by construction, constraint solving, theorem proving, analysis, synthesis, query processing, transactions, and actors.