Revisit your favourite VSL moments.

VSL keynote recordings now online

Missed one of the VSL keynote talks by Dana Scott, Christos Papadimitriou, Alex Wilkie, Franz Baader and Edmund Clarke? Never mind, you can now (re)watch all the keynote talks online:

Dana Scott · Christos Papadimitriou · Alex Wilkie · Franz Baader · Edmund M. Clarke

Dana Scott: VSL Opening
Christos Papadimitriou: Computational Ideas and the Theory of Evolution – Abstract

Alex Wilkie: The theory and applications of o-minimal structures – Abstract

Franz Baader: Ontology-Based Monitoring of Dynamic Systems – Abstract

Edmund M. Clarke: Verification of Computer Systems with Model Checking – Abstract

KR 2014 Best Paper Awards

The best contributions to the 14th International Conference on Principles of Knowledge Representation and Reasoning are awarded prizes in two categories.

The 2014 Ray Reiter Best Paper Prize

The best paper of the conference receives the 2014 Ray Reiter Best Paper Prize sponsored by the Artificial Intelligence Journal which goes to:

Leonid Libkin

for his paper entitled

Certain Answers as Objects and Knowledge

(presented today at 2:30pm in EI7)

The 2014 Marco Cadoli Student Paper Prize

The best paper of the conference whose main author is a student receives the 2014 Marco Cadoli Student Paper Prize. It is sponsored by KR Inc. and goes to:

Elena Botoeva, Roman Kontchakov, Vladislav Ryzhikov, Frank Wolter and Michael Zakharyaschev

for their paper on

Query Inseparability for Description Logic Knowledge Bases

The award ceremony will take place today (Wed July 22nd) following the

Great Moments in KR invited talk by
Sheila McIlraith entitled “Situation Calculus: The last 15 years”

at 6:30pm in EI7.

More information on:

[Photos] LogicLounge: Gottlob, Zach, Bloem, Cook

Meeting place for friends of logic at Heuer Coffee Bar Garden Restaurant during Vienna Summer of Logic 2014 • Insights in exactly one hour live and in public • Tribute to antique philosophical symposium

Treffpunkt für FreundInnen der Logik im “Heuer am Karlsplatz” während des Vienna Summer of Logic 2014 • Erläuterungen in exakt einer Stunde live und vor Publikum • Reverenz an antikes philosophisches Symposium

There are two more dates of LogicLounge coming up:

  • July 22: Drones with a guilty conscience: the ethics of Artificial Intelligence
    Moshe Vardi (Rice U) – Herbert Hrachovec (U Wien)
  • July 23: Female logics
    Magdalena Ortiz (TU Wien), Ruzica Piskac (Yale U) – Tanja Traxler (Der Standard)

Photos © VSL 2014 / Photography: Nadja Meister

VCLA International Student Awards

VCLAThe Vienna Center for Logic and Algorithms announces the first edition of the

VCLA International Student Awards

and calls for the nomination of authors of outstanding scientific works in the field of Logic and Computer Science, in the following two categories:

Outstanding Master Thesis Award

Outstanding Undergraduate Research Award

In both categories, the work must make an original contribution to a research field that can be classified as part of Logic in Computer Science, understood broadly as the use of logic as a tool that enables computer programs to reason about the world. The main areas of interest include:

  • Databases and Artificial Intelligence: Answer-Set Programming, Datalog, query languages, novel database-theoretical methods, logic programming, description logics, knowledge representation and reasoning, argumentation, planning, preferential reasoning.
  • Verification, ranging from model checking, program analysis and abstraction to new interdisciplinary areas such as fault localization, program repair, program synthesis, and the analysis of biological systems.
  • Computational Logic, proof theory, cut elimination, proof mining, interpolants, automated deduction, non-classical logics, computational complexity, SAT, QSAT, CSP.

The degree must have been awarded no earlier than November 1st, 2012. Students that obtained the degree at the Vienna University of Technology are excluded from nomination. The committee will select a winner for each category. The winners will be invited to Vienna to present their project and participate in a festive award ceremony. Additionally, the Outstanding Master Thesis Award category is accompanied by a prize of 1,200 Eur, and the Outstanding Undergraduate Research Award by a prize of 800 Eur. The decisions of the committee are not appealable.

More information and nomination instructions:

Important dates:
Nomination deadline: November 15, 2014 (AoE)
Notification of the committee’s decision: Mid January, 2015
Award ceremony: Spring 2015

Award committee

