FLoC Olympic Games 2014

Citius, Maius, Potentius – Faster, Bigger, More Powerful

icon_11079

FLoC Olympic Games Theme:
Kurt Gödel Fanfare (© Michael F. P. Huber)

icon_11079

floc_logo_color_big

The aim of the FLoC Olympic Games 2014 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.

The arena had been set up to display the competition events to a broad audience at the Vienna Summer of Logic. Big Screen events show live performances of the individual 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. Thus 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.

FLoC Olympic Games at a Glance

From the wide field of satisfiability solvers to automatic theorem provers and term rewriters, from declarative logic programming solvers and ontology reasoners to automatic software verifiers, from programs that check models of hardware designs to solvers that automatically synthesize computer programs, and to provers that test program termination, the FLoC Olympic Games will bring together theorists and practitioners, allowing them to learn the advancements and new results in other fields, and gain new insights. And last but not least, the Games will celebrate not only the champions, but all the contenders of the FLoC Olympics whose participation makes the competitions as they are and motivates everyone to show their best, as we believe it is not the winning but the participation that counts.

July
2014
Sat,
12th
Sun,
13th
Mon,
14th
Tue,
15th
Wed,
16th
Thu,
17th
Fri,
18th
Sat,
19th
Sun,
20th
Mon,
21st
VSL Joint Award
Ceremonies (16:30-19:00)
VSL
Award
1
VSL
Award
2
Big Screens (all-day), FLoC Panel (08:45-10:15) Big
Screen
1
FLoC Panel Big
Screen
2
Competition Events and Sessions CoCo SMT-COMP ASPCOMP SV-COMP
ORE ORE CASC-J7
QBF Gallery CSSC termCOMP
Max-SAT HWMCC
SAT-COMP SyGuS-COMP
SYNTCOMP
July
2014
Sat,
12th
Sun,
13th
Mon,
14th
Tue,
15th
Wed,
16th
Thu,
17th
Fri,
18th
Sat,
19th
Sun,
20th
Mon,
21st

Award Ceremonies

kurt_goedel_medal

Copyright (C) Münze Österreich AG

The Vienna Summer of Logic features two joint award ceremonies during which distinguished laureates will receive prizes for their excellent work or lifetime achievements.  Both ceremonies are located in the
official flagship hall of Vienna University of Technology called Kuppelsaal.  Renowned scientists will present the victors of each award with Kurt Gödel Society medals and FLoC Olympic Games award certificates.

  1. VSL Joint Award Ceremony: Thursday, July 17 2014, 16:30-19:00
  2. VSL Joint Award Ceremony: Monday, July 21 2014, 16:30-19:00

Live Events: Big Screens and Modeling Competition

Some competitions will take place during the Vienna Summer of Logic. The evaluation progress and results will be presented live and on-site on public Big Screens. The ASP Modeling Competition 2014 will host a live modeling contest.

