VSL 2014: VIENNA SUMMER OF LOGIC 2014
ITP ON SUNDAY, JULY 20TH, 2014
Days:
previous day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 123: FLoC Plenary Talk (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Plenary Talk: Electronic voting: how logic can help?

ABSTRACT. Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures.

After an introduction to electronic voting, we will describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.

10:15-10:45Coffee Break
10:15-18:00 Session 126A: FLoC Olympic Games Big Screen: CASC Automated Theorem Proving System Competition (CASC-J7) (joint with 9 other meetings)
Location: FH, 2nd floor
10:15
FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7)

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

10:15-18:00 Session 126B: FLoC Olympic Games Big Screen: Termination Competition (termComp) (joint with 9 other meetings)
Location: FH, 2nd floor
10:15
FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014)
SPEAKER: Albert Rubio

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

13:00-14:30Lunch Break
14:30-16:00 Session 129G: FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (joint with 9 other meetings)
Location: FH, Hörsaal 2
14:30
FLoC Olympic Games: Answer Set Programming Modeling Competition 2014
SPEAKER: unknown

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

16:00-16:30Coffee Break