- Haskell - Haskell.org

ARiSVe 2013 final call for papers
by Andrei Paskevich 04 Mar '13

04 Mar '13

Call For Papers 1st International Workshop on Automated Reasoning in Software Verification http://arisve2013.lri.fr Monday, June 10, 2013 Lake Placid, NY, USA Affiliated with CADE-24 Aims and Scope The focus of the workshop is application of automated reasoning in the context of software verification, and, more generally, automation in software verification. Relevant topics include but are not limited to: * specifics of verification-related automated reasoning tasks; * efficient translation of high-level verification conditions to logical languages of automated reasoning tools; * handling of the prover's feedback: proofs, models, answer terms; * logical theories of interest for program verification, decision procedures, integration into existing ATP and SMT systems; * combination of automated and user-assisted verification; * tool presentations, tool comparisons, and benchmarks; * experience reports on verification of complex algorithms and real-life software with the use of automated reasoning tools. Paper Submission and Proceedings All submissions are reviewed by the program committee. We expect that one author of every accepted paper will present their work at the workshop. Submissions are limited to 6-12 pages in the LaTeX EasyChair format easychair.cls (http://www.easychair.org/publications/easychair.zip) Technical details may be included in an appendix to be read at the reviewers' discretion. Tool presentation papers and experience reports are welcome. Papers should be submitted through EasyChair, at http://www.easychair.org/conferences/?conf=arisve2013 Submissions must be in PDF format. Electronic version of proceedings will be freely distributed from the workshop web site. Important Dates * Abstract submission deadline: March 8, 2013 * Submission deadline: March 15, 2013 * Notification: April 10, 2013 * Camera ready versions due: May 10, 2013 * Workshop: June 10, 2013 Invited Speaker K. Rustan M. Leino (Microsoft Research) Program Committee * June Andronick (NICTA) * Clark Barrett (New York University) * Ernie Cohen (Microsoft Corp.) * Loïc Correnson (CEA) * Gidon Ernst (Ausburg University) * Jean-Christophe Filliâtre (CNRS), co-chair * Alwyn Goodloe (NASA) * Matthias Horbach (Koblenz University) * Vladimir Klebanov (Karlsruhe Institute of Technology) * Konstantin Korovin (The University of Manchester) * Rosemary Monahan (National University of Ireland) * Andrei Paskevich (Université Paris-Sud), co-chair * Silvio Ranise (Fondazione Bruno Kessler)

1 0

Call for Papers: 10th International Colloquium on Theoretical Aspects of Computing, September 4-6, 2013, Shanghai, China
by Huibiao Zhu 03 Mar '13

03 Mar '13

*************************************************************** ICTAC 2013 10th International Colloquium on Theoretical Aspects of Computing *** Call For Papers *** September 4-6, 2013 Shanghai, China http://ictac2013.ecnu.edu.cn/ *************************************************************** ICTAC 2013 is the 10th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC 2013 will bring together practitioners and researchers from academia, industry and government to present research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development. The other main purpose is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries, as in the mandate of the United Nations University. THEMES AND TOPICS OF PAPERS ICTAC 2013 calls for regular research papers on theories of computation and programming, foundations of software engineering, and on formal techniques in software design and verification; short papers on recent work or proposals of challenges in new programming paradigms such as Cyber-Physical Systems, Cloud Computing and Social Networks; and papers about tools that support formal techniques for software modeling, system design and verification. The topical areas of the conference include, but not limited to Automata theory and formal languages; Principles and semantics of programming languages; Theories of concurrency, mobility and reconfiguration; Logics and their applications; Software architectures and their models, refinement and verification; Relationship between software requirements, models and code; Program static and dynamic analysis and verification; Software specification, refinement, verification and testing; Model checking and theorem proving; Models of object and component systems; Coordination and feature interaction; Integration of theories, formal methods and tools for engineering computing systems; Service-oriented architectures: models and development methods; Models of concurrency, security, and mobility; Theory of distributed, grid and cloud computing; Real-time, embedded, hybrid and cyber-physical systems; Type and category theory in computer science; Models for learning and education; Case studies, theories, tools and experiments of verified systems; Domain-specific modeling and technology: examples, frameworks and experience. Challenges and foundations in the environmental modeling and monitoring, healthcare, and disaster management. PUBLICATION AND SUBMISSION As for the past editions, it is the plan that the proceedings of ICTAC 2013 will be published by Springer in the series Lecture Notes in Computer Science (LNCS) and will be available at the colloquium. A special issue of a journal with extended version of selected papers from ICTAC 2013 is under negotiation. Submissions to the colloquium must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the conference. Submissions can be Regular Papers, Short Papers or Tool Papers. Short papers can present recent or ongoing work or discuss new ideas which are at an early stage of development and have not been thoroughly evaluated yet. Papers should be written in English. Regular Papers should not exceed 18 pages and Short Papers and tool papers should be between 5 and 10 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Papers must be submitted at http://www.easychair.org/conferences/?conf=ictac2013. Short papers and tool papers must contain clear reference to the background theories and techniques; and a tool paper must further provide a link to a webpage that contains a tutorial and demo of the tool. All queries should be sent to the e-mail address ictac2013(a)sei.ecnu.edu.cn. IMPORTANT DATES Paper submission deadline: 8 March 2013 Paper Accept/Reject Notification: 26 Apr 2013 Final paper submission: 17 May 2013 Conference dates: 4 --- 6 September 2013 ASSOCIATED EVENTS Festschrift Symposium in Honor of Prof. Jifeng He: 01-03 September 2013 Summer School on Software Engineering: 26-30 August 2013 INVITED SPEAKERS Luca Cardelli, Microsoft Research Cambridge, UK Jifeng He, East China Normal University, China Marta Kwiatkowska, University of Oxford, UK CONFERENCE CHAIRS Zhou Chaochen, Software Institute, Chinese Academy of Sciences, China Peter Haddawy, UNU-IIST, Macau SAR, China Bill Roscoe, University of Oxford, UK PROGRAMME CHAIRS Zhiming Liu, UNU-IIST, Macau SAR, China Jim Woodcock, University of York, UK Huibiao Zhu, East China Normal University, China PROGRAMME COMMITTEE Farhad Arbab (CWI and Leiden University, The Netherlands) Michael Butler (University of Southampton, UK) Ana Cavalcanti (University of York, UK) Zhenbang Chen (National University of Defense Technology, China) Van Hung Dang (University of Engineering and Technology, Vietnam) Thao Dang (VERIMAG, France) David Deharbe (Universidade Federal do Rio Grande do Norte, Brasil) Jinsong Dong (National University of Singapore, Singapore) Meenakshi Dsouza (IIIT, India) Zhenhua Duan (Xidian University, China) John Fitzgerald (Newcastle University, UK) Martin Fraenzle (Carl von Ossietzky University Oldenburg, Germany) Marcelo Frias (Instituto Tecnologico Buenos Aires, Argentina) Lindsay Groves (Victoria University of Wellington, New Zealand) Kim Guldstrand Larsen (Aalborg University, Denmark) Ian J. Hayes (University of Queensland, Australia) Zhenjiang Hu (NII, Japan) Lei Ju (Shandong University, China) Daniel Kroening (Oxford University, UK) Martin Leucker (University of Lübeck, Germany) Zhiming Liu (UNU-IIST, Macau SAR, China) Annabelle Mciver (Macquarie University, Australia) Dominique Mery (Université de Lorraine, France) Tobias Nipkow (Technische Universit?t München, Germany) Paritosh Pandya (TIFR, India) Jun Pang (University of Luxembourg, Luxembourg) Geguang Pu (East China Normal University, China) Shengchao Qin (Teesside University, UK) Zongyan Qiu (Peking University, China) Abhik Roychoudhury (National University of Singapore, Singapore) Augusto Sampaio (Federal university of Pernambuco, Brasil) Ondrej Sery (University of Lugano, Switzerland) Natarajan Shankar (SRI, US) Marjan Sirjani (Reykjavik University, Iceland) Andrzej Tarlecki (Warsaw University, Poland) Mark Utting (The University of Waikato, New Zealand) Tarmo Uustalu (Tallinn University of Technology, Estonia) Farn Wang (National Taiwan University, Taiwan) Burkhart Wolff (University Paris-Sud, France) Jim Woodcock (University of York, UK) Wang Yi (Uppsala University, Sweden) Naijun Zhan (Chinese Academy of Sciences, China) Jianjun Zhao (Shanghai Jiao Tong University, China) Jianhua Zhao (Nanjing University, China) Huibiao Zhu (East China Normal University, China)

