RiSE/SHiNE Winter School 2018
News
- February 7, 2018: updated course material.
- February 6, 2018: updated course material.
- February 5, 2018: added information on social dinner.
- January 22, 2018: updated speaker information.
- January 8, 2018: added registration information.
- January 3, 2018: webpage goes online.
Overview
The RiSE/SHiNE Winter School 2018 is an event of the Austrian national research network RiSE.
The target audience are researchers, advanced master students, PhD students, or Post-Docs working on theoretical and practical aspects of logic in computer science, formal verification, and automated reasoning in a broad sense.
Date and Venue
- Duration: the RiSE/SHiNE Winter School 2018 will take place from Monday, February 5 to Friday, February 9, 2018 at TU Wien, Austria.
- Venue: All talks will be held in lecture room EI 10 Fritz Paschke HS, Gusshausstr. 25-29 (ground floow), 1040 Wien (view on Google Maps).
Registration
Please send an email to Florian Lonsing with your name and the name of your advisor (if you have one). Please indicate whether you will join the visit to the "Heurige" (social dinner on Wednesday, February 7).
COST: 150 Euro
Please transfer the money indicating the code "KTG192030A18" until January 31 2018 to the following account:
| UniCredit Bank Austria | |
| 1010 Wien, Schottengasse 6 - 8 | |
| Account name: | TU Wien |
| BIC (SWIFT): | BKAUATWW |
| IBAN: | AT72 1200 0514 2900 0401 |
IMPORTANT: Do not forget to indicate the code "KTG192030A18" and the participant name in the description.
Speakers
Federico Aschieri, TU Wien, Austria.
- Lecture Title: Curry-Howard Correspondence
- Abstract:
The Curry-Howard correspondence is a profound connection between the world of logical proofs and the world of computer programs. It says that logical formulas can be used as types for specifying program behaviour, while proofs can be used to prove correctness of the programs with respect to the specification. In this lecture, we shall learn how to use logical formulas as types for various programming languages: purely functional, functional with control operators and functional with constructs for concurrent computation.
- Biographical Sketch:
Federico Aschieri received a PhD in computer science from the University of Torino and Queen Mary, University of London in 2011. He was postdoctoral researcher at INRIA Paris in 2011/2012 and at the ENS Lyon in 2012/2014. He is postdoctoral researcher at the TU Wien since 2014. His principal research interest is the interplay between logic and computation.
Dirk Beyer, LMU Munich, Germany.
- Lecture Title: Configurable Software Model Checking --- A Unifying View
- Abstract:
The goal of this lecture is to bridge the gap between verification research and software engineering. Consequently, the lecture starts with theory and concepts, continues with a unifying view on several different verification algorithms, and finally addresses some practical problems that occur in software verification. The first part gives an introduction of the framework of configurable program analysis and shows how state-or-the-art concepts like cartesian and boolean abstraction, lazy abstraction, CEGAR, interpolation, and large-block encoding can be integrated in a configurable way. The second part consolidates knowledge and we show how to express the four different "schools of thought" of software verification in one unifying framework: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. The third part focuses on practical aspects of software model checking and explains approaches like regression verification, witness-based result validation, conditional model checking, and reducer-based verification.
- Biographical Sketch:
Dirk Beyer is Full Professor of Computer Science and has a Research Chair for Software and Computational Systems at LMU Munich, Germany (since 2016). Before, he was Full Professor of Computer Science at University of Passau, Germany (2009-2016). He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada (2006-2009), and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004) in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is the architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.
Olaf Beyersdorff, University of Leeds, UK.
- Lecture Title: Proof Complexity
- Abstract:
The aim of this lecture is to present an up-to-date introduction to propositional proof complexity. We will start with a gentle introduction to the complexity of theorem proving and its relations to central questions in computational complexity. The lecture will cover important proof systems, current knowledge about proof lengths in these systems, and implications for the performance of satisfiability algorithms. We will also provide an overview of proof complexity results for non-classical logics as modal, intuitionistic and quantified boolean formulas and their relations to QBF solving.
- Biographical Sketch:
Olaf Beyersdorff is Professor of Computational Logic at the School of Computing of the University of Leeds. Before coming to Leeds in 2012, he was a visiting professor at Sapienza University Rome and held positions at Leibniz University Hanover and Humboldt University Berlin, where he obtained his PhD in 2006. His main research interests are in logic and complexity and specifically proof complexity.
Laura Kovacs, TU Wien, Austria, and Andrei Voronkov, University of Manchester, UK.
- Lecture Title: First-Order Theorem Proving in Rigorous Systems Engineering
- Abstract:
First-order theorem proving is one of the earliest research areas within artificial intelligence and formal methods. It is undergoing a rapid development thanks to its successful use in program analysis and verification, semantic Web, database systems, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists. This tutorial aims to address this by introducing the audience to first-order theorem proving with a focus on applications in rigorous systems engineering. The workhorse used for a demonstration of concepts discussed at the tutorial will be our award-winning theorem prover Vampire.
The tutorial will be split in two parts. The first part immediately helps the audience place the work in context by introducing them to an application of theorem proving in Vampire for program analysis. The second part details the underlying theory with a focus on recent developments in program analysis, interpolation and theory reasoning. particular relevance to the rest of the tutorial. Both part are accompanied by live demonstrations and hands-on exercises with Vampire.
- Biographical Sketch Laura Kovacs:
Laura Kovacs is a professor in computer science at the Vienna University of Technology, Austria. She has also an adjunct professor position at the Chalmers University of Technology, Sweden. Her research aims at the design of new methods, tools and algorithms supporting program analysis, by combining techniques from automated reasoning and symbolic computation techniques. She has been awarded an ERC Starting Grant 2014 and a Swedish Wallenberg Academy Fellowship 2014.
- Biographical Sketch Andrei Voronkov:
Andrei Voronkov is a professor of computer science at the University of Manchester, UK and a visiting professor at the Vienna University of Technology, Austria. He is the founder and CEO of EasyChair, the main designer of the theorem prover Vampire, and the founder of the LPAR conference series. His research focuses on automated theorem proving and EasyChair-inspired areas, such as automatic code analysis and (secure) code generation, scientific document analysis, keyphrase extraction from scientific documents and constraint satisfaction problems related to conference management. He received a Herbrand Award in 2015 for his numerous theoretical and practical contributions to automated deduction.
Program
- The program starts on Monday, February 5, at 14:00 and ends on Friday, February 9, at 12:30.
- Abbreviations used in table below:
- LK/AV: Laura Kovacs and Andrei Voronkov.
- OB: Olaf Beyersdorff.
- FA: Federico Aschieri.
- DB: Dirk Beyer.
| Monday | Tuesday | Wednesday | Thursday | Friday | |
| 09:00-10:30 | arrival | LK/AV | OB | FA | DB |
| 10:30-11:00 | coffee | coffee | coffee | coffee | |
| 11:00-12:30 | LK/AV | OB | FA | DB | |
| 12:30-14:00 | lunch | lunch | lunch | departure | |
| 14:00-15:30 | LK/AV | OB | FA | DB | |
| 15:30-16:00 | coffee | coffee | coffee | coffee | |
| 16:00-17:30 | LK/AV | OB | FA | DB | |
| social dinner |
Material
- First-Order Theorem Proving (Laura Kovacs and Andrei Voronkov): slides
- Proof Complexity (Olaf Beyersdorff): slides
- Curry-Howard Correspondence (Federico Aschieri): slides
Lunches and Social Dinner
The winter school does not offer organized lunches. There are plenty of restaurants and kiosks within walking distance of the venue.
The social dinner takes place on Wednesday, February 7, at 7pm at Heuriger Mayer am Pfarrplatz, Pfarrplatz 2, 1190 Wien (directions).
Travel
TU Wien is easily accessible by public transport.
- Vienna International Airport.
- Vienna public transport travel planning.
- Austrian Railways travel planning.
Accommodation
Organizers
The RiSE/SHiNE Winter School 2018 is organized by Uwe Egly and Florian Lonsing, Knowledge-Based Systems Group, Institute of Information Systems, TU Wien, Austria.
This website is maintained by Florian Lonsing.