Differences

This shows you the differences between two versions of the page.

--- svtp17 [2017/02/21 10:01]
vkuncak
+++ svtp17 [2017/03/08 09:16]
vkuncak
@@ Line 17: / Line 17: @@
 An SMT solver takes first-order formulas as input and provides impressive automation.  But what if the problem at hand goes beyond first order?  The Dafny program verifier provides well-founded functions, inductive proofs, and predicates defined as least and greatest fixpoints.  It encodes properties of these into first-order logic in such a way that harnesses the automation of SMT solvers.  In this talk, I will give an overview of functions and induction in Dafny, and will then focus on the encoding on predicates defined by fixpoints.
+**Bio:** Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.  He is an ACM Fellow.
+Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he likes to cook and, being a multi-instrumentalist, play music. Leino instructed group cardio and strength classes for many years, he more recently danced on a salsa performance team, and he once needed a helicopter to get off a Swiss mountain.
 ==== 10:30. Coffee ====
@@ Line 37: / Line 40: @@
 adversaries can be used to improve existing techniques such as partial
 order reduction.
+**Bio:** Sergio holds an MSc and a PhD in Computer Science, both obtained at National Universities in Argentina, with a strong focus on formal methods, logic and compilers. After serving as a Research Assistant in Oxford University in the area quantitative analysis of distributed systems, he joined Google for 4 years, working on distributed data processing and analysis applied to a variety of problems including demand forecast, fraud detection and development of Java security libraries for Android.
 ==== 12:00. Lunch ====
@@ Line 47: / Line 52: @@
 enumerating and counting solutions. We will cover some of the newer features in Z3 that expose constraint services.
 For applications in product configuration, Z3 includes specialized solvers for finding backbones under assumptions, for solving quantified formulas Z3 contains elements of partial quantifier elimination methods based on models, and for solving optimization modulo SMT, Z3 contains dedicated MaxSMT.
+**Bio:**
+Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work with Leonardo de Moura  and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014. Previously, he developed the DFSR, Distributed File System - Replication, and Remote Differential Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first few years of university at DTU and DIKU.
 ==== 15:00. Coffee ====
@@ Line 69: / Line 77: @@
 Florian Zuleger.
+**Bio:**
+Philipp Ruemmer is an assistant professor at Uppsala University, Sweden. He received his doctorate in Computer Science from Chalmers University and Gothenburg University in 2008. Before joining Uppsala University as an assistant professor, he has been research assistant at the Oxford University Computing Laboratory. His research interests include various directions in program verification, theorem proving and SMT reasoning, and application of such methods in the area of embedded systems. Philipp received the Oscar Prize of Uppsala University in 2013, for contributions to the field of program correctness, and the IJCAR best paper award in 2014; the theorem prover Princess resulting from his research won the TFA division of the theorem proving competition CASC in 2012.
 ==== 16:30. Bruno Marnette: On the Real Expressive Power of Datalog Extensions ====
@@ Line 74: / Line 84: @@
 Numerous extensions of the Datalog language have been introduced to address the lack of expressive power of traditional Datalog. In particular, equality constraints and value invention have proven convenient in the context Data Exchange and DL-like reasoning. Adding such constraints to the Datalog language however leads to intractability, and a great amount of work has aimed at identifying tractable islands, typically relying on syntactic properties (such as acyclicity or guardedness). In this talk we'll investigate whether the theoretic expressive power of these tractable extensions truly differ from standard Datalog. (Spoiler alert: they don't).
+**Bio:** Dr. Bruno Marnette is the CEO of Prodo and CTO of Enki. Previously, he worked at Palantir and was a post-doctoral researcher at ENS/INRIA. Bruno holds PhD from Oxford University.
+----
+{{::restaurantslausanne.pdf|List of Selected Restaurants}}
+----