1 0

Haskell Weekly News: Issue 260
by Daniel Santa Cruz 01 Mar '13

01 Mar '13

Welcome to issue 260 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers the week of February 17 to 23, 2013. Quotes of the Week * danharaj: zygohistobfuscatory maintainomorphism * merijn: after a week you can delete 80% of your code and replace it with whatever edwardk wrote that day ;-) * merijn: If Oleg is the unit of type hackery I propose Edward as the unit of haskell productivity. * edwardk: the merijn is the unit for the number of distinct units you've named * elliott: If you encounter an edwardk in the wild: nod reassuringly when he talks about something you understand. Under NO circumstances EVER give your GitHub account name Top Reddit Stories * An awesome Haskell Valentines card, from my non-programmer girlfriend. Domain: i.imgur.com, Score: 127, Comments: 32 On Reddit: [1] http://goo.gl/5Cxwr Original: [2] http://goo.gl/BeksW * Announcing SmallCheck 1.0 Domain: ro-che.info, Score: 61, Comments: 16 On Reddit: [3] http://goo.gl/R0gvO Original: [4] http://goo.gl/7b5Dq * Intro to FRP and purely functional games: live-coding the basics of Mario in ~30 lines in Elm [video] Domain: ustream.tv, Score: 50, Comments: 12 On Reddit: [5] http://goo.gl/E22PW Original: [6] http://goo.gl/q7r8e * Reflections After a Hard Day in Haskell GUI Land Domain: fluffynukeit.com, Score: 49, Comments: 53 On Reddit: [7] http://goo.gl/xQv8i Original: [8] http://goo.gl/0hvT6 * Duncan Coutts on Parallelism and Concurrency with Haskell, Distributed Programming with Cloud Haskell Domain: infoq.com, Score: 44, Comments: 5 On Reddit: [9] http://goo.gl/jU9EH Original: [10] http://goo.gl/UkRDk * A Game of Type-Safe Tic-Tac-Toe Domain: github.com, Score: 42, Comments: 20 On Reddit: [11] http://goo.gl/SrIEx Original: [12] http://goo.gl/dFIyd * The Algebra of Algebraic Data Types, Part 3 Domain: chris-taylor.github.com, Score: 36, Comments: 7 On Reddit: [13] http://goo.gl/NQI8S Original: [14] http://goo.gl/CPkiV * Write Yourself a Haskell... in Lisp Domain: gergo.erdi.hu, Score: 36, Comments: 3 On Reddit: [15] http://goo.gl/YqdSl Original: [16] http://goo.gl/E3yzO * Overloading record fields with Lens Domain: statusfailed.com, Score: 31, Comments: 19 On Reddit: [17] http://goo.gl/oF7zN Original: [18] http://goo.gl/SOEz4 * On partial functions in Idris Domain: edwinb.wordpress.com, Score: 29, Comments: 3 On Reddit: [19] http://goo.gl/0HquS Original: [20] http://goo.gl/OaO2r * Who's using Haskell commercially? New collection of real-world case studies from FP Complete. Domain: fpcomplete.com, Score: 26, Comments: 12 On Reddit: [21] http://goo.gl/IM2rb Original: [22] http://goo.gl/zsf4c * Making 'Super Nario Bros.' in Haskell Domain: youtube.com, Score: 26, Comments: 11 On Reddit: [23] http://goo.gl/2Hg7o Original: [24] http://goo.gl/9Bb5t Top StackOverflow Questions * Why is there no implicit parallelism in Haskell? votes: 29, answers: 4 Read on SO: [25] http://goo.gl/n6VkF * Why is (a,b,c,d) not sugar for (a,(b,(c,(d,()))))? votes: 26, answers: 2 Read on SO: [26] http://goo.gl/aW6K2 * How can I understand “(.) . (.)”? votes: 21, answers: 5 Read on SO: [27] http://goo.gl/kqbcO * Are there any advantages of using Rank2Types in favor of RankNTypes? votes: 18, answers: 2 Read on SO: [28] http://goo.gl/V5naQ * What's the closest thing to Haskell's typeclasses in OCaml? votes: 16, answers: 4 Read on SO: [29] http://goo.gl/AWvgl * Why does ghci give me a type for “1 ++ 2” instead of ragequitting? votes: 16, answers: 2 Read on SO: [30] http://goo.gl/66Pti * Is (>>) supposed to discard all left-side output? votes: 11, answers: 2 Read on SO: [31] http://goo.gl/wvnLJ * Find inferred type for local function votes: 11, answers: 3 Read on SO: [32] http://goo.gl/WFCz1 * STUArray s i e - space leak only when i == Int? votes: 11, answers: 2 Read on SO: [33] http://goo.gl/fbyPE * Connecting to the System GHC votes: 10, answers: 1 Read on SO: [34] http://goo.gl/FGVN5 * Correctness of implicit lifting votes: 10, answers: 2 Read on SO: [35] http://goo.gl/5s8pR Until next time, +Daniel Santa Cruz References 1. http://i.imgur.com/P0d7v7z.jpg 2. http://www.reddit.com/r/haskell/comments/18q510/an_awesome_haskell_valentin… 3. http://ro-che.info/articles/2013-02-19-smallcheck.html 4. http://www.reddit.com/r/haskell/comments/18uhfy/announcing_smallcheck_10/ 5. http://www.ustream.tv/recorded/29330499 6. http://www.reddit.com/r/haskell/comments/190n1t/intro_to_frp_and_purely_fun… 7. http://fluffynukeit.com/2013/02/reflections-after-a-hard-day-in-haskell-gui… 8. http://www.reddit.com/r/haskell/comments/18p0nu/reflections_after_a_hard_da… 9. http://www.infoq.com/interviews/coutts-haskell 10. http://www.reddit.com/r/haskell/comments/18zvk2/duncan_coutts_on_parallelis… 11. https://github.com/leonidas/codeblog/blob/master/2013/2013-02-19-typesafe-t… 12. http://www.reddit.com/r/haskell/comments/18tys6/a_game_of_typesafe_tictacto… 13. http://chris-taylor.github.com/blog/2013/02/13/the-algebra-of-algebraic-dat… 14. http://www.reddit.com/r/haskell/comments/18p3p5/the_algebra_of_algebraic_da… 15. http://gergo.erdi.hu/blog/2013-02-17-write_yourself_a_haskell..._in_lisp/ 16. http://www.reddit.com/r/haskell/comments/18pm7r/write_yourself_a_haskell_in… 17. http://statusfailed.com/blog/2013/02/19/overloading-record-fields-with-lens… 18. http://www.reddit.com/r/haskell/comments/18t2n7/overloading_record_fields_w… 19. http://edwinb.wordpress.com/2013/02/19/on-partial-functions-in-idris/ 20. http://www.reddit.com/r/haskell/comments/18tbkj/on_partial_functions_in_idr… 21. http://fpcomplete.com/announcing-case-studies/ 22. http://www.reddit.com/r/haskell/comments/18p5n4/whos_using_haskell_commerci… 23. http://www.youtube.com/watch?v=gVLFGQGRsDw 24. http://www.reddit.com/r/haskell/comments/18v4ep/making_super_nario_bros_in_… 25. http://stackoverflow.com/questions/15005670/why-is-there-no-implicit-parall… 26. http://stackoverflow.com/questions/14973459/why-is-a-b-c-d-not-sugar-for-a-… 27. http://stackoverflow.com/questions/15029843/how-can-i-understand 28. http://stackoverflow.com/questions/15020428/are-there-any-advantages-of-usi… 29. http://stackoverflow.com/questions/14934242/whats-the-closest-thing-to-hask… 30. http://stackoverflow.com/questions/15041581/why-does-ghci-give-me-a-type-fo… 31. http://stackoverflow.com/questions/14953032/is-supposed-to-discard-all-left… 32. http://stackoverflow.com/questions/15034392/find-inferred-type-for-local-fu… 33. http://stackoverflow.com/questions/15038386/stuarray-s-i-e-space-leak-only-… 34. http://stackoverflow.com/questions/14918453/connecting-to-the-system-ghc 35. http://stackoverflow.com/questions/14928302/correctness-of-implicit-lifting 36. https://plus.google.com/105107667630152149014/about

