Today Simon Legner successfully defended his master thesis on “Non Linear Arithmetic”.
- Details
- Category: News Archive
Thibault works as a researcher on the project “Interactive Proof: Proof Translation, Premise Selection, Rewriting “.
- Details
- Category: News Archive
Harald Zankl’s research is concerned with the automated analysis of programs.
His thesis ``Challenges in Automation of Rewriting’‘ explains how several properties of rewrite systems can be investigated automatically.
- Details
- Category: News Archive
We invite candidates for a PhD student or postdoc researcher position to start as soon as possible in the ongoing Certification Redux project. Click here for details. output of FORT can be certified. Moreover, the expressiveness and the performance of FORT will be increased, and its limitations better understood.
- Details
- Category: News Archive
In its 63rd board meeting the Austrian Science Fund (FWF) approved Aart Middeldorp’s project proposal. The 3-year project will start on September 1 and has a grant amount of EUR 345K.
FORTissimo is about the first-order theory of rewriting, which is a decidable theory for left-linear right-ground rewrite systems in which well-known properties like confluence, normalization and termination are expressible. The decision procedure for this theory is based on tree automata techniques and a first implementation was conducted by Franziska Rapp. The resulting tool FORT is equipped with a synthesis mode to generate rewrite systems that satisfy properties expressible in the first-order theory of rewriting.
The aim of FORTissimo is to formalize the decision procedure in the proof assistant Isabelle/HOL such that the output of FORT can be certified. Moreover, the expressiveness and the performance of FORT will be increased, and its limitations better understood.
- Details
- Category: News Archive
CL is proud to announce that Cezary Kaliszyk’s project SMART: “Strong Modular proof Assistance: Reasoning across Theories” has been approved by the European Research Council. The project has a duration of 5 years and a total grant amount of EUR 1450K. The project will commence on March 1, 2017.
The goal of SMART is to develop a strong and uniform learning-reasoning system available for multiple logical foundations. This system will be capable of providing proof advice for multiple proof assistants and the combinations of their libraries.
More information in German can be found here.
- Details
- Category: News Archive
This month the 5th Confluence Competition (CoCo 2016) took place at CLA 2016 in Obergurgl. It ran live during IWC 2016. Four confluence tools and one certifier that are developed at CL participated and won several categories (results).
Confluence is a central property of programs since it ensures uniqueness of computation results. Numerous techniques for proving confluence of rewrite systems, lambda calculi, etc. have been developed, and many of them are implemented in automated tools that (dis)prove confluence. CoCo aims to foster the development of techniques for (dis)proving confluence automatically by setting up a dedicated competition among confluence tools. Previous editions of the competition were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015).
In 2016 CoCo had four competition categories
- confluence of first-order term rewrite systems (TRS)
- confluence of conditional term rewrite systems (CTRS)
- certification (CPF)
- confluence of higher-order term rewrite systems (HRS)
and tools from Innsbruck participated and won in all of them:
- CSI won the TRS category
- ConCon was the most powerful tool for CTRSs
- The certifier CeTA in combination with CSI for TRSs and with ConCon for CTRSs won the category for certified confluence proofs
- CSI^ho was the strongest tool in the higher-order category
Additionally there were three demonstration categories
- ground confluence of many-sorted term rewrite systems (GCR)
- unique normalization of term rewrite systems (UN) – new this year
- confluence of nominal rewrite systems (NRS)
with CL participation by CSI in the UN category and the newcomer FORT in both the UN and the GCR categories. All these tools are open source.
- Details
- Category: News Archive
Between September 5 and 9, the international workshop on confluence, the international workshop on termination, the Austria-Japan workshop on rewriting, and the logic, complexity and automation project meeting have been conducted in the Obergurgl university center. With more than 50 presentations, eight invited speakers, two competitions, and nearly 70 international participants it was an exciting event, with ample discussion on new research areas as well as the strengthening and initiation of collaborations.
Detailed information on the workshop is available at its website.
- Details
- Category: News Archive
The international cooperation project was approved by the French Science Fund (ANR) and the Austrian Science Fund (FWF). The project is carried out by a consortium of four partners, two Austrian and two French, all being internationally recognised for their work on structural proof theory, but each coming from a different tradition.
The project has a duration of 3 years and a total grant amount of EUR 630K. The project has started on January 1, 2016.
The FISP project is part of a long-term, ambitious project whose objective is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations.
- Details
- Category: News Archive
Today Franziska successfully defended her master thesis on “Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground TRSs”. Franziska will continue for a PhD and be employed on the FWF-funded project “From Confluence to Unique Normal Forms: Certification and Complexity“.operations.
- Details
- Category: News Archive
The Termination Competition 2015 is over. Five termination/complexity tools and one certifier developed by CL members participated and won in several categories (results).
Termination of programs is a fundamental topic in computer science. While being undecidable in general, numerous techniques have been developed to automatically prove/disprove termination of meaningful programs.
The international competition of termination tools is executed annually since 2004, after a tool demonstration in 2003. Recent competitions were executed live in the main conferences of the field: VSL 2014, RDP 2013, IJCAR 2012, RTA 2011, and FLoC 2010.
This year, 15 tools (plus one certifier) ran in 22 competition categories and eight demonstrations. Tools by CL members dominated three competition and three demonstration categories.
Links:
- Details
- Category: News Archive