Ezio Bartocci Simone Bova Michael Fink
Robert Ganian Igor Konnov Tomer Kotek
Roman Kutzmets Magdalena Ortiz Revantha Ramanayake
Mantas Simkus Daniel Weller Florian Zuleger

Véronique Cortier
Véronique Cortier

[Photos] FLoC Plenary Talks

FLoC plenary talks by Véronique Cortier (Electronic voting: how logic can help?) and Orna Kupferman (From Reachability to Temporal Specifications in Game Theory)

Photos © VSL 2014 / Photography: Sara Meister

Orna Kupferman Orna Kupferman Véronique Cortier Véronique Cortier

SIGLOG Launch event 15th July

Guest post by Prakash Panangaden

The Association of Computing Machinery has chartered a new special interest group (SIG) focussed on logic and computation. The new group, called SIGLOG, was chartered in April and was announced to the community at an event on the 15th of July at FLoC. There were about 100 people in attendence and the SIGLOG Chair (Prakash Panangaden) gave a brief presentation of the new group, its structure, aims and contributions to the logic and computation community. At the end of June membership stood at 111 and it is hoped that the group will grow to at least 200 by the end of July. The eventual target membership for the group is 500.
Information about SIGLOG can be found at where there is a Chair’s statement and a link to the page to join SIGLOG.

SIGLOG publishes an electronic newsletter for its members quarterly; the first issue was released on 1st July. This newsletter will feature columns on Automata, Complexity, Security, Semantics and Verification. Volunteers are requested to help with the running of SIGLOG and the newsletter. In particular there was interest expressed by some of those present in joining the SIGLOG education committee. There will be another event on the 22nd of July run by Rajeev Alur.

2nd VSL Joint Award Ceremony

The first VSL Joint Award Ceremony last week was a huge success. Join us today at 4.30pm in Main Building, Kuppelsaal for the second Joint Award Ceremony.

VSL Joint Award Ceremony

Kurt Gödel Medal

© Münze Österreich AG

In the Award Ceremony of the FLoC Olympic Games with a laudation by Edmund M. Clarke, the teams of 9 different competitions receive Gödel medals for their contributions to the development of efficient solvers from the wide field of satisfiability solvers to automatic theorem provers and term rewriters, from declarative logic programming solvers and ontology reasoners to automated software verifiers, from programs that check models of hardware designs to solvers that automatically synthesize computer programs, and to provers that test program termination.

Werner “Jimmy” DePauli-Schimanovich is being honored for his contributions to Gödel research, for his efforts towards re-establishing Vienna as a center of logic in the second half of the past century, and for extending the outreach of formal logic and logical thinking to other disciplines.

Zhang Mingyi is awarded a Lifetime Achievement Award by the Kurt Gödel Society for pioneering research in Artificial Intelligence and Knowledge Representation in China especially for mathematical characterizations of various forms of non-monotonic reasoning.

Maria Magdalena Ortiz de la Fuente is receiving the EMCL Distinguished Alumni Award 2014 for her outstanding contributions to the field of Computational Logic.

The award ceremony concludes with the FLoC closing of week 2.

  • FLoC Olympic Games Award Ceremony 2
    • Fifth Answer Set Programming Competition (ASPCOMP 2014)
    • The 7th IJCAR ATP System Competition (CASC-J7)
    • Hardware Model Checking Competition (HWMCC 2014)
    • OWL Reasoner Evaluation (ORE 2014)
    • Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
    • Competition on Software Verification (SV-COMP 2014)
    • Syntax-Guided Synthesis Competition (SyGuS-COMP 2014)
    • Synthesis Competition (SYNTCOMP 2014)
    • Termination Competition (termCOMP 2014)
  • Werner Depauli-Schimanovich – Lifetime Achievement Award
  • Mingyi Zhang – Lifetime Achievement Award
  • European Masters Program In Computational Logic EMCL Distinguished Alumni Award
  • FLoC Closing Week 2

2014 CAV Award
2014 CAV Award

2014 CAV Award

Guest post by Marta Kwiatkowska, Chair of the CAV Award Committee

2014 CAV AwardThe 2014 CAV Award was presented yesterday to Patrice Godefroid, Doron Peled, Antti Valmari, and Pierre Wolper “for the development of partial-order-reduction algorithms for efficient state-space exploration of concurrent systems.”

They developed efficient algorithms to explore the state space on-the-fly that have become the key component of explicit model checkers. Partial-order reduction is one of the major contributions to the field of automated verification in the last two decades. Its development contributed in a crucial way to make model checking successful and practically applicable to concurrent systems.

