Opendata, web and dolomites

SYMCAR SIGNED

Symbolic Computation and Automated Reasoning for Program Analysis

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "SYMCAR" data sheet

The following table provides information about the project.

Coordinator
TECHNISCHE UNIVERSITAET WIEN 

Organization address
address: KARLSPLATZ 13
city: WIEN
postcode: 1040
website: www.tuwien.ac.at

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country Austria [AT]
 Total cost 1˙500˙000 €
 EC max contribution 1˙500˙000 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2014-STG
 Funding Scheme ERC-STG
 Starting year 2016
 Duration (year-month-day) from 2016-04-01   to  2021-03-31

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    TECHNISCHE UNIVERSITAET WIEN AT (WIEN) coordinator 1˙500˙000.00

Map

 Project objective

Individuals, industries, and nations are depending on software and systems using software. Automated approaches are needed to eliminate tedious aspects of software development, helping software developers in dealing with the increasing software complexity. Automatic program analysis aims to discover program properties preventing programmers from introducing errors while making changes and can drastically cut the time needed for program development. This project addresses the challenge of automating program analysis, by developing rigorous mathematical techniques analyzing the logically complex parts of software. We will carry out novel research in computer theorem proving and symbolic computation, and integrate program analysis techniques with new approaches to program assertion synthesis and reasoning with both theories and quantifiers. The common theme of the project is a creative development of automated reasoning techniques based on our recently introduced symbol elimination method. Symbol elimination makes the project challenging, risky and interdisciplinary, bridging together computer science, mathematics, and logic. Symbol elimination will enhance program analysis, in particular by generating polynomial and quantified first-order program properties that cannot be derived by other methods. As many program properties can best be expressed using quantified formulas with arithmetic, our project will make a significant step in analyzing large systems. Since program analysis requires reasoning in the combination of first-order logic and theories, we will design efficient algorithms for automated reasoning with both theories and quantifiers. Our results will be supported by the development of world-leading tools supporting symbol elimination in program analysis. Our project brings breakthrough approaches to program analysis, which, together with other advances in the area, will reduce the cost of developing safe and reliable computer systems used in our daily life.

 Publications