The whole-day Big Screen events and the on-site Modeling Competition are

  1. Big Screen: Friday, July 18 2014, 09:00-18:00
    • OWL Reasoner Evaluation 2014 (ORE 2014), Live

      OWL is a logic-based ontology language standard designed to promote interoperability, particularly in the context of the (Semantic) Web. The standard has encouraged the development of numerous OWL reasoning systems, and such systems are already key components of many applications. The 2nd OWL Reasoner Evaluation Competition (ORE 2014) compares and evaluates 11 OWL reasoning systems on a data set containing a wide range of ontologies from the web, obtained through a standard web crawl and the Google Custom Search API, and a snapshot from the well known BioPortal repository. Some user submitted ontologies spice up the corpus with particularly relevant and difficult test cases. The ontologies in the test set are binned by profiles to enable the participation of reasoners specialised on the EL and DL profiles of OWL. The evaluation is performed in three different categories that cover the important tasks of ontology classification, consistency checking, and ontology realisation (i.e., the computation of entailed types of individuals).

    • Satisfiability Modulo Theories solver competition (SMT-COMP 2014), Live

      The 9th SMT competition seeks to spur interest, usefulness, and capability of SMT solvers in application-centric contexts. This year’s competition has 12-15 participants (a record number) with problems drawn from 117K benchmarks in 26 different logics; problems are expressed in a common, standardized format (SMTLIBv2). There are tracks measuring sequential and parallel performance and emulating batch and interactive application environments. The benchmarks are increasingly supplied by application environments that use SMT solvers to discharge constraint problems and verification conditions that arise in software verification, scheduling, component placement and other domains. This year’s competition also inaugurates a experimental competition on Separation Logic SMT solvers and problems, also using the SMTLIBv2 problem format. The competition is run over a period of a month using the StarExec computation cluster.

  2. Big Screen: Sunday, July 20 2014, 10:15-18:00
    • The 7th IJCAR ATP System Competition (CASC-J7)

      The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J7 will be held on 20th July 2014, during the 7th International Joint Conference on Automated Reasoning (IJCAR, which incorporates CADE), CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of the number of problems solved, the number of problems solved with a solution output, and the average runtime for problems solved; in the context of: a bounded number of eligible problems, chosen from the TPTP Problem Library, and specified time limits on solution attempts. The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. The panel members are Bernhard Beckert, Maria Paola Bonacina, and Aart Middeldorp.

    • Termination Competition (termCOMP 2014)

      The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. Moreover, there are also categories for automated complexity analysis. In all categories, participation of tools providing certified proofs is welcome. In every category, all participating tools of that category are run on a randomly selected subset of the available problems. The goal of the termination competition is to demonstrate the power of the leading tools in each of these areas. The 2014 execution of the competition is organized by Johannes Waldmann and Stefan von der Krone. The Steering Committee is formed by Jürgen Giesl, Frederic Mesnard, Albert Rubio (Chair), René Thiemann and Johannes Waldmann.

  3. Answer Set Programming Modeling Competition 2014: Sunday, July 20 2014, 14:30-16:00, FH HS2

    Answer Set Programming (ASP) is a well-established paradigm of declarative programming that has been developed in the field of logic programming and nonmonotonic reasoning. The ASP Modeling Competition 2014, held on-site collocated with the 30th International Conference on Logic Programming (ICLP), follows the spirit of Prolog Programming Contests from previous ICLP editions. That is, complex problems of various kinds are waiting to be modeled, using the ASP-Core-2 standard input language of ASP systems. Dauntless programmers, novices and experts, are encouraged to team up, take the challenge and the glory.

List of Olympic Disciplines

Competition Affiliation
1 Fifth Answer Set Programming Competition (ASPCOMP 2014) ICLP 2014
2 The 7th IJCAR ATP System Competition (CASC-J7) IJCAR 2014
3 3rd Confluence Competition (CoCo 2014) IWC 2014
4 Configurable SAT Solver Challenge (CSSC 2014) SAT 2014
5 Hardware Model Checking Competition (HWMCC 2014) CAV 2014
6 Ninth Max-SAT Evaluation (Max-SAT 2014) SAT 2014
7 OWL Reasoner Evaluation (ORE 2014) ORE 2014
8 QBF Gallery 2014 QBF 2014
9 SAT Competition 2014 (SAT-COMP 2014) SAT 2014
10 Satisfiability Modulo Theories solver competition (SMT-COMP 2014) SMT 2014
11 Competition on Software Verification (SV-COMP 2014) TACAS 2014
12 Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) CAV 2014
13 Synthesis Competition (SYNTCOMP 2014) CAV 2014
14 Termination Competition (termCOMP 2014) IJCAR 2014

Sponsors

HWMCC 2014 aalto_logo oski_tech_logo arise_logo
SAT-COMP 2014 satassoc_logo
SyGus-COMP 2014 excape_logo microsoft_research_logo
SYNTCOMP 2014 arise_logo

Organization

The FLoC Olympic Games 2014 are organized by Thomas Krennwallner.