1 0

SLE 2013 - Call for Papers
by Martin Erwig 27 Feb '13

27 Feb '13

======================================================================== CALL FOR PAPERS 6th International Conference on Software Language Engineering (SLE 2013) Oct 26-28, 2013, Indianapolis, IN, USA (Co-located with SPLASH 2013 and GPCE 2013) General chair: Eric Van Wyk, University of Minnesota, USA Program co-chairs: Martin Erwig, Oregon State University, USA Richard Paige, University of York, UK Keynote speaker: Don Batory, University of Austin, USA http://planet-sl.org/sle2013 ======================================================================== IMPORTANT DATES Deadline for abstracts: June 7, 2013 (Midnight UTC-8, Pacific Standard Time) Deadline for full papers: June 14, 2013 (Midnight UTC-8, Pacific Standard Time) Notification to authors: August 3, 2013 Camera-ready copies due: August 16, 2013 Conference: October 26 -28, 2013 TYPES OF SUBMISSIONS We solicit the following types of papers: - Research papers: These should report a substantial research contribution to SLE or successful application of SLE techniques or both. Full paper submissions must not exceed 20 pages (in LNCS format). - Industrial experience papers: These papers discuss practical applications of SLE technology with an emphasis on the advantages and disadvantages of the method, techniques, or tools used. These papers must not exceed 10 pages (in LNCS format). - Tool demonstration papers: Because of SLE's ample interest in tools, we seek papers that present software tools related to the field of SLE. These papers will accompany a tool demonstration to be given at the conference. These papers must not exceed 10 pages (in LNCS format). The selection criteria include the originality of the tool, its innovative aspects, the relevance of the tool to SLE, and the maturity of the tool. Papers are submitted via the Easychair system: https://www.easychair.org/conferences/?conf=sle2013 SCOPE The term "software language" refers to artificial languages used in software development. These include general-purpose programming languages, domain-specific languages, modeling and metamodeling languages, data models and ontologies. Examples include general purpose modeling languages such as SysML and UML, metamodeling frameworks such as Ecore, MOF or GOPRR, domain-specific modeling languages for business process modeling, such as BPMN, or embedded systems, such as Simulink or Modelica, and specialized XML-based and OWL-based languages and vocabularies. The term "software language" is intentionally broad; besides the above categories and examples, it also encompasses implicit approaches to language definition, such as APIs and collections of design patterns. Software language engineering is the application of systematic, disciplined, and measurable approaches to the development (design, implementation, testing, deployment), use, deployment, and maintenance (evolution, recovery, and retirement) of these languages. Of special interest are (1) formal descriptions of languages that are used to design or generate language-based tools and (2) methods and tools for managing such descriptions, including modularization, refactoring, refinement, composition, versioning, co-evolution, recovery, and analysis. TOPICS OF INTEREST We solicit high-quality contributions in the area of SLE ranging from theoretical and conceptual contributions to tools, techniques, and frameworks that support the aforementioned lifecycle activities. The topics of interest include, but are not limited to the following: - Formalisms used in designing and specifying languages, and tools that analyze language descriptions - Language implementation techniques: compiler generator tools, attribute grammar systems, term-rewriting systems, functional programming-based combinator libraries; metamodel-based and ontology tools implementing constraint, rule, view, transformation, and query formalisms and engines. - Transformations and transformation languages, as well as program and model transformation tools, and approaches for mapping between ontologies. - Language evolution: Included are extensible languages and type systems and their supporting tools and language conversion tools, approaches for ontology evolution, approaches for impact analysis of language evolution. - Approaches to the elicitation, specification, and verification of requirements for software languages: Examples include the use of requirements engineering techniques in domain engineering and in the development of domain-specific languages and the application of logic-based formalisms for verifying language and domain requirements. - Language development frameworks, methodologies, techniques, best practices, and tools for the broader language lifecycle covering phases such as analysis, testing, and documentation. For example, frameworks for advanced type or reasoning systems, constraint mechanisms, tools for metrics collection and language usage analysis, assessing language usability, documentation generators, visualization backends, generation of tests for language-based tools, knowledge and process management approaches, as well as IDE support for many of these activities are of interest. - Integration and interoperation between different approaches to software language engineering; for example, ways to integrate grammar-based and ontology-based approaches to language definition. - Design challenges in SLE: Example challenges include finding a balance between specificity and generality in designing domain-specific languages, between strong static typing and weaker yet more flexible type systems, or between deep and shallow embedding approaches, as, for example, in the context of adding type-safe XML and database programming support to general-purpose programming languages. - Applications of languages including innovative domain-specific languages or "little" languages: Examples include policy languages for security or service-oriented architectures, web-engineering with schema-based generators or ontology-based annotations. Of specific interest are the engineering aspects of domain-specific language support in all of these cases. The program committee chairs encourage potential contributors to contact them with questions about the scope and topics of interest of SLE. The overall principle of SLE is to be broad-minded and inclusive about relevance and scope, and to invest in community building when soliciting and selecting papers. PROGRAM COMMITTEE Emilie Balland, INRIA, France Olaf Chitil, University of Kent, UK James R. Cordy, Queen's University, Canada Davide Di Ruscio, Università degli Studi dell'Aquila, Italy Iavor Diatchki, Galois Inc., USA Anne Etien, LIFL - University of Lille 1, Fance Jean-Marie Favre, University of Grenoble, Fance Dragan Gasevic, Athabasca University, Canada Andy Gill, University of Kansas, USA Jeremy Gibbons, University of Oxford, UK Jeff Gray, University of Alabama, USA Giancarlo Guizzardi, Federal University of Espirito Santo, Brazil Gorel Hedin, Lund University, Sweden Markus Herrmannsdoerfer, Technische Universität München, Germany Zhenjiang Hu, NII, Japan Oleg Kiselyov, USA Paul Klint, Centrum Wiskunde & Informatica, The Netherlands Thomas Kuehne, Victoria University of Wellington, New Zealand Kim Mens, UC Louvain, Belgium Pierre-Etienne Moreau, Ecole des Mines Nancy, France Klaus Ostermann, Marburg University, Germany Arnd Poetzsch-Heffter, University of Kaiserslautern, Germany Fiona Polack, Dept of Computer Science, University of York, UK Lukas Renggli, University of Bern, Switzerland Bernhard Rumpe, RWTH Aachen University, Germany João Saraiva, Universidade do Minho, Portugal Friedrich Steimann, Fernuniversität in Hagen, Germany Gabriele Taentzer, Marburg University, Germany Mark Van Den Brand, TU/e, The Netherlands Jurgen Vinju, Centrum Wiskunde & Informatica, The Netherlands

