Opendata, web and dolomites


Analysis, Verification, and Synthesis for Infinite-State Systems

Total Cost €


EC-Contrib. €






Project "AVS-ISS" data sheet

The following table provides information about the project.


Organization address
postcode: 80539
website: n.a.

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 Germany [DE]
 Total cost 1˙834˙975 €
 EC max contribution 1˙834˙975 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2014-CoG
 Funding Scheme ERC-COG
 Starting year 2015
 Duration (year-month-day) from 2015-08-01   to  2020-07-31


Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 


 Project objective

The central objective of this project is to investigate key algorithmic verification questions concerning two fundamental mathematical structures used to model and analyse infinite-state systems, namely discrete linear dynamical systems and counter automata, in both ordinary and parametric form. Motivated especially by applications to software model checking (more specifically the termination of linear loops and predicate abstraction computations), as well as parametric real-time reasoning and the verification of Markov chains, we will focus on model-checking, module-checking, and synthesis problems for linear dynamical systems and one-counter automata against various fragments and extensions of Linear Temporal Logic (LTL) specifications. The key deliverables will be novel verification algorithms along with a map of the complexity landscape. A second objective is then to transfer algorithmic insights into practical verification methodologies and tools, in collaboration with colleagues in academia and industrial research laboratories.

We will build on a series of recent advances and breakthroughs in these areas (some of which from the PI’s team) to attack a range of specific algorithmic problems. We believe that this line of research will not only result in fundamental theoretical contributions and insights in their own right—potentially answering mathematical questions that have been open for years or even decades—but will also impact the practice of formal verification and lead to new and more powerful methods and tools for the use of engineers and programmers.


year authors and title journal last update
List of publications.
2019 Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell
Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
published pages: 1027-1048, ISSN: 1432-4350, DOI: 10.1007/s00224-019-09913-3
Theory of Computing Systems 63/5 2019-10-03
2019 Mehran Hosseini, Joel Ouaknine, James Worrell
Termination of Linear Loops over the Integers
published pages: 118:1-118:13, ISSN: , DOI: 10.4230/lipics.icalp.2019.118
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP) LIPIcs 132 2019-10-03
2019 Thomas Colcombet, Joel Ouaknine, Pavel Semukhin, James Worrell
On Reachability Problems for Low-Dimensional Matrix Semigroups
published pages: 44:1-44:15, ISSN: , DOI: 10.4230/lipics.icalp.2019.44
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP) LIPIcs 132 2019-10-03
2019 Nir Drucker, Hsi-Ming Ho, Joël Ouaknine, Michal Penn, Ofer Strichman
Cyclic-routing of Unmanned Aerial Vehicles
published pages: 18-45, ISSN: 0022-0000, DOI: 10.1016/j.jcss.2019.02.002
Journal of Computer and System Sciences 103 2019-10-03
2019 Joël Ouaknine, Amaury Pouly, João Sousa-Pinto, James Worrell
On the Decidability of Membership in Matrix-exponential Semigroups
published pages: 1-24, ISSN: 0004-5411, DOI: 10.1145/3286487
Journal of the ACM 66/3 2019-10-03
2016 Ventsislav Chonev, Joël Ouaknine, James Worrell
On the Complexity of the Orbit Problem
published pages: 1-18, ISSN: 0004-5411, DOI: 10.1145/2857050
Journal of the ACM 63/3 2019-06-06
2017 Daniel Bundala, Joel Ouaknine
On parametric timed automata and one-counter machines
published pages: 272-303, ISSN: 0890-5401, DOI: 10.1016/j.ic.2016.07.011
Information and Computation 253 2019-06-06
2016 Ventsislav Chonev, Joel Ouaknine, and James Worrell
On the Skolem Problem for Continuous Linear Dynamical Systems
published pages: , ISSN: , DOI: 10.4230/LIPIcs.ICALP.2016.100
43rd International Colloquium on Automata, Languages, and Programming (ICALP) 2019-06-06
2016 Antonia Lechner, Richard Mayr, Joel Ouaknine, Amaury Pouly, and James Worrell
Model Checking Flat Freeze LTL on One-Counter Automata
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CONCUR.2016.29
27th International Conference on Concurrency Theory (CONCUR) 2019-06-06
2016 Bruna, Maria; Grigore, Radu; Kiefer, Stefan; Ouaknine, Joël; Worrell, James
Proving the Herman-Protocol Conjecture
published pages: , ISSN: , DOI: 10.4230/LIPIcs.ICALP.2016.104
43rd International Colloquium on Automata, Languages, and Programming (ICALP) 2019-06-06
2016 Christoph Haase, Joël Ouaknine, James Worrell
Relating Reachability Problems in Timed and Counter Automata
published pages: 317-338, ISSN: 0169-2968, DOI: 10.3233/FI-2016-1316
Fundamenta Informaticae 143/3-4 2019-06-06
2016 Ranko Lazić, Joël Ouaknine, James Worrell
Zeno, Hercules, and the Hydra
published pages: 1-27, ISSN: 1529-3785, DOI: 10.1145/2874774
ACM Transactions on Computational Logic 17/3 2019-06-06
2017 Nathanael Fijalkow, Pierre Ohlmann, Joel Ouaknine, Amaury Pouly, and James Worrell
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
published pages: , ISSN: , DOI: 10.4230/LIPIcs.STACS.2017.29
34th Symposium on Theoretical Aspects of Computer Science (STACS) 2019-06-06
2017 Shaull Almagor, Joel Ouaknine, and James Worrell
The Polytope-Collision Problem
published pages: , ISSN: , DOI: 10.4230/LIPIcs.ICALP.2017.24
44th International Colloquium on Automata, Languages, and Programming (ICALP) 2019-06-06

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "AVS-ISS" 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 ( 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 "AVS-ISS" are provided by the European Opendata Portal: CORDIS opendata.

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

NanoPD_P (2020)

High throughput multiplexed trace-analyte screening for diagnostics applications

Read More  

TOROS (2019)

A Theory-Oriented Real-Time Operating System for Temporally Sound Cyber-Physical Systems

Read More  

EVOMENS (2020)

The evolution of menstruation in primates

Read More