year authors and title journal last update
List of publications.
2017 Laura Kovacs, Andrei Voronkov
First-Order Interpolation and Interpolating Proof Systems
published pages: 49-64, ISSN: , DOI:
Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) EasyChair EPiC Series in Comput 2019-08-06
2016 Yuting Chen, Laura Kovács, Simon Robillard
Theory-Specific Reasoning about Loops with Arrays using Vampire
published pages: 16-32, ISSN: , DOI:
Proceedings of the 3rd Vampire Workshop EasyChair EPiC Series in Compu 2019-08-06
2017 Giles Reger, Martin Suda
Set of Support for Theory Reasoning
published pages: 124-134, ISSN: , DOI:
Proceedings of the 2017 International Workshop on the Implementation of Logics (IWIL) Kalpa Publications in Computing 2019-08-06
2017 Moulay A. Barkatou, Maximilian Jaroschek, Suzy S. Maddah
Formal solutions of completely integrable Pfaffian systems with normal crossings
published pages: 41-68, ISSN: 0747-7171, DOI: 10.1016/j.jsc.2016.11.018
Journal of Symbolic Computation 81 2019-08-06
2017 Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
Blocked Clauses in First-Order Logic
published pages: 31-48, ISSN: , DOI:
Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) EasyChair EPiC Series in Comput 2019-08-06
2017 Laura Kovacs
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)
published pages: 3:13:1, ISSN: , DOI: 10.4230/LIPIcs.CSL.2017.3
Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL) LIPIcs 82, 2019-08-06
2017 Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution
published pages: 101-124, ISSN: 0747-7171, DOI: 10.1016/j.jsc.2016.07.023
Journal of Symbolic Computation 80 2019-08-06
2017 Laura Kovács, Simon Robillard, Andrei Voronkov
Coming to terms with quantified reasoning
published pages: 260-270, ISSN: 0362-1340, DOI: 10.1145/3093333.3009887
ACM SIGPLAN Notices 52/1 2019-08-06
2017 Jan Jakubuv, Martin Suda, Josef Urban
Automated Invention of Strategies and Term Orderings for Vampire
published pages: 121-133, ISSN: , DOI:
Proceedings of the 3rd Global Conference on Artificial Intelligence (GCAI) EasyChair EPiC Series in Comput 2019-08-06
2017 Giles Reger, Martin Suda
Checkable Proofs for First-Order Theorem Proving
published pages: 55-63, ISSN: , DOI:
Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE) EasyChair EPiC Series in Comput 2019-08-06
2016 Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
A Clausal Normal Form Translation for FOOL
published pages: 53-71, ISSN: , DOI:
Proceedings of the 2nd Global Conference on Artificial Intelligence (GCAI) EasyChair EPiC Series in Comput 2019-08-06
2018 Simon Robillard
An Inference Rule for the Acyclicity Property of Term Algebras
published pages: 20-32, ISSN: , DOI:
Proceedings of the 4th Vampire Workshop EasyChair EPiC Series Volume 53 2019-08-06
2018 Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF
published pages: 1-27, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9482-4
Journal of Automated Reasoning 2019-08-06
2018 Adrian Rebola Pardo, Martin Suda
A Theory of Satisfiability-Preserving Proofs in SAT Solving
published pages: 583-603, ISSN: , DOI:
Proceedings of the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR) EasyChair EPiC Series, volume 5 2019-08-06
2018 Giles Reger, Martin Suda, Andrei Voronkov
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
published pages: 3-22, ISSN: , DOI: 10.1007/978-3-319-89960-2_1
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) LNCS 10805 2019-08-06
2018 Mikolas Janota, Martin Suda
Towards Smarter MACE-style Model Finders
published pages: 454-470, ISSN: , DOI:
Proceedings of the 22nd 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR) EasyChair EPiC Series, volume 5 2019-08-06
2018 Martin Suda, Bernhard Gleiss
Local Soundness for QBF Calculi
published pages: 217-234, ISSN: , DOI: 10.1007/978-3-319-94144-8_14
Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT) LNCS 10929 2019-08-06
2018 Giles Reger, Martin Suda
Local proofs and AVATAR
published pages: 33-41, ISSN: , DOI:
Proceedings of the 4th Vampire Workshop EPiC Series in Computing 53 2019-08-06
2018 Giles Reger, Martin Suda
Incremental Solving with Vampire
published pages: 52-63, ISSN: , DOI:
Proceedings of the 4th Vampire Workshop EPiC Series in Computing 53 2019-08-06
2018 Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Invariant Generation for Multi-Path Loops with Polynomial Assignments
published pages: 226-246, ISSN: , DOI: 10.1007/978-3-319-73721-8_11
Proceedings of the 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) LNCS 10747 2019-08-06
2018 Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Aligator.jl - A Julia Package for Loop Invariant Generation
published pages: 111-117, ISSN: , DOI: 10.1007/978-3-319-96812-4_10
Proceedings of the International Conference on Intelligent Computer Mathematics (CICM) LNCS 11006 2019-08-06
2018 Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
A FOOLish Encoding of the Next State Relations of Imperative Programs
published pages: 405-421, ISSN: , DOI: 10.1007/978-3-319-94205-6_27
Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR) LNCS 10900 2019-08-06
2018 Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
Superposition with Datatypes and Codatatypes
published pages: 370-387, ISSN: , DOI: 10.1007/978-3-319-94205-6_25
Proceedings of the 9th International Conference on Automated Reasoning (IJCAR) LNCS 10900 2019-08-06
2018 Bernhard Gleiss, Simon Robillard, Laura Kovács
Loop Analysis by Quantification over Iterations
published pages: 381-399, ISSN: , DOI:
Proceedings of the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR) EasyChair EPiC Series, volume 5 2019-08-06

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "SYMCAR" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "SYMCAR" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

PROGRESS (2019)

The Enemy of the Good: Towards a Theory of Moral Progress

Read More  

Photopharm (2020)

Photopharmacology: From Academia toward the Clinic.

Read More  

VictPart (2019)

Righting Victim Participation in Transitional Justice

Read More