1 0

AI4FM 2013 : First Call For Papers (ITP 2013 workshop)
by Grov, Gudmund 22 Feb '13

22 Feb '13

Apologies for multiple copies ---------------------------------------------------- AI4FM 2013 - the 4th International Workshop on the use of AI in Formal Methods http://www.ai4fm.org/ai4fm-2013/ Rennes, France, 22nd July, 2013 In association with ITP 2013 ---------------------------------------------------- --- First Call for Papers --- General ------- This workshop will bring together researchers from formal methods and AI; it will address the issue of how AI can be used to support the formal software development process, including modelling and proof. Previous AI4FM workshops have included a mix of industrial and academic participants and we anticipate attracting a similarly diverse audience. Industrial use of formal methods is certainly increasing but, in order to make it more mainstream, the cost of applying formal methods, in terms of mathematical skill level and development time, must be reduced - we believe that AI can help with these issues. Rigorous software development using formal methods allows the construction of an accurate characterisation of a problem domain that is firmly based on mathematics; by applying standard mathematical analyses, these methods can be used to prove that systems satisfy formal specifications. A recent ACM computing survey paper describes over sixty industrial projects and discusses the effect formal methods have on time, cost and quality. It shows that with tools backed by mature theory, formal methods are becoming cost effective and their use is easier to justify, not as an academic exercise or legal requirement, but as part of a business case. Furthermore, the use of such formal methods is no longer confined to safety critical systems: the list of industrial partners in the EU-funded DEPLOY project is one indication of this broader use. Most methods tend to fit a ``posit-and-prove'' paradigm where the user posits a development step (expressed in terms of specifications of yet-to-be-realised components) that has to be justified by proofs. The associated properties that must be verified are often called proof obligations (POs) or verification conditions. In most cases, such proofs require mechanical support by theorem provers. One can distinguish between automatic and interactive provers, where the latter are generally more expressive but require user interaction. AI has had a large impact on the development of provers. In fact, some of the first AI applications were in theorem proving and all theorem provers now contain heuristics to reduce the search space that can be attributed to AI. Nevertheless, theorem proving research and (pure) AI research have diverged and theorem proving is barely considered to be AI-related anymore. Scope ----- We encourage submissions presenting work in progress, tools under development, and PhD projects, in order that the workshop can become a forum for active dialogue between the groups involved in theorem provers, formal methods and artificial intelligence. Particular areas of interest include, but are not limited to: * The use of machine learning to support interactive theorem proving; * The use of machine learning to enhance automated theorem proving; * The development of search heuristics; * The us of AI for term synthesis, invariant generation, lemma discovery and concept invention; * The use of AI for counter-example generation; * The use of AI to support and guide the formal modelling process; * The role of AI planning for formal systems developments, from requirements to the end product (including software and hardware); * The interplay between reasoning and modelling and the role of AI in this framework; * Ontologies in the formal engineering process. Submission ---------- The main aim for the workshop is discussion, thus submissions do not need to be original. Extended versions of submissions may have been published previously, or submitted concurrently with or after AI4FM 2013 to another workshop, conference or a journal. Submission is by email to: ai4fm2013(a)ai4fm.org Please submit an abstract up to 3 pages in a PDF format. The extended abstracts will be handed out to all participants, and will be made into a technical report prior to the workshop. Acceptance for presentation at the workshop will be made by the organisers based on relevance to the workshop. Important Dates --------------- Submission deadline: April 20, 2013 Notification of acceptance: May 01, 2013 Final version due: May 15, 2013 Workshop: July 22nd, 2013 Organisers ----------------- * Leo Freitas (Newcastle University, UK) * Gudmund Grov (Heriot-Watt University, UK) * Ewen Maclean (University of Edinburgh, UK) Contact Details ---------------- If you have any queries, please email the organisers at the following email address: ai4fm2013(a)ai4fm.org ----- Sunday Times Scottish University of the Year 2011-2013 Top in the UK for student experience Fourth university in the UK and top in Scotland (National Student Survey 2012) We invite research leaders and ambitious early career researchers to join us in leading and driving research in key inter-disciplinary themes. Please see www.hw.ac.uk/researchleaders for further information and how to apply. Heriot-Watt University is a Scottish charity registered under charity number SC000278.

