This is an old revision of the document!


A PCRE internal error occured. This might be caused by a faulty plugin

====== Richmodel Toolkit COST Action Meeting in Tallinn (SVARM 2012) ====== Meeting of the [[http://richmodels.epfl.ch|Rich Model Toolkit]] COST Action IC0901, is organized in Tallinn, Estonia, right after [[http://www.etaps.org/|ETAPS 2012]], in coordination with the [[http://pauillac.inria.fr/~herbelin/aipa2012/index.html|AIPA]] workshop. This is a two day meeting organized in coordination with AIPA where the first day 31st of March 2012 is mainly focusing on the Automation in Proof Assistants topics, while the second day is more focused also on the other IC0901 topics, including additional invited talks, contributed talks from IC0901 Action participants, and informal technical discussion session and our usual MC meeting on 1st of April 2012. ===== Venue ===== Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration, Akadeemia tee 3. ====== Organizers ====== [[http://users.ics.tkk.fi/~kepa|Keijo Heljanko]] and [[http://yquem.inria.fr/~herbelin/index-eng.html|Hugo Herbelin]] are the program organizers. [[http://cs.ioc.ee/~tarmo/|Tarmo Uustalu]] and [[http://ati.ttu.ee/~jaan/|Jaan Raik]] as local organizers on behalf of the IC0901 Action. ===== Preliminary Program ===== ** Sat 31.3 AIPA+SVARM ** * 9:00- 9:30 Philip Ruemmer (Software Verification Using k-Induction) * 9:30-10:00 Cesar Sanchez (A Decision Procedure for Skiplists with Unbounded Height and Length) * 10:00-10:30 Maria Paola Bonacina (Interpolation for resolution, superposition and DPLL(Gamma+T)) * 10:30-11:00 coffee * 11:00-12:00 Jean-Christophe FilliĆ¢tre (Combining Interactive and Automated Theorem Proving in Why3) [invited talk] * 12:00-12:30 Jesper Bengtson (A framework for higher-order separation logic in Coq) * 12:30-14:00 lunch * 14:00-15:00 Jasmin Blanchette (Sharing the Burden of (Dis)proof with Nitpick, Quickcheck, and Sledgehammer) [invited talk] * 15:00-15:30 Corneliu Popeea (Synthesizing Software Verifiers from Proof Rules) * 15:30-16:00 coffee * 16:00-16:30 Tuomas Launiainen (Building a modern concolic tester) * 16:30-17:00 Predrag Janicic (Automated Synthesis of Geometric Construction Procedures) * 17:00-17:30 Fu Song (Efficient CTL Model-Checking for Pushdown Systems) ** Sun 1.4 SVARM ** * 9:00-10:00 Chad E. Brown (Using Satallax to Generate Proof Terms for Conjectures in Coq) [invited talk] * 10:00-10:30 Jasmin Blanchette (TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism) * 10:30-11:00 coffee * 11:00-12:30 **COST action IC0901 Management Committee meeting** * 12:30-14:00 lunch * 14:00-15:00 Serdar Tasiran (Generalizing Reduction and Abstraction to Simplify Concurrent Programs: The QED Approach) [invited talk] * 15:00-15:30 Jean-Francois Raskin (Strategy synthesis for quantitative games) * 15:30-16:00 coffee * 16:00-16:30 Stefan Ratschan (Physical/Software Systems and their Formal Safety Verification) * 16:30-17:00 Julian Samborski-Forlese (Translation of RLTL into Buchi Automata) ** Sun 1.4 AIPA ** * 9:00-10:00 Chad E. Brown (Using Satallax to Generate Proof Terms for Conjectures in Coq) [invited talk] * 10:00-10:30 Jasmin Blanchette (TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism) * 10:30-11:00 coffee * 11:00-12:30 break for COST people to attend action meeting * 12:30-14:00 lunch * 14:00-14:30 Rob Arthan (Now f is continuous (exercise!)) * 14:30-15:00 David Pereira (Deciding Regular Expression (In-)Equivalence in Coq) * 15:00-15:30 Claudio Sacerdoti (Unification in the Matita ITP) * 15:30-16:00 coffee * 16:00-16:30 Pierre Boutillier (Heterogeneous-equality-free compilation of dependent pattern-matching) ===== Registration ===== The **invited IC0901 participants** will be required to register and pay 40 Euros for two lunches and coffees by **9th of March 2012** through a Web based payment system provided by the local organizers: [[https://purchase.ioc.ee/svarm12/|SVARM12 Electronic Payment of Lunch Fees]] These fees can be later claimed from COST as lunch fees. For the invited IC0901 participants there will be no other registration fees, and **NO need to register to AIPA2012 through the ETAPS2012 system** for the two Workshop days. The participants who are **NOT invited IC0901 participants should register to AIPA2012 Workshop through the ETAPS2012 registration**, and pay the ETAPS fees for the two Workshop days. ===== (EXPIRED) Call for Technical Contributions ===== We are planning to have a program including: * contributed talks from Action participants * invited talks from: Chad E. Brown, Jean-Christophe FilliĆ¢tre, Jasmin Blanchette, and Serdar Tasiran * informal technical discussion sessions * our usual MC meeting An informal technical discussion session is meant to be an opportunity to bring up and discuss a topic that is important for our research area, and perceived to be key for the success of our Action. The intention is to encourage us to have some form of technical interaction beyond talks. As examples of such discussions, one may think of technical discussion sessions at project meetings, or technical discussion session at workshops such as SMT, where there is usually such a session on SMT-LIB/SMT-COMP. In order to assemble a program, we need to hear from you! Therefore: (A) If you wish to give a talk, please send title and abstract. Optionally: Mention if you would prefer to be on the first day which is mainly focused on topics related to Automation in Proof Assistants. (B) If you wish to propose a topic for a technical discussion session, please send title and paragraph of motivation, and be prepared to chair, or co-chair, the session you propose. We may help you to find a co-chair, or one of us may co-chair with you, if need be. Please send both kinds of contributions ((A) and (B)) to both addresses <keijo.heljanko@aalto.fi> and <hugo.herbelin@inria.fr> at your earliest convenience, but no later than March 1, 2012 (This deadline is for finalizing the technical program; COST invitations are generated automatically for MC members and you'll receive one sooner.)