Category Archives: VSL Blog

2014 CAV Award

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

The 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: http://www.prlog.org/12350330-2014-cav-computer-aided-verification-conference-award-announcement.html

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

by
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. Knight The 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

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

: World premiere of “Tribute to Kurt Gödel” performed by Adamas string quartet

: Dana Scott awarding Marcin Sabok in the Logical Foundations of Mathematics category

: Dana Scott awarding Matteo Mio in the Logical Foundations of Computer Science category

: Dana Scott awarding Gianluigi Greco in the Logical Foundations of Artificial Intelligence category

: Winners of the the 2014 Kurt Goedel Research Prize Fellowships Competition

FLoC Olympic Games

: Winners of the 3rd Confluence Competition (CoCo 2014)

: Winners of the Configurable SAT Solver Challenge (CSSC 2014)

: Winners of the Ninth Max-SAT Evaluation (Max-SAT 2014)

: Winners of QBF Gallery 2014

: Winners of SAT Competition 2014 (SAT-COMP 2014)

Vardi Fest

: Moshe Vardi’s birthday cake

: Happy Birthday!

[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

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.

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.