1 0

PhD Studentship in Nottingham
by Graham Hutton 21 Feb '13

21 Feb '13

Dear all, The School of Computer Science at the University of Nottingham is currently advertising a PhD position on applying functional programming techniques to optimisation problems: http://www.cs.nott.ac.uk/~ajp/PhD-opportunities.htm This would be a great position for someone who is interested in applying FP ideas to real-world problems. The closing date for applications is 28th February 2013. If you have any queries about the position, please contact Andrew Parkes <andrew.parkes(a)nottingham.ac.uk>. Best wishes, Graham -- Prof Graham Hutton Functional Programming Lab School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~gmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

1 0

Haskell Weekly News: Issue 259
by Daniel Santa Cruz 21 Feb '13

21 Feb '13

Welcome to issue 259 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers the week of February 10 to 16, 2013. Quotes of the Week * frerich: i thought endo is where the ewoks live * edwardk: on the other hand i also write excessively polymorphic code Top Reddit Stories * Comonads are objects Domain: haskellforall.com, Score: 105, Comments: 86 On Reddit: [1] http://goo.gl/ssFWD Original: [2] http://goo.gl/ADN3k * GHC HEAD now has OverloadedLists as an extension - allowing you to more easily specify literal Maps, Text, Vector, ByteString etc values. Domain: hackage.haskell.org, Score: 86, Comments: 66 On Reddit: [3] http://goo.gl/tVmBE Original: [4] http://goo.gl/m08GR * GHC HEAD: new parallel I/O manager merged Domain: haskell.org, Score: 67, Comments: 39 On Reddit: [5] http://goo.gl/HX04c Original: [6] http://goo.gl/j8AaN * The Algebra of Algebraic Data Types (Part I) Domain: chris-taylor.github.com, Score: 51, Comments: 23 On Reddit: [7] http://goo.gl/9WjrL Original: [8] http://goo.gl/Jyco0 * deprecation rage :: hpaste Domain: hpaste.org, Score: 49, Comments: 9 On Reddit: [9] http://goo.gl/ycHWD Original: [10] http://goo.gl/KAdsV * Github incorrectly recognizes haskell code as perl thus making language usage studies based on github useless. Domain: github.com, Score: 45, Comments: 45 On Reddit: [11] http://goo.gl/WQN38 Original: [12] http://goo.gl/jfpeH * StackOverflow [haskell] hits 10k questions! Domain: imgur.com, Score: 41, Comments: 31 On Reddit: [13] http://goo.gl/znqwX Original: [14] http://goo.gl/cdm3C * Don Stewart provides a great concise overview of the many areas of Haskell performance analysis Domain: stackoverflow.com, Score: 39, Comments: 1 On Reddit: [15] http://goo.gl/W9AOL Original: [16] http://goo.gl/nC6Mk * The Algebra of Algebraic Data Types, Part 2 Domain: chris-taylor.github.com, Score: 37, Comments: 9 On Reddit: [17] http://goo.gl/VHUjp Original: [18] http://goo.gl/mk95s * Upcoming conduit 1.0 & comparison to pipes & io-streams Domain: yesodweb.com, Score: 32, Comments: 11 On Reddit: [19] http://goo.gl/dbnpi Original: [20] http://goo.gl/8RHfb * Library: A collection of tools for processing PDF files in Haskell Domain: github.com, Score: 31, Comments: 38 On Reddit: [21] http://goo.gl/BtpFw Original: [22] http://goo.gl/loL4n * Introduction to Haskell, Lecture 5 is Live (Creating Data Types) Domain: shuklan.com, Score: 29, Comments: 2 On Reddit: [23] http://goo.gl/h2q3G Original: [24] http://goo.gl/ASx0B * FP Complete Hiring for Haskell evangelist / customer and community relations advocate Domain: haskellers.com, Score: 28, Comments: 0 On Reddit: [25] http://goo.gl/g2nic Original: [26] http://goo.gl/di728 * Quick and Easy DSLs with Writer Endo Domain: ocharles.org.uk, Score: 22, Comments: 17 On Reddit: [27] http://goo.gl/6p43B Original: [28] http://goo.gl/p8aX4 Top StackOverflow Questions * Least-strict (*) votes: 17, answers: 2 Read on SO: [29] http://goo.gl/tHzUf * Referential transparency with polymorphism in Haskell votes: 14, answers: 1 Read on SO: [30] http://goo.gl/PyBgK * Truncating to Word type votes: 11, answers: 1 Read on SO: [31] http://goo.gl/C4wwu * Is there a generalization of these Free-like constructions? votes: 11, answers: 0 Read on SO: [32] http://goo.gl/WLb7S * How fast is Data.Sequence.Seq compared to []? votes: 9, answers: 1 Read on SO: [33] http://goo.gl/d0x2d * Does FreeT keep the equational reasoning benefits of Free? votes: 9, answers: 1 Read on SO: [34] http://goo.gl/7vu37 * Understanding recursion in Haskell votes: 7, answers: 5 Read on SO: [35] http://goo.gl/I2SBM * What laws are the standard Haskell type classes expected to uphold? votes: 7, answers: 2 Read on SO: [36] http://goo.gl/FqQ5J * What does (== “ ”) mean, in Haskell? votes: 7, answers: 4 Read on SO: [37] http://goo.gl/EecMz * Linking separate projects in GHC votes: 7, answers: 1 Read on SO: [38] http://goo.gl/ZjVao * What are structures with “subtraction” but no inverse? votes: 7, answers: 1 Read on SO: [39] http://goo.gl/SaQ66 Until next time, +Daniel Santa Cruz References 1. http://www.haskellforall.com/2013/02/you-could-have-invented-comonads.html 2. http://www.reddit.com/r/haskell/comments/18isiu/comonads_are_objects/ 3. http://hackage.haskell.org/trac/ghc/wiki/OverloadedLists 4. http://www.reddit.com/r/haskell/comments/18ncub/ghc_head_now_has_overloaded… 5. http://www.haskell.org/pipermail/ghc-devs/2013-February/000414.html 6. http://www.reddit.com/r/haskell/comments/18d81l/ghc_head_new_parallel_io_ma… 7. http://chris-taylor.github.com/blog/2013/02/10/the-algebra-of-algebraic-dat… 8. http://www.reddit.com/r/haskell/comments/18902u/the_algebra_of_algebraic_da… 9. http://hpaste.org/82331 10. http://www.reddit.com/r/haskell/comments/18hnh3/deprecation_rage_hpaste/ 11. https://github.com/timthelion?tab=repositories 12. http://www.reddit.com/r/haskell/comments/189cti/github_incorrectly_recogniz… 13. http://imgur.com/Wtx1kT4 14. http://www.reddit.com/r/haskell/comments/18kwe2/stackoverflow_haskell_hits_… 15. http://stackoverflow.com/a/3276557/74497 16. http://www.reddit.com/r/haskell/comments/18jkvw/don_stewart_provides_a_grea… 17. http://chris-taylor.github.com/blog/2013/02/11/the-algebra-of-algebraic-dat… 18. http://www.reddit.com/r/haskell/comments/18bqth/the_algebra_of_algebraic_da… 19. http://www.yesodweb.com/blog/2013/02/upcoming-conduit-1-0 20. http://www.reddit.com/r/haskell/comments/18iskd/upcoming_conduit_10_compari… 21. https://github.com/Yuras/pdf-toolbox 22. http://www.reddit.com/r/haskell/comments/18n0l1/library_a_collection_of_too… 23. http://shuklan.com/haskell/lec05.html 24. http://www.reddit.com/r/haskell/comments/18e0vn/introduction_to_haskell_lec… 25. http://www.haskellers.com/jobs/25 26. http://www.reddit.com/r/haskell/comments/18b37b/fp_complete_hiring_for_hask… 27. http://ocharles.org.uk/blog/posts/2013-02-12-quick-dsls-with-endo-writers.h… 28. http://www.reddit.com/r/haskell/comments/18dhwf/quick_and_easy_dsls_with_wr… 29. http://stackoverflow.com/questions/14906261/least-strict 30. http://stackoverflow.com/questions/14865734/referential-transparency-with-p… 31. http://stackoverflow.com/questions/14820699/truncating-to-word-type 32. http://stackoverflow.com/questions/14852712/is-there-a-generalization-of-th… 33. http://stackoverflow.com/questions/14798613/how-fast-is-data-sequence-seq-c… 34. http://stackoverflow.com/questions/14907510/does-freet-keep-the-equational-… 35. http://stackoverflow.com/questions/14820138/understanding-recursion-in-hask… 36. http://stackoverflow.com/questions/14861379/what-laws-are-the-standard-hask… 37. http://stackoverflow.com/questions/14865442/what-does-mean-in-haskell 38. http://stackoverflow.com/questions/14884561/linking-separate-projects-in-ghc 39. http://stackoverflow.com/questions/14913904/what-are-structures-with-subtra…