See press release at:

Herbrand Award

International Conference on Automated Deduction (CADE)
Herbrand Award for Distinguished Contributions to Automated Reasoning
presented to

Robert L. Constable

in recognition of his pioneering research in automated reasoning, such as his seminal contributions to the foundations of computational type theory; the creation of Nuprl, the first constructive type theory based theorem prover; the development of the correct-by-construction programming paradigm; and their applications to verification and synthesis of computer systems, including distributed computing.

Presented at

IJCAR 2014
The 7th International Joint Conference on Automated Reasoning
July 19, 2014

Maria Paola Bonacina
President of CADE Inc.

IJCAR Best Paper Award

The IJCAR 2014 best paper award will be given to

Approximations for Model Construction

Aleksandar Zeljic, Christoph M. Wintersteiger, and Philipp Rummer

The paper presents a new way to integrate approximation techniques into automated reasoning procedures and proves its usefulness for the important case of floating-point arithmetic.

This paper was selected by the IJCAR 2014 Program Committee.
International Joint Conference on Automated Reasoning (IJCAR)

Awards at the Logic Colloquium

Julia F. KnightThe Association for Symbolic Logic presents two of its major awards at this year’s Logic Colloquium at the Vienna Summer of Logic.

The Karp Prize, named for Carol Karp, is awarded every five years for connected body of research, most of which has been completed in the time since the previous prize was awarded. The 2013 Karp Prize is shared between Moti Gitik (Tel Aviv University), Ya’acov Peterzil, (University of Haifa), Jonathan Pila (University of Oxford), Sergei Starchenko (University of Notre Dame), and Alex Wilkie (University of Manchester).

Moti Gitik is being honored for his definitive work on the Singular Cardinals Hypothesis. His earlier work determined the exact consistency strength of the failure of the Singular Cardinals Hypothesis. His deep understanding led to a counterexample to the PCF conjecture, for which he is being awarded his share of the Karp prize. Matt Foreman will discuss Gitik’s work at 3 pm on Saturday.

Kobi Peterzil, Jonathan Pila, Sergei Starchenko, and Alex Wilkie shared the other half of the 2013 Karp Prize for their efforts in turning the theory of o-minimality into a sharp tool for attacking conjectures in number theory, which culminated in the solution of important special cases of the André-Oort Conjecture by Pila. The award lecture was given by Matthias Aschenbrenner on Tuesday, his slides are online.

The Gödel Lecture is an invited address delivered each year, alternating between the ASL Annual Meeting and the Logic Colloquium. The ASL Committee on Prizes and Awards is charged with selecting the Gödel Lecturer based on outstanding contributions to logic through research and scholarship.

The 2014 Gödel Lecturer is Julia F. Knight (Notre Dame University). She is being honored for her work on model theory and recursion theory. Julia Knight has been among the main contributors, if not the main one, to the area of computable structure theory. Her work continues to be extremely influential in the area. She is also well-known for her theorems on the upward closure of degree spectra of non-trivial structures. Her work with Ash and Slaman on generic copies of structures became a standard tool that has been used to solve a whole variety of problems.
Knight will speak at 5:30 pm on Saturday.

The Place of Logic in Computer Science Education Followup

Cross-post from Logblog: Richard Zach’s Logic Blog by Richard Zach

The Special Session on “The Place of Logic in Computer Science Education” took place at the Logic Colloquium on Tuesday. It was well attended and, I think, overall a successful session.  The newly-formed ACM Special Interest Group on Logic and Computation (SIGLOG) was represented by its chair Prakash Panangaden. He stressed the importance of logicians (and computer scientists/instructors relying on logic and logical methods) to push for the integration of logical methods in the CS curriculum — the way the SIG on Programming Languages SIGPLAN has successfully managed to give prominence to programming languages and design. In the US, the existence of a standard curriculum makes it difficult for departments that would even want to put a focus on logic and formal methods to introduce dedicated courses, a point made by Phokion Kolaitis in discussion.  That curriculum includes only propositional logic and just the very basics of predicate logic as a requirement for all CS majors. In a previous panel at a SIGCSE meeting, it was argued that a remedy would be to integrate bits of logic in other courses where logical methods are needed.  This resulted in the TeachLogic Project, led by Moshe Vardi at Rice University, which aimed to provide course materials and ideas for where and how to incorporate logic into CS courses.

