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

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

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

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.

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

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.
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.
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