1 0

CFP: 10th CHR Workshop in Berlin, July 2013
by Jon Sneyers 20 Feb '13

20 Feb '13

========================================================================= Call for Papers Tenth International Workshop on Constraint Handling Rules CHR 2013 http://dtai.cs.kuleuven.be/CHR/CHR2013/ Berlin (Germany), July 11-12th, 2013 (co-located with the 3rd Intl Summer School on CHR) ========================================================================= Introduction The CHR 2013 Workshop will be held on July 11th and 12th, 2013 in Berlin (Germany) at the occasion of the 3rd International Summer School on CHR. More information on the venue and the co-located summer school can be found on the summer school website (http://met.guc.edu.eg/CHR2013/) The Constraint Handling Rules (CHR) language has become a major declara- tive specification formalism and implementation language for constraint reasoning algorithms and applications. Algorithms specified using infe- rence rules, rewrite rules, sequents, proof rules, or logical axioms can often be directly written in CHR. Its clean semantics facilitates pro- gram design, analysis, and transformation. For more information, please visit the CHR website (http://dtai.cs.kuleuven.be/CHR/) The aim of the CHR workshop series is to stimulate and promote interna- tional research and collaboration on topics related to the CHR language. The workshop is a lively, friendly forum for presenting and discussing new results, interesting applications, and work in progress. Previous Workshops on Constraint Handling Rules were organized in 2004 in Ulm (Germany), in 2005 in Sitges (Spain) at ICLP, in 2006 in Venice (Italy) at ICALP, in 2007 in Porto (Portugal) at ICLP, in 2008 in Hagen- berg (Austria) at RTA, in 2009 in Pasadena (California, US) at ICLP, in 2010 in Edinburgh (Scotland, UK) at ICLP, in 2011 in Cairo (Egypt), at the 2nd CHR summer school, and in 2012 in Budapest (Hungary) at ICLP. Topics of Interest The workshop calls for full papers and short papers describing ongoing work on any aspect of CHR and related approaches. The following topics are relevant (this list is non-exhaustive): - (Logical) Algorithms - Applications - Constraint Solvers - Critical Assessment - Expressiveness and Complexity - Implementations and Optimization - Language Extensions (Types, Modules,...) - Mutual inspiration from related areas such as Answer Set Programming, (Term) Rewriting Systems, ... - Program Analysis - Program Transformation and Generation - Programming Environments (Debugging) - Programming Pearls - Programming Tools - Retractable Constraints - Semantics - System Descriptions Important dates - Paper submission deadline: May 8th, 2013 - Notification of acceptance: June 8th, 2013 - Final version due: June 23rd, 2013 - Workshop date: July 11th and 12th, 2013 Submission Information The two categories for submissions are: - full papers for describing technically sound, innovative ideas that can advance the state of the art of CHR; - short papers, for ongoing work not yet ready for full publication and research project overviews. All papers must describe original, previously unpublished research, and must not simultaneously be submitted for publication elsewhere. They must be written in English. Technical papers must not exceed 15 pages. The limit for short papers is 8 pages, as is the standard page limit for application papers, and system and tool papers. However, particularly strong contributions in the latter two areas may be submitted as technical paper as well. All papers must be in the Springer LNCS format. General information about the Springer LNCS series and the LNCS authors' instructions are available at the Springer LNCS home page (http://www.springer.com/computer/lncs?SGWID=0-164-7-72376-0) Submissions must be made via the EasyChair submission system, available at http://www.easychair.org/conferences/?conf=chr2013 Programme Committee - Slim Abdennadher, German University of Cairo, Egypt - María Alpuente, UPV, Spain - Henning Christiansen, Roskilde University, Denmark (co-chair) - Marina De Vos, University of Bath, UK - François Fages, INRIA Rocquencourt, France - Thom Frühwirth, University of Ulm, Germany - Maurizio Gabbrielli, University of Bologna, Italy - Marco Gavanelli, University of Ferrara, Italy - Rémy Haemmerlé, Technical University of Madrid, Spain - Michael Maher, University of New South Wales, Canberra, Australia - Thierry Martinez, INRIA Paris-Rocquencourt, France - Maria Chiara Meo, Gabriele d'Annunzio University, Italy - Eric Monfroy, UTFSM and LINA, Chile/France - Tom Schrijvers, Ghent University, Belgium - Jon Sneyers, KU Leuven, Belgium (co-chair) - Armin Wolf, Fraunhofer FIRST, Germany Workshop Coordinators Contact: chr2013(a)easychair.org Henning Christiansen Department of Communication, Business and Information Technologies, Roskilde University, Denmark http://www.ruc.dk/~henning/ Jon Sneyers Department of Computer Science, KU Leuven Leuven, Belgium http://people.cs.kuleuven.be/~jon.sneyers/ Steering committee: Thom Frühwirth Programmiermethodik und Compilerbau, Ulm University Ulm, Germany http://www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/ Slim Abdennadher Department of Computer Science & Engineering, German University in Cairo Cairo, Egypt http://met.guc.edu.eg/staff/slim_abdennadher.aspx

