[TYPES/announce] CfP: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems, extended deadline *May 5th, 2014*
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for cross posting, Deadline extended to *May 5th, 2014*] CALL FOR PAPERS 8th International Verification Workshop (VERIFY'14) in connection with IJCAR 2014 at FLoC 2014 July 23-24, 2014, Vienna, Austria http://vsl2014.at/verify The formal verification of critical information systems has a long tradition as one of the main areas of application for automated theorem proving. Nevertheless, the area is of still growing importance as the number of computers affecting everyday life and the complexity of these systems are both increasing. The purpose of the VERIFY workshop series is to discuss problems arising during the formal modeling and verification of information systems and to investigate suitable solutions. Possible perspectives include those of automated theorem proving, tool support, system engineering, and applications. The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem proving techniques, and in the development of tool support. Practical experiences gained in realistic verifications are of interest to the automated theorem proving community and new theorem proving techniques should be transferred into practice. The overall objective of the VERIFY workshops is to identify open problems and to discuss possible solutions under the theme What are the verification problems? What are the deduction techniques? The 2014 edition of VERIFY aims for extending the verification methods for processes implemented in hard- and software to processes that may well include computer-assistance, but have a large part or a frequent interaction with non-computer-based process steps. Hence the 2014 edition will run under the focus theme Verification Beyond IT Systems A non-exclusive list of application areas with these characteristics are * Ambient assisted living * Intelligent home systems and processes * Business systems and processes * Production logistics systems and processes * Transportation logistics * Clinical processes * Social systems and processes (e.g., voting systems) The scope of VERIFY includes topics such as * ATP techniques in verification * Case studies (specification verification) * Combination of verification systems * Integration of ATPs and CASE-tools * Compositional modular reasoning * Experience reports on using formal methods * Gaps between problems techniques * Formal methods for fault tolerance * Information flow control security * Refinement decomposition * Reliability of mobile computing * Reuse of specifications proofs * Management of change * Safety-critical systems * Security models * Tool support for formal methods Submissions are encouraged in one of the following two categories: A. Regular paper: Submissions in this category should describe previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. Papers must be 5-14 pages long (in EasyChair style) or 6-15 pages long (in Springer LNCS style). B. Discussion papers: Submissions in this category are intended to initiate discussions and hence should address controversial issues, and may include provocative statements. Papers must be 3-14 pages long (in EasyChair style) or 3-15 pages long (in Springer LNCS style). Important dates Abstract Submission Deadline:May 5th, 2014 (extended) Paper Submission Deadline: May 5th, 2014 (extended) Notification of acceptance: May 20, 2014 Final version due: May 27, 2014 Workshop date: July 23-24, 2014 Submission is via EasyChair: http://www.easychair.org/conferences/?conf=verify2014 Program Committee Serge Autexier (DFKI) - chair Bernhard Beckert (Karlsruhe Institute of Technology) - chair Wolfgang Ahrendt (Chalmers University of Technology) Juan Augusto (Middlesex University) Iliano Cervesato (Carnegie Mellon University) Jacques Fleuriot (University of Edinburgh) Marieke Huisman (University of Twente) Dieter Hutter (DFKI GmbH) Reiner Haehnle (Technical University of Darmstadt) Deepak Kapur (University of New Mexico) Gerwin Klein (NICTA and UNSW) Joe Leslie-Hurd (Intel Corporation) Fabio Martinelli (IIT-CNR) Catherine Meadows (NRL) Stephan Merz (INRIA Lorraine) Tobias Nipkow (TU Munich) Lawrence Paulson (University of Cambridge) Johann Schumann (SGT, Inc/NASA Ames) Kurt
[TYPES/announce] 2nd CFP: Dependently Typed Programming 2014
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies if you receive this more than once!] DTP 2014 Workshop on Dependently-Typed Programming 13th July 2014, Vienna, Austria (co-located with CSL-LICS 2014) 2nd CALL FOR PRESENTATIONS http://eb.host.cs.st-andrews.ac.uk/DTP2014 Workshop Overview - Dependently typed programming is here today: where will it go tomorrow? On the one hand, dependent type theories have grown programming languages; on the other hand, the type systems of programming languages like Haskell and Scala are incorporating some kinds of type-level data. The purpose of this workshop is to discuss experiences with dependent types in programming and future developments for dependently-typed languages. Topics of interest include, but are not limited to: * Language Design, both in the context of possible extensions and modifications of existing languages and the development of new languages with dependent types; * Theory, such as formal treatments of semantics and type systems; * Compilation, including implementations and optimization of dependently-typed languages; * Tools, in the form of IDEs, profilers, tracers, debuggers, and testing tools; * Functional Pearls, being elegant, instructive examples of using dependent types; * Experience Reports, general practice and experience with dependently-typed languages, e.g., in an education or industry context. Workshop Format --- The workshop will consist of invited speakers (details TBA) and contributed talks. Talks will be selected according to relevance to the workshop, based on submission of an extended abstract. Submission Details -- * Abstract Submission : Friday, 2nd May 2014 * Author Notification : Friday, 9th May 2014 * Workshop: Sunday, 13th July 2014 Submissions should be an extended abstract of 1--2 pages in portable document format (PDF). Submission is via EasyChair: https://www.easychair.org/conferences/?conf=dtp14 After the workshop, we plan to invite authors to submit full papers for publication, details TBA. Program Committee - Andreas Abel (Chalmers and Gothenburg University, Sweden) Amal Ahmed (Northeastern University, USA) Nicola Botta (Postdam Institute for Climate Impact Research, Germany) Edwin Brady (University of St Andrews, UK, Chair) David Christiansen (IT University of Copenhagen, Denmark) Adam Gundry (Well-Typed LLP) Dan Licata (Wesleyan University, USA) Shin-Cheng Mu (Academia Sinica, Taiwan) Hongwei Xi (Boston University, USA) History --- This workshop follows a series of workshops on dependently-typed programming. Past meetings include [DTP 2013 in Boston](http://www.seas.upenn.edu/~sweirich/dtp13/), [DTP 2011 in Nijmegen](http://www.cs.ru.nl/dtp11/), [DTP 2010 in Edinburgh](http://sneezy.cs.nott.ac.uk/darcs/dtp10/), and [DTP 2008 in Nottingham](http://sneezy.cs.nott.ac.uk/darcs/DTP08/), as well as seminars organized in 2011 at [Shonan Village, Japan](http://www.nii.ac.jp/shonan/seminar007/) and in 2004 at [Dagstuhl, Germany](http://drops.dagstuhl.de/opus/volltexte/2005/186/).