In Europe, departments seem to have a lot more leeway.  This makes it possible, e.g., for Austrian CS departments to even offer specialized grad programs in logic and computing, as Alex Leitsch reported.  Nicole Schweikardt presented ideas from an introductory course she teaches in Frankfurt.  One of her didactic lessons was that engaging examples are important to draw in students — pure logic courses tend to do a less-than-optimal job at convincing students that this stuff is useful and important.  Her “provocative statement was: “When confronting computer science students with formal logic for the first time, we should dare to be less formal.” This tied in with another topic of discussion: diversity.  In the US, the gender split in CS is even worse than in philosophy: 12% of 2010-11 CS degrees were awarded to women. Byron Cook also mentioned this as an issue, and pointed to Harvey Mudd College as a success story for how to get and keep members of underrepresented groups in(to) CS.  Now Harvey Mudd is an elite college and in many places that kind of institution-wide initiative is sadly not feasible (as Phokion pointed out).

There are lessons to be learned, not just for how we teach formal methods in CS but also for logic courses in philosophy departments. One may be to make these courses — not: less rigorous — but simply more appealing by focussing more on examples and applications which are familiar and engaging to a broader audience that’s not already familiar with formal methods. In the discussion, Brigitte Pientka pointed out, however, that it would be a mistake to think that we have sacrifice rigor in logic or CS courses to make them appealing to women and enable them to succeed in them.  She referred to the environment at Carnegie Mellon University and the research by Carol Frieze and others who have documented that a more balanced environment allows both men and women to participate, contribute, and be successful, in the CS major, without accommodating presumed gender differences or watering down the curriculum to become “more female friendly”.  Since 2002 the percentage of bachelor‘s degrees granted to women in the CS major at CMU has exceeded and stayed well above the national average. It is currently at 25%.  These and other initiatives are covered in a piece on drawing women to computer science published in the NYT’s TheUpshot blog just yesterday.

SIGLOG is forming an Education Committee, which will carry on the work of the TeachLogic project and hopefully can serve as a clearing house for ideas, materials, and tools.  If you’re interested in being involved, Prakash would like to hear from you!  In addition, this would be a good place to announce that the conference Tools for Teaching Logic is happening again next year!

1st VSL Joint Award Ceremony

Kurt Gödel Medal

© Münze Österreich AG

To us, Vienna is known as a city of logic. But to many visitors, Vienna is better known as a city of music. And so, on Thursday evening the first of two VSL Joint Award Ceremony took place accompanied by the world premiere of Tribute to Kurt Gödel by Michael F.P. Huber and performed by the excellent Adamas String Quartet.

This VSL Joint Award Ceremony brought together the ceremonies of the Kurt Gödel Research Prize Fellowships (organized by the Kurt Gödel Society with support from the John Templeton Foundation) and part one of the 1st FLoC Olympic Games. Winners were awarded one of the prestigious Kurt Gödel medals. Last but not least, Moshe Vardi’s birthday was celebrated with a surprise FLoC-styled birthday cake. Congratulations to everyone!

The second VSL Joint Award Ceremony will take place on Monday July 21, 16:30–19:00 in Main Building, Kuppelsaal.

Kurt Gödel Research Prize Fellowships

FLoC Olympic Games

Vardi Fest

All photos © VSL 2014 / Photography: Nadja Meister

[Photos] 1st FLoC Panel: Publication Models in Computing Research

Thursday morning, the first of two FLoC panels touched a delicate topic: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? moderated by Moshe Vardi brought together five panelists with distinct and sometimes controversial views on the subject. Discussion covered different facets of computer science publishing, such as conference vs. journal publications, the role and importance of open access, or reviewer load in our community.

Panelists: Nina Amla, National Science Foundation. Georg Gottlob, Oxford University, Vienna University of Technology. Falk Reckling, Austrian Science Fund. Sweitze Roffel, Elsevier. Andrei Voronkov, University of Manchester.
Moderator: Moshe Vardi, Rice University

Photos © VSL 2014 / Photography: Sara Meister

First FLoC Panel

First FLoC Panel

[Photos] Keynotes Week 1: Scott, Papadimitriou, Wilkie

The first week of Vienna Summer of Logic featured three keynote talks be extraordinary scientists: Dana Scott addressed the participants in the VSL Opening Talk, Christos Papadimitriou gave a talk on his most recent work concerning the theory of evolution, and Alex Wilkie rocked the blackboards with theory and applications of o-minimal structures.