1 0

PhD Positions in Formal Methods and Language-based Security at Chalmers
by Andrei Sabelfeld 20 Feb '13

20 Feb '13

*PhD* Positions in Formal Methods and Language-based Security at the Dept. of Computer Science and Engineering, Chalmers University of Technology, Sweden Application deadline: March 30, 2013 ------------------------------------------------------------------------ *Job description ...* *... of the 2 PhD positions in Formal Methods* The Formal Methods group is an internationally recognized research group with a high-profile research track record and an excellent network of collaborators. The group's research focus is in the theoretical and practical aspects of formal software verification, including automated reasoning, interactive theorem proving, runtime verification, and test generation. Together with international collaborators, the group members co-developed widely recognized verification tools like KeY (www.key-project.org) Vampire (http://vprover.org) ALIGATOR (http://mtc.epfl.ch/software-tools/Aligator) and LARVA. The research of the two advertised PhD positions will be in the area of Software Verification, where - one position has a stronger focus on the creative use and development of automated reasoning techniques for software verification, - the other has a stronger focus on combining static and runtime verification of software. The selection of the specific research topic will take into account both the interests of the new PhD student and the research agenda of the group. *... of the (up to) 2 PhD positions in Language-based Security* The PhD students will join a world-leading team of researchers on programming language-based security. Language-based security facilitates specifying and enforcing security policies at the level of programming languages early in the software design and construction phase. The focus of the advertised positions is on the following directions of work: - To design rich security policies for confidentiality and integrity, as demanded by practical applications (such as web applications). - To develop practical enforcement mechanisms for these policies in expressive programming languages (such as web languages). These enforcement mechanisms may combine static (for example, type system-based) and dynamic (for example, execution monitoring-based) techniques. - To support the above with case studies in web-application security. In pursuing these goals, there are possibilities for collaboration with our high-profile academic and industrial partners. We run a number of ambitious projects with top international partners in academia and industry, including the European project WebSand on web application security: https://www.websand.eu/ ------------------------------------------------------------------------ *Details about Employment* PhD student positions are limited to five years and normally include 20 per cent departmental work, mostly teaching duties. Salary for the position is as specified in Chalmers' general agreement for PhD student positions. Currently the starting salary is 26,250SEK a month before tax. The positions are intended to start in spring or fall 2013. ------------------------------------------------------------------------ *Suitable Background* Applicants for a PhD position must have a degree in Computing Science or in a related subject with a strong Computing Science component. They must also have a strong, documented interest in doing research. The ideal candidate for a position in Formal Methods will have strong background in one or more of the following areas: logic, theorem proving, software verification. The ideal candidate for a position in Language-based Security will have strong background in both programming languages and security. You may even apply if you have not yet completed your degree, but expect to do so before the position starts. ------------------------------------------------------------------------ *The Department* The Department has about 70 faculty members and enrolls about 70 PhD students from more than 30 countries. The research spans the whole spectrum, from theoretical foundations to applied systems development. There is extensive national and international collaboration with academia and industry all around the world. For more information, see http://www.chalmers.se/cse/EN/ Knowledge of Swedish is not a prerequisite for application. English is our working language for research. Both Swedish and English are used in undergraduate courses. Half of our researchers and PhD students come from more than 30 different countries. ------------------------------------------------------------------------ *Gothenburg, Sweden* Gothenburg is often referred to as the "heart of Scandinavia". The videos below give an impression what it's like to live and study in Gothenburg. Live in Gothenburg: http://youtu.be/sbwVIQeGcdY Study in Gothenburg: http://youtu.be/0WrlGlSyS1c ------------------------------------------------------------------------ *How to Apply* Electronic application can be submitted following these guidelines: For the PhD positions in Formal Methods: http://www.chalmers.se/en/about-chalmers/vacancies/Pages/default.aspx?RMURL… For the PhD positions in Language-based Security: http://www.chalmers.se/en/about-chalmers/vacancies/Pages/default.aspx?RMURL…

