HISTORY OF THE PROPOSAL
The desire for unified approaches in automated reasoning has been recognized and pursued for years by the experts interested in the Action, resulting in several discussions at scientific conferences. Discussions about coordinated activities started through a number of individual visits and meetings between the experts in years 2007 and 2008. The discussions were particularly intensified after realizing that COST is an ideal instrument to coordinate these activities and that an organized effort is necessary to ensure strong results that will have a large impact on the community and the society. These observations led the experts to jointly draft the proposal.
RECENT PUBLICATIONS BY EXPERTS
Action experts maintain an active publication record, with over 150 relevant publications in years 2007 and 2008 written by the experts that participated in preparation of the proposal. The following is a sample of publications in years 2007 and 2008.
Ahmed Bouajjani, Anca Muscholl, Tayssir Touili: Permutation rewriting and algorithmic verification. Inf. Comput. 205(2): 199-224 (2007)
Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. CAV 2007: 207-220
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. TACAS 2007: 690-705
Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas W. Reps: Interprocedural Analysis of Concurrent Programs Under a Context Bound. TACAS 2008: 282-298
Alexander Malkis, Andreas Podelski, Andrey Rybalchenko: Precise Thread-Modular Verification. SAS 2007: 218-232
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv: Thread-modular shape analysis. PLDI 2007: 266-277
Amine Chaieb, Tobias Nipkow: Proof Synthesis and Reflection for Linear Arithmetic. J. Autom. Reasoning 41(1): 33-59 (2008)
Andreas Griesmayer, Stefan Staber, Roderick Bloem: Automated Fault Localization for C Programs. Electr. Notes Theor. Comput. Sci. 174(4): 95-111 (2007)
Andreas Podelski, Andrey Rybalchenko, Thomas Wies: Heap Assumptions on Demand. CAV 2008: 314-327
Andreas Podelski, Andrey Rybalchenko: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3): (2007)
Andrey Rybalchenko, Viorica Sofronie-Stokkermans: Constraint Solving for Interpolation. VMCAI 2007: 346-362
Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu: Proving non-termination. POPL 2008: 147-158
Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, Roderick Bloem: Anzu: A Tool for Property Synthesis. CAV 2007: 258-262
Bernardo Cuenca Grau, Ian Horrocks, Boris Motik, Bijan Parsia, Peter F. Patel-Schneider, Ulrike Sattler: OWL 2: The next step for OWL. J. Web Sem. 6(4): 309-322 (2008)
Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, Ulrike Sattler: A Logical Framework for Modularity of Ontologies. IJCAI 2007: 298-303
Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, Ulrike Sattler: Just the right amount: extracting modules from ontologies. WWW 2007: 717-726
Birte Glimm, Ian Horrocks, Carsten Lutz, Ulrike Sattler: Conjunctive Query Answering for the Description Logic SHIQ. IJCAI 2007: 399-404
Boris Motik, Ian Horrocks, Ulrike Sattler: Bridging the gap between OWL and relational databases. WWW 2007: 807-816
Boris Motik, Ian Horrocks: OWL Datatypes: Design and Implementation. International Semantic Web Conference 2008: 307-322
Boris Motik, Rob Shearer, Ian Horrocks: Optimized Reasoning in Description Logics Using Hypertableaux. CADE 2007: 67-83
Bruno Marnette, Viktor Kuncak, and Martin Rinard. Polynomial constraints for sets with cardinality bounds. In Foundations of Software Science and Computation Structures (FOSSACS), volume 4423 of LNCS, March 2007.
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi: Proving that programs eventually do something good. POPL 2007: 265-276
Byron Cook, Andreas Podelski, Andrey Rybalchenko: Proving thread termination. PLDI 2007: 320-330
Byron Cook, Daniel Kroening, Natasha Sharygina: Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. 388(1-3): 227-242 (2007)
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv: Proving Conditional Termination. CAV 2008: 328-340
Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi: Automated Verification of Security Policies in Mobile Code. IFM 2007: 37-53
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop Summarization Using Abstract Transformers. ATVA 2008: 111-125
David Déharbe, Silvio Ranise, Jorgiano Vidal: Distributing the Workload in a Lazy Theorem-Prover. Electr. Notes Theor. Comput. Sci. 184: 21-37 (2007)
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Invariant Synthesis for Combined Theories. VMCAI 2007: 378-394
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko: Path invariants. PLDI 2007: 300-309
Dmitry Tsarkov, Ian Horrocks, Peter F. Patel-Schneider: Optimizing Terminological Reasoning for Expressive Description Logics. J. Autom. Reasoning 39(3): 277-316 (2007)
Enric Rodríguez-Carbonell, Deepak Kapur: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4): 443-476 (2007)
Felix Klaedtke, Stefan Ratschan, Zhikun She: Language-Based Abstraction Refinement for Hybrid System Verification. VMCAI 2007: 151-166
Gaël Patin, Mihaela Sighireanu, Tayssir Touili: Spade: Verification of Multithreaded Dynamic and Recursive Programs. CAV 2007: 254-257
Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT 2008: 77-90
Giorgos Stoilos, Giorgos B. Stamou, Jeff Z. Pan, Vassilis Tzouvaras, Ian Horrocks: Reasoning with Very Expressive Fuzzy Description Logics. J. Artif. Intell. Res. (JAIR) 30: 273-320 (2007)
Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm: Logical characterizations of heap abstractions. ACM Trans. Comput. Log. 8(1): (2007)
Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv: Cartesian Partial-Order Reduction. SPIN 2007: 95-112
Görschwin Fey, Stefan Staber, Roderick Bloem, Rolf Drechsler: Automatic Fault Localization for Property Checking. IEEE Trans. on CAD of Integrated Circuits and Systems 27(6): 1138-1149 (2008)
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. on CAD of Integrated Circuits and Systems 27(2): 366-379 (2008)
Hugo Herbelin, Silvia Ghilezan: An approach to call-by-name delimited continuations. POPL 2008: 383-394
Ian Horrocks, Ulrike Sattler: A Tableau Decision Procedure for SHOIQ. J. Autom. Reasoning 39(3): 249-276 (2007)
Ian Horrocks: Logic for Ontology Engineering Corner. J. Log. Comput. 17(4): 615 (2007)
Ian Horrocks: Ontologies and the semantic web. Commun. ACM 51(12): 58-67 (2008)
Jeff Z. Pan, Ian Horrocks: RDFS(FA): Connecting RDF(S) and OWL DL. IEEE Trans. Knowl. Data Eng. 19(2): 192-206 (2007)
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv: Thread Quantification for Concurrent Shape Analysis. CAV 2008: 399-413
Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. PLDI, 2008.
Karin Greimel, Roderick Bloem, Barbara Jobstmann, Moshe Y. Vardi: Open Implication. ICALP (2) 2008: 361-372
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow: The Isabelle Framework. TPHOLs 2008: 33-38
Maria Paola Bonacina, Mnacho Echenim: On Variable-inactivity and Polynomial T-Satisfiability Procedures. J. Log. Comput. 18(1): 77-96 (2008)
Maria Paola Bonacina, Mnacho Echenim: T-Decision by Decomposition. CADE 2007: 199-214
Maria Paola Bonacina, Nachum Dershowitz: Abstract canonical inference. ACM Trans. Comput. Log. 8(1): (2007)
Maria Paola Bonacina, Nachum Dershowitz: Canonical Inference for Implicational Systems. IJCAR 2008: 380-395
Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Daniele Varacca: Security types for dynamic web data. Theor. Comput. Sci. 402(2-3): 156-171 (2008)
Milena Vujosevic-Janicic, Jelena Tomasevic, Predrag Janicic: Random k-GD-SAT Model and its Phase Transition, Journal of Universal Computer Science, Vol. 13, No. 4, pp. 572-591. 2007.
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio: The Barcelogic SMT Solver. CAV 2008: 294-298
Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili: On the Reachability Analysis of Acyclic Networks of Pushdown Systems. CONCUR 2008: 356-371
Noam Rinetzky, G. Ramalingam, Shmuel Sagiv, Eran Yahav: On the complexity of partially-flow-sensitive alias analysis. ACM Trans. Program. Lang. Syst. 30(3): (2008)
Paul B. Jackson, Bill J. Ellis and Kathleen Sharp: Using SMT Solvers to Verify High-Integrity Programs. 2nd International Workshop on Automated Formal Methods, (AFM '07). Atlanta, Georgia, USA, November 2007.
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar: Computing Simulations over Tree Automata. TACAS 2008: 93-108
Peter F. Patel-Schneider, Ian Horrocks: A comparison of two modelling paradigms in the Semantic Web. J. Web Sem. 5(4): 240-250 (2007)
Predrag Janicic and Alan Bundy. Automatic Synthesis of Decision Procedures: a Case Study of Ground and Linear Arithmetic, Kauers et al. (Eds.) Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science, 4573, pp. 80–93. Springer-Verlag, Berlin-Heidelberg, 2007.
Predrag Janicic, Pedro Quaresma: Automatic Verification of Regular Constructions in Dynamic Geometry Systems, Francisco Botana and Tomas Recio (Eds.) Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, 4869, Springer-Verlag, Berlin-Heidelberg, 2007.
Robert Nieuwenhuis, Albert Oliveras: Fast congruence closure and extensions. Inf. Comput. 205(4): 557-580 (2007)
Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev: RAT: A Tool for the Formal Analysis of Requirements. CAV 2007: 263-267
Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv: Shape Analysis by Graph Decomposition. TACAS 2007: 3-18
Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, 2008.
Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In Computed-Aided Verification (CAV), volume 5123 of LNCS, 2008.
Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha: Verification of evolving software via component substitutability analysis. Formal Methods in System Design 32(3): 235-266 (2008)
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. CADE 2007: 362-378
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3-4): 231-254 (2007)
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Towards SMT Model Checking of Array-Based Systems. IJCAR 2008: 67-82
Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: Combining Proof-Producing Decision Procedures. FroCos 2007: 237-251
Stefan Ratschan, Zhikun She: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embedded Comput. Syst. 6(1): (2007)
Stefan Staber, Roderick Bloem: Fault Localization and Correction with QBF. SAT 2007: 355-368
Thanh Tran, Peter Haase, Boris Motik, Bernardo Cuenca Grau, Ian Horrocks: Metalevel Information in Ontology-Based Applications. AAAI 2008: 1237-1242
Tobias Nipkow: Linear Quantifier Elimination. IJCAR 2008: 18-33
Viktor Kuncak and Martin Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In Conference on Automateded Deduction (CADE-21), volume 4603 of LNCS, 2007.
Werner Damm, Guilherme Pinto, Stefan Ratschan: Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. Int. J. Found. Comput. Sci. 18(1): 63-86 (2007)
EARLY STAGE RESEARCHERS
In terms of early stage researchers such as PhD students and postdocs, we firmly believe that the best way to promote them is to expose them to the environment in multiple research groups. This Action therefore concretely proposes to minimize other expenses (such as additional yearly meetings) and instead focus its resources on short-term scientific missions for these researchers.
BROAD PARTICIPATION AND GENDER BALANCE
The Action is doing all that is in its power to attract the top researchers from all eligible countries, from all broadly relevant areas, regardless of their demographic characteristics. It is also committed to promoting gender balance, as described in Section E.4. If approved, the Action membership is expected to grow further both in terms of the number of researchers and the number of participating countries. The program provisions for this growth by the broad nature of the proposed activity and by provisioning for up to two more work groups.
MONITORING PROVISIONS
To ensure progress towards objectives, work group coordinators will monitor the evaluation of objectives and milestones and summarize current progress at yearly meetings.
INDUSTRIAL APPLICATIONS
The activities will continuously be based on practical applications, which will also be the driving force of the benchmarks for the Rich Model Toolkit. Starting from the second year of the Action, the Action will specifically invite members of major research labs and companies with large research and development efforts (specific contacts include IBM Zurich, IBM Haifa, Intel Haifa, ABB, ST Microelectronics Grenoble, Infeneon, OneSpin, and Nokia), to explore the potential for technology transfer and the building of tools in industry based on Rich-Model Toolkit.
A SAMPLE OF NATIONAL PROJECTS COORDINATED BY THE ACTION
The following is a sample list of projects (sorted by country) in which Action experts are currently involved and whose activities will be among those coordinated.
Germany: Verisoft (http://www.verisoft.de/)
Germany: AVACS (http://www.avacs.org/)
Germany: Ph.D. programme Puma (http://puma.in.tum.de/)
UK: EP/F065841/1 HermiT: Reasoning with Large Ontologies (http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/F065841/1)
UK: EP/C543319/2 LOGO: Logics for Ontologies (http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/C543319/2)
UK: EP/E03781X/1 Reasoning Infrastructure for Ontologies and Instances (http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/E03781X/1)
UK: EP/C537211/2 REOL: Reasoning for Expressive Ontology Languages (http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/C537211/2)
Spain:LogicTools Project, funded by the Spanish Spanish Ministry of Science and Education
Serbia: National Project 144030 funded by the Serbian Ministry of Science
Serbia: PROJECT 144029, Models, Languages, Types, and Processes in Computing funded by the Serbian Ministry of Science
Switzerland: Detection of Security Flaws and Vulnerabilities by Guided Model Checking, Swiss National Science Foundation.
Switzerland: Formal Verification Techniques for Security. Tasso Foundation
Switzerland: Precise and Scalable Analyses for Reliable Software, Swiss National Science Foundation.
Italy: Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems.
Romania: CONQUERS: Continuous Quality Evaluation and Restructuring of Software (Romanian national research grant, 2007-2010)
Czech science foundation project GACR 201/08/J020 “Verification of Hybrid Systems - Exploiting the Synergy with Underlying Constraint Solving Technology”