Photos © VSL 2014 / Photography: Nadja Meister

Dana Scott Christos Papadimitriou Alex Wilkie

RTA-TLCA Best Paper Awards

Guest post for RTA-TLCA

Sylvain Schmitz received the RTA-TLCA Best Paper Award for solving by his paper “Relevance Logic is 2-ExpTime-Complete” a problem open for 25 years. The proof uses reductions to and from coverability in branching vector addition systems.

Łukasz Czajka received the RTA-TLCA Best Student Paper Award for “A Coinductive Confluence Proof for Infinitary Lambda-Calculus”. Łukasz avoids the use of ordinals and metric convergence, making the proof thus better suitable for formalisation in a proof-assistant.

RTA-TLCA Best Paper Award
RTA-TLCA Best Student Paper Award

The awards were handed over during the RTA-TLCA dinner at a Viennese “Heurigen” on July 17.

RTA = Int. Conf. on Rewriting Techniques and Applications
TLCA = Int. Conf. on Typed Lambda Calculi and Applications

Design and production of awards: Barta Pokale,

Ackermann Award Ceremony

Guest post by Anuj Dawar (President of the EACSL)

The Ackermann Award is given by the European Association for Computer Science Logic annually since 2005 to an outstanding doctoral dissertation in the area of Logic in Computer Science. The tenth Ackermann award will be presented on Friday, 18 July, at 17.00 in Hörsaal 1.

The winner of the 2014 Ackermann Award is Michael Elberfeld for his thesis “Space and Circuit Complexity of Monadic Second-Order Definable Problems on Tree-Decomposable Structures”. He will present a lecture on his thesis work at the ceremony.

Moshe Vardi
Moshe Vardi

Welcoming Comments at the VSL Opening Reception

Guest post by Moshe Vardi

Moshe VardiWhen John F. Kennedy became president of the United States, he invited all US Nobel Laureates for a dinner at the White House. At his welcoming remarks he commented that this was the greatest assemblage of intellect in the White House, “since Thomas Jefferson used to dine here, alone!” This magnificent hall contains now about 1,000 logicians. It is probably the greatest assemblage of intellect in Vienna since Kurt Goedel lived here. :-)

This morning Dana Scott told us about the amazing period of the Vienna Circle in the first part of the 20th Century, when Vienna, unquestionably, was the logic capital of the world. The apex of that period was in 1930-1, when Goedel published first the Completeness Theorem and then the Incompleteness Theorem. Unfortunately, that period ended rather tragically. Hans Hahn, Goedel’s PhD advisor, died rather young, at age 54, in 1934. Rudolf Carnap, concerned with the rise of Nazism, emigrated to the US in 1935. Moritz Schlick, the key organizer of the Vienna Circle, was assassinated on his way to class in 1936. In 1939, after the 1938 annexation of Austria by Nazi Germany, Goedel left Vienna and made his way to the United States via a circuitous route. So died logic in Vienna, 75 years ago.

And logic stayed dead in Vienna until the mid 1980s, about 30 years ago, when Matthias Baaz, Georg Gottlob, and Alexander Leitsch, brought it back to life. Today, logic again is flourishing in Vienna, in particular, and in Austria in general, So it is entirely appropriate that today, 75 years after logic died in Austria, we celebrate its revival in the 2014 Vienna Summer of Logic.

1000+ logicians gathering at Vienna’s town hall for the Mayor’s reception. According to Moshe Vardi "the highest concentration of brain power in Vienna since Gödel lived here."

© VSL 2014 / Photography: Nadja Meister

Toller Start: Über 100 Leute in erster LogicLounge

Logic Lounge at Heuer am Karlsplatz: Over a 100 guests enjoying the conversation between Christos Papadimitriou and Helmut Veith on the pancake stacking problem (as solved together with Bill Gates) and the nexus of sex and algorithms

Wie stapelt Bill Gates seine Pfannkuchen? Wie verpackt man die Geschichte der Logik in Comics, und was hat Sex mit Algorithmen zu tun? Über 100 Leute hörten heute in der LogicLounge am Karlsplatz Christos Papadimitriou und Helmut Veith. Mehr davon ab morgen:

The pancake sorting problem

The pancake sorting problem

How does Bill Gates sort a stack of pancakes? How to present the history of logic in a comic, and what has sex got to do with algorithms? Over 100 people attended today’s LogicLounge with Christos Papadimitriou und Helmut Veith. More LogicLounge starting tomorrow: