#	Pagina
attuale pagina	/open-h2020/projects/197841/index.html

Opendata, web and dolomites

SYMCAR SIGNED

Symbolic Computation and Automated Reasoning for Program Analysis

Total Cost €

EC-Contrib. €

Partnership

Views

Outcomes and
results

SYMCAR project word cloud

Explore the words cloud of the SYMCAR project. It provides you a very rough idea of what is the project "SYMCAR" about.

analyzing drastically software mathematical helping eliminate discover world complexity interdisciplinary programmers polynomial computation nations tools logically computer depending synthesis theme developers automated elimination dealing individuals mathematics expressed brings automating life risky safe carry techniques integrate area efficient daily cut time rigorous logic algorithms quantifiers automatic creative introducing generating breakthrough parts combination supporting tedious preventing formulas symbol theorem arithmetic theories symbolic first reasoning industries reduce bridging quantified science proving errors assertion

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

List of publications.
year	authors and title	journal	last update
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.