1 0

Call for Papers: 10th International Colloquium on Theoretical Aspects of Computing, September 4-6, 2013, Shanghai, China
by Huibiao Zhu 18 Feb '13

18 Feb '13

*************************************************************** ICTAC 2013 10th International Colloquium on Theoretical Aspects of Computing *** Call For Papers *** September 4-6, 2013 Shanghai, China http://ictac2013.ecnu.edu.cn/ *************************************************************** ICTAC 2013 is the 10th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC 2013 will bring together practitioners and researchers from academia, industry and government to present research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development. The other main purpose is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries, as in the mandate of the United Nations University. THEMES AND TOPICS OF PAPERS ICTAC 2013 calls for regular research papers on theories of computation and programming, foundations of software engineering, and on formal techniques in software design and verification; short papers on recent work or proposals of challenges in new programming paradigms such as Cyber-Physical Systems, Cloud Computing and Social Networks; and papers about tools that support formal techniques for software modeling, system design and verification. The topical areas of the conference include, but not limited to Automata theory and formal languages; Principles and semantics of programming languages; Theories of concurrency, mobility and reconfiguration; Logics and their applications; Software architectures and their models, refinement and verification; Relationship between software requirements, models and code; Program static and dynamic analysis and verification; Software specification, refinement, verification and testing; Model checking and theorem proving; Models of object and component systems; Coordination and feature interaction; Integration of theories, formal methods and tools for engineering computing systems; Service-oriented architectures: models and development methods; Models of concurrency, security, and mobility; Theory of distributed, grid and cloud computing; Real-time, embedded, hybrid and cyber-physical systems; Type and category theory in computer science; Models for learning and education; Case studies, theories, tools and experiments of verified systems; Domain-specific modeling and technology: examples, frameworks and experience. Challenges and foundations in the environmental modeling and monitoring, healthcare, and disaster management. PUBLICATION AND SUBMISSION As for the past editions, it is the plan that the proceedings of ICTAC 2013 will be published by Springer in the series Lecture Notes in Computer Science (LNCS) and will be available at the colloquium. A special issue of a journal with extended version of selected papers from ICTAC 2013 is under negotiation. Submissions to the colloquium must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the conference. Submissions can be Regular Papers, Short Papers or Tool Papers. Short papers can present recent or ongoing work or discuss new ideas which are at an early stage of development and have not been thoroughly evaluated yet. Papers should be written in English. Regular Papers should not exceed 18 pages and Short Papers and tool papers should be between 5 and 10 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Papers must be submitted at http://www.easychair.org/conferences/?conf=ictac2013. Short papers and tool papers must contain clear reference to the background theories and techniques; and a tool paper must further provide a link to a webpage that contains a tutorial and demo of the tool. All queries should be sent to the e-mail address ictac2013(a)sei.ecnu.edu.cn. IMPORTANT DATES Paper submission deadline: 8 March 2013 Paper Accept/Reject Notification: 26 Apr 2013 Final paper submission: 17 May 2013 Conference dates: 4 --- 6 September 2013 ASSOCIATED EVENTS Festschrift Symposium in Honor of Prof. Jifeng He: 01-03 September 2013 Summer School on Software Engineering: 26-30 August 2013 INVITED SPEAKERS Luca Cardelli, Microsoft Research Cambridge, UK Jifeng He, East China Normal University, China Marta Kwiatkowska, University of Oxford, UK CONFERENCE CHAIRS Zhou Chaochen, Software Institute, Chinese Academy of Sciences, China Peter Haddawy, UNU-IIST, Macau SAR, China Bill Roscoe, University of Oxford, UK PROGRAMME CHAIRS Zhiming Liu, UNU-IIST, Macau SAR, China Jim Woodcock, University of York, UK Huibiao Zhu, East China Normal University, China PROGRAMME COMMITTEE Farhad Arbab (CWI and Leiden University, The Netherlands) Michael Butler (University of Southampton, UK) Ana Cavalcanti (University of York, UK) Zhenbang Chen (National University of Defense Technology, China) Van Hung Dang (University of Engineering and Technology, Vietnam) Thao Dang (VERIMAG, France) David Deharbe (Universidade Federal do Rio Grande do Norte, Brasil) Jinsong Dong (National University of Singapore, Singapore) Meenakshi Dsouza (IIIT, India) Zhenhua Duan (Xidian University, China) John Fitzgerald (Newcastle University, UK) Martin Fraenzle (Carl von Ossietzky University Oldenburg, Germany) Marcelo Frias (Instituto Tecnologico Buenos Aires, Argentina) Lindsay Groves (Victoria University of Wellington, New Zealand) Kim Guldstrand Larsen (Aalborg University, Denmark) Ian J. Hayes (University of Queensland, Australia) Zhenjiang Hu (NII, Japan) Lei Ju (Shandong University, China) Daniel Kroening (Oxford University, UK) Martin Leucker (University of Lübeck, Germany) Zhiming Liu (UNU-IIST, Macau SAR, China) Annabelle Mciver (Macquarie University, Australia) Dominique Mery (Université de Lorraine, France) Tobias Nipkow (Technische Universit?t München, Germany) Paritosh Pandya (TIFR, India) Jun Pang (University of Luxembourg, Luxembourg) Geguang Pu (East China Normal University, China) Shengchao Qin (Teesside University, UK) Zongyan Qiu (Peking University, China) Abhik Roychoudhury (National University of Singapore, Singapore) Augusto Sampaio (Federal university of Pernambuco, Brasil) Ondrej Sery (University of Lugano, Switzerland) Natarajan Shankar (SRI, US) Marjan Sirjani (Reykjavik University, Iceland) Andrzej Tarlecki (Warsaw University, Poland) Mark Utting (The University of Waikato, New Zealand) Tarmo Uustalu (Tallinn University of Technology, Estonia) Farn Wang (National Taiwan University, Taiwan) Burkhart Wolff (University Paris-Sud, France) Jim Woodcock (University of York, UK) Wang Yi (Uppsala University, Sweden) Naijun Zhan (Chinese Academy of Sciences, China) Jianjun Zhao (Shanghai Jiao Tong University, China) Jianhua Zhao (Nanjing University, China) Huibiao Zhu (East China Normal University, China)

1 0