View: session overviewtalk overviewside by side with other conferences

09:00-10:15 Session 64A: Opening + Invited Talk 1
Location: FH, Seminarraum 134A
Invited talk: Proof and Refutations for Horn-clause Encodings of Reachability Problems

ABSTRACT. The talk focuses on solving program reachability problems by means of a Horn-clause style program encoding and suitable decision procedures. We will first examine a way to construct the necessary invariants using a combination of abstract interpretation and DPLL-style satisfiability solving. We will then consider a technique for generating counterexamples, and ways how these counterexamples can be used for proof in a synergistic fashion. I will finally show an encoding for concurrent systems based on partial-order semantics.

10:15-10:45Coffee Break
10:45-13:00 Session 66AL: Technical Session
Location: FH, Seminarraum 134A
Please consult the program at http://vsl2014.at/hcvs
13:00-14:30Lunch Break
14:30-15:30 Session 75AL: Invited Talk (joint with VPT)
Location: FH, Seminarraum 134A
Invited talk: Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools
We argue that formal methods such as B can be used to conveniently express a wide range of constraint satisfaction problems.
We also show that some problems can be solved quite effectively by existing formal methods tools such as Alloy or ProB.
We illustrate our claim on several examples.
Our approach is particularly interesting when a high assurance of correctness is required.
Indeed, validation and double checking of solutions is available for certain formal methods tools and formal proof can be applied to establish important properties or
 provide unambiguous semantics to problem specifications.
The experiments also provide interesting insights about the effectiveness of existing formal method tools, and highlight interesting avenues for future uimprovement.
15:30-16:00 Session 78C: Technical Session
Location: FH, Seminarraum 134A
Please consult the program at http://vsl2014.at/hcvs
16:00-16:30Coffee Break
16:30-19:00 Session 79A: VSL Joint Award Ceremony 1
Location: MB, Kuppelsaal
Foundations and Technology Competitions Award Ceremony

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

  • Logical Foundations of Mathematics,
  • Logical Foundations of Computer Science, and
  • Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

  • Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
  • Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
  • Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.


FLoC Olympic Games Award Ceremony 1

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

  • 3rd Confluence Competition (CoCo 2014);
  • Configurable SAT Solver Challenge (CSSC 2014);
  • Ninth Max-SAT Evaluation (Max-SAT 2014);
  • QBF Gallery 2014; and
  • SAT Competition 2014 (SAT-COMP 2014).
FLoC Closing Week 1
SPEAKER: Helmut Veith
16:30-18:00 Session 80E: Technical Session + Discussion
Location: FH, Seminarraum 134A
Please consult the program at http://vsl2014.at/hcvs