COST Report 2011

Please enter any relevant information below and provide the relevant links. Thanks!

Please provide this information by April 30th. Sorry for the late notice! –vkuncak

Joint publications by authors from different participating institutions:

• Verified Resource Guarantees using COSTA and KeY. Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez, in: Proc. ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM'11), 24-25 January 2011 - Austin, Texas, USA, ACM Press.

• HATS: A Formal Software Product Line Engineering Methodology. Dave Clarke, Nikolay Diakov, Reiner Hähnle, Einer Broch Johnsen, German Puebla, Balthasar Weitzel, Peter Wong, in: 1st International Workshop on Formal Methods in Software Product Line Engineering (Jeju Island, South Corea).

• Practical Aspects of Automated Deduction for Program Verification. Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer, in: KI - Künstliche Intelligenz, Volume 24, Number 1 / April, 2010, Pages 43-49, Springer Berlin / Heidelberg.

• Dynamic QoS Management and Optimisation in Service-Based Systems. Radu Calinescu, Lars Grunske, Marta Kwiatkowska, Raffaela Mirandola and Giordano Tamburrelli, in: IEEE Transactions Software Engineering, October 2010 (http://dx.doi.org/10.1109/TSE.2010.92).

• Peter Habermehl, Lukas Holik, Jiri Simacek, Adam Rogalewicz, and Tomas Vojnar. Forest Automata for Verification of Heap Manipulation. In Proc. of 23rd International Conference on Computer Aided Verification—CAV'11, to appear in LNCS, Springer-Verlag, 2011.

• Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tomas Vojnar. Programs with Lists are Counter Automata. Formal Methods in System Design, 38(2):158–192, Springer-Verlag, 2011.

• Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic: Types for role based access control of dynamic web data. WFLP'10 invited talk, Lecture Notes in Computer Science 6559: 1-29, Springer-Verlag (2011).

Projects related to the topic of the Action (not restricted to joint projects).

• COST IC0701, http://www.cost-ic0701.org/

• HATS, www.hats-project.eu

• Charter, http://charterproject.ning.com/

• KeY, http://www.key-project.org/

• EternalS, https://www.eternals.eu/

• Cloud Computing - LSCITS, http://www1.aston.ac.uk/eas/research/groups/csrg/research-projects/cloud-computing/

• Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, Czech Science Foundation P103/10/0306, http://www.fit.vutbr.cz/research/view_project.php.en?id=475

• Automata and Logic for Symbolic Verification of Software, Czech-French Barrande project MEB 021023, http://www.fit.vutbr.cz/research/view_project.php.en?id=493

• Project Diamond (Diagnosis, Error Modelling and Correction for Reliable Systems Design) http://www.fp7-diamond.eu/

• Project Coconut (the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation) http://www.iaik.tugraz.at/content/research/design_verification/coconut/

• ToMeSo (Tools and Methods for Scalable Software Verification) - http://www.itu.dk/research/pls/wiki/index.php/Tools_and_Methods_for_Scalable_Software_Verification_(TOMESO) (Lars Birkdedal)

• MOREASO (Modular Reasoning about Software) - http://www.itu.dk/people/birkedal/moreaso (Lars Birkdedal)

• LIME2 (LightweIght formal Methods for distributed component-based Embedded systems) - http://www.tcs.hut.fi/Research/Logic/LIME2/ (Ilkka Niemelä)

• StMcDes (Symbolic Testing and Model Checking of Distributed Embedded Systems) - http://www.tcs.hut.fi/Research/Logic/StMcDes.shtml (Ilkka Niemelä)

• MCM (Methods for Constructing and Solving Large Constraint Models) - http://www.tcs.hut.fi/Research/Logic/MCM.shtml (Ilkka Niemelä)

• MODSAFE (Model-Based Safety Evaluation of Automation Systems) http://www.tcs.hut.fi/Research/Logic/MODSAFE/ (Keijo Heljanko)

• ASCENS http://www.ascens-ist.eu (Barbara Jobstmann)

• Secure Type Systems and Deduction - DFG Project http://www4.in.tum.de/proj/theoremprov/local_projects/rs3.html (Tobias Nipkow)

• SEMACODE (Stratégies d'Évaluation, Machines Abstraites et COntrôle DElimité) INRIA Associate Team Project (Hugo Herbelin, Silvia Ghilezan)

Events (workshops, conferences, summer schools) related to the action, where one of the participants is organiser, PC chair, or similar (not just PC member).

• Reiner Hähnle was co-PC chair of IJCAR 2010

• Radu Calinescu was PC co-chair of ICECCS 2010 (http://web.comlab.ox.ac.uk//ICECCS2010/), Monterey 2010 (http://www.montereyworkshop.org/home.html); advisory committee co-chair of ADAPTIVE-2010 (http://www.iaria.org/conferences2010/ADAPTIVE10.html), ICAS-2010 (http://www.iaria.org/conferences2010/ICAS10.html), ADAPTIVE-2011 (http://www.iaria.org/conferences2011/ADAPTIVE11.html), ICAS-2011 (http://www.iaria.org/conferences2011/ICAS11.html); co-organiser of a 2011 Cloud Computing Summer School (https://sites.google.com/site/cloudcomputingsummerschool2011/)

• Tomas Vojnar is a PC co-chair of the MEMICS 2011 workshop (http://www.memics.cz/2011/)

• Roderick Bloem is a Chair for Austrian Rigorous Systems Engineering Society

• Roderick Bloem is a Chair for FMCAD 10

• Lars Birkedal is Co-Organizer for the Dagstuhl Seminar on Modelling, Controlling, and Reasoning about State. http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=10351

• Peter Schneider-Kamp is a PC-Chair of the 11th International Workshop on Termination (WST 2010) http://www.imada.sdu.dk/~petersk/WST2010/

• Ilkka Niemelä is a PC Chair of JELIA 2010 (12th European Conference on Logics in Artificial Intelligence) http://jelia2010.tkk.fi/

• Tayssir TOUILI is a Co-chair of CAV 2010 http://www.liafa.jussieu.fr/~touili/cav2010/

• Barbara Jobstamann is a co-chair for MEMOCODE 2010 http://www-memocode2010.imag.fr/

• Rupak Majumdar is a Program Co-Chair, TACAS 2010 (part of ETAPS 2010) http://tacas10.in.tum.de/

• Eran Yahav is a co-organizer LFX 2010 http://research.ihost.com/lfx2010/

• Eran Yahav is a co-organizer PSY 2010 http://research.ihost.com/psy2010/

• Predrag Janicic is an organizer of the Workshops on Formal and Automated Theorem Proving and Applications FATPA 2010 (http://argo.matf.bg.ac.rs/events/2010/fatpa2010/fatpa2010.html) and FATPA 2011 (http://argo.matf.bg.ac.rs/events/2011/fatpa2011/fatpa2011.html)

• Silvia Ghilezan is a Conference Chair of he 6th Federated Conference on Rewriting, Deduction and Programming - RDP 2011 (http://www.rdp2011.uns.ac.rs)

Joint activities by participants from different institutions to apply for new projects, even not approved yet or even unsuccessful

• A planned Czech-French Barrande project on advanced techniques of symbolic program verification between L. Holik, A. Rogalewicz, and T. Vojnar (FIT BUT, Brno, Czech Republic), T. Touili, P. Habermehl (LIAFA, Paris, France), and R. Iosif (VERIMAG, Grenoble, France).