(PN) Formal Methods in Computer-Aided Design - Call for Papers
2nd CALL FOR PAPERS International Conference on Formal Methods in Computer-Aided Design (FMCAD) Vienna, Austria, October 2-6, 2017 http://www.fmcad.org/FMCAD17 IMPORTANT DATES Abstract Submission:May 01, 2017 Paper Submission: May 08, 2017 Author Response Period: June 19-23, 2017 Author Notification:July 14, 2017 Camera-Ready Version: Aug 09, 2017 All deadlines are 11:59 pm AoE (Anywhere on Earth) FMCAD Tutorial Day: October 2, 2017 FMCAD Regular Program: October 3-6, 2017 Part of the FMCAD 2017 program: - Symposium in memoriam of Helmut Veith - Hardware Model Checking Competition 2017 - FMCAD Student Forum (deadline: July 21, 2017) Limited funds will be available for travel assistance for students with accepted contributions at the student forum. Co-located event: MEMOCODE 2017 (http://memocode.irisa.fr/2017/) CONFERENCE SCOPE AND PUBLICATION FMCAD 2017 is the seventeenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing. FMCAD employs a rigorous peer-review process. Accepted papers are distributed through both ACM and IEEE digital libraries. In addition, published articles are made available freely on the conference page; the authors retain the copyright. There are no publication fees. At least one of the authors is required to register for the conference and present the accepted paper. A small number of outstanding FMCAD submissions will be considered for inclusion in a Special Issue of the journal on Formal Methods in System Design (FMSD). TOPICS OF INTEREST FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer- aided design. Topics of interest include (but are not limited to): -- Model checking, theorem proving, equivalence checking, abstraction and reduction, compositional methods, decision procedures at the bit- and word-level, probabilistic methods, combinations of deductive methods and decision procedures. -- Synthesis and compilation for computer system descriptions, modeling, specification, and implementation languages, formal semantics of languages and their subsets, model-based design, design derivation and transformation, correct-by-construction methods. -- Application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software, including timing and power modeling, verification of computing systems on all levels of abstraction, system-level design and verification for embedded systems, cyber-physical systems, automotive systems and other safety-critical systems, hardware-software co-design and verification, and transaction-level verification. -- Experience with the application of formal and semi-formal methods to industrial-scale designs; tools that represent formal verification enablement, new features, or a substantial improvement in the automation of formal methods. -- Application of formal methods to verifying safety, correctness, connectivity, and security properties of networks and distributed systems. SUBMISSIONS Submissions must be made electronically in PDF format via EasyChair: https://easychair.org/conferences/?conf=fmcad17 Two categories of papers are invited: Regular papers, and Tool & Case Study papers. Regular papers are expected to offer novel foundational ideas, theoretical results, or algorithmic improvements to existing methods, along with experimental impact validation where applicable. Tool & Case Study papers are expected to report on the design, implementation or use of verification (or related) technology in a practically relevant context (which need not be industrial), and its impact on design processes. Both Regular and Tool & Case study papers must use the IEEE Transactions format on letter-size paper with a 10-point font size. Regular papers can be up to 8 pages in length and tool papers up to 4 pages, although there is no requirement to fill all pages in either category. Authors will be required to select the appropriate paper category at abstract submission time. Submissions may contain an optional appendix, which will not appear in the final version of the paper. The reviewers should be able to assess the quality and the relevance of the results in the paper without reading the appendix. Submissions in both categories must contain original research that has not been previously published, nor is concurrently submitted for publication. Any partial overlap with
(PN) Summer School on Verification Technology
=== First Call for Participation 10th International Summer School on Verification Technology, Systems & Applications http://www.mpi-inf.mpg.de/vtsa17/ The 10th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by the Max-Planck-Institut für Informatik Saarbrücken in cooperation with the University of Liège, Inria Nancy - Grand Est, and the Université du Luxembourg. The school will take place from July 31st to August 4th, 2017 on Saarland Informatics Campus, Saarbrücken, Germany. The following speakers have accepted to give courses at VTSA 2017: - Rajeev Alur: Syntax-Guided Synthesis & Quantitative Policies over Streaming Data - Christel Baier: Probabilistic Model Checking - Hoon Hong: Symbolic Computation (Quantifier Elimination) - Andrew Reynolds: SMT Solvers for Verification and Synthesis - Thomas Wies: Introduction to Permission-Based Program Logics Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science; it includes the lectures, daily coffee and lunchbreaks, and a school dinner. There is a limited number of free shared rooms on campus available for distribution by the selection committee. Please express your interest with your application. Attendance is limited to 40 participants. Please apply electronically by sending to fku...@mpi-inf.mpg.de: - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, - a copy of your bachelor certificate (or equivalent or a more significant certificate), - a short statement if you want to contribute to the student sessions. The deadline for application is June 1st, 2017. Notification of acceptance will be given by June 15th, 2017. Full details are available at http://www.mpi-inf.mpg.de/vtsa17/ The school is synchronized with the SC2 Summer School 2017, happening at the same time in the same place: http://www.sc-square.org/CSA/school/index.html [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) TABLEAUX/FroCoS/ITP Call for Papers
(Apologies for multiple copies. Please redistribute) * FIRST CALL FOR PAPERS TABLEAUX 2017 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods University of BrasÃlia, Brazil September 26-29, 2017 Submission Deadline: 25 Apr 2017 http://tableaux2017.cic.unb.br/ GENERAL INFORMATION TABLEAUX is the main international conference at which research on all aspects, theoretical foundations, implementation techniques, systems development and applications, of the mechanization of tableau-based reasoning and related methods is presented. The conference will be held in BrasÃlia from 26-29 September 2017. TABLEAUX 2017 will be co-located with both the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017). TOPICS Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableau methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation; * flexible, easily extendable, light weight methods for theorem proving; * novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...); * extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs; * decision procedures, theoretically optimal procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community and should focus on the role of reasoning, and logical aspects of the solution. WORKSHOPS AND TUTORIALS Proposals for Workshops and Tutorial sessions have been solicited in a separate call, which can be found at http://tableaux2017.cic.unb.br/#cfw. PUBLICATION DETAILS The conference proceedings will published in the Springer LNAI/LNCS series, as in previous editions. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 9 pages. Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical elegance, and possible implementability. For category B submissions, a working implementation must be accessible via the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system: https://easychair.org/conferences/?conf=tableaux2017. For all accepted papers at least one author is required to attend the conference and present the paper. A paper title and a short abstract of about 100 words must be submitted before the paper
(PN) TABLEAUX, FroCoS, ITP - Call for Workshops and Tutorials
(with apologies for multiple postings) CALL FOR WORKSHOPS AND TUTORIALS Three of the main conferences on automated reasoning -- TABLEAUX, FroCoS, and ITP - will be held in Brasilia, Brazil, between 25 and 29 September 2017. Following the long tradition of those events, we invite researchers and practitioners to submit proposals for co-located workshops and in-depth tutorials on topics relating to automated theorem proving and its applications. Workshops/tutorials can target the automated reasoning community in general, focus on a particular theorem proving system, or highlight more specific issues or recent developments. Co-located events will take place between 23 and 24/25 September and will be held on the same premises as the main conference. Conference facilities are offered free of charge to the organisers. Workshop/tutorial-only attendees will enjoy a significantly reduced registration fee. Detailed organisational matters such as paper submission and review process, or publication of proceedings, are up to the organisers of individual workshops. All accepted workshops/tutorials will be expected to have their program ready by 18 August 2017. Proposals for workshops/tutorials should contain at least the following pieces of information: - name and contact details of the main organiser(s) - (if applicable:) names of additional organisers - title and organisational style of event (tutorial, public workshop, project workshop, etc.) - preferred length of workshop (between half day and two days) - estimated number of attendees - short (up to one page) description of topic - (if applicable:) pointers to previous editions of the workshop, or to similar events Proposals are invited to be submitted by email to na...@unb.br, no later than 9 December 2016. Selected events will be notified by 23 December 2016. The workshop/tutorial selection committee consists of the TABLEAUX, FroCoS, and ITP program chairs and the conference organisers. [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) DL 2017, Call for Papers
--- CALL FOR PAPERS 30th International Workshop on Description Logics, DL 2017 July 18th to July 21st, 2017 - Montpellier, France http://dl.kr.org/dl2017/ --- The DL workshop is the major annual event of the description logic research community. It is the forum at which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences. The workshop will be held in Montpellier, France from July 18th to July 21st, 2017. Important Dates (Firm Deadlines) Paper registration deadline: April 28, 2017 Paper submission deadline: May 8, 2017 Notification of acceptance: June 12, 2017 Camera-ready copies: July 3, 2017 Workshop: July 18-21, 2017 Since we wanted the DL submission deadlines to be after the IJCAI notification date, the schedule is tight and NO DEADLINE EXTENSIONS will be possible. Invited Speakers = * Markus Krötzsch, Technical University of Dresden * Andreas Pieris, University of Edinburgh * Uli Sattler, University of Manchester Workshop Scope = We invite contributions on all aspects of description logics, including but not limited to: * Foundations of description logics: decidability and complexity of reasoning, expressive power, novel inference problems, inconsistency management, reasoning techniques, and modularity aspects * Extensions of description logics: closed-world and nonmonotonic reasoning, epistemic reasoning, temporal and spatial reasoning, procedural knowledge, query answering, reasoning over dynamic information * Integration of description logics with other formalisms: object-oriented representation languages, database query languages, constraint-based programming, logic programming, and rule-based systems * Applications and use areas of description logics: ontology engineering, ontology languages, databases, ontology-based data access, semi-structured data, graph structured data, linked data, document management, natural language, learning, planning, Semantic Web, cloud computing, conceptual modelling, web services, business processes * Systems and tools around description logics: reasoners, software tools for and using description logic reasoning (e.g. ontology editors, database schema design, query optimisation, and data integration tools), implementation and optimisation techniques, benchmarking, evaluation, modelling Submissions == * Submissions may be of two types: (1) Papers accepted at some conference can be submitted as accepted elsewhere together with a 1-page abstract that also specifies where the paper has been accepted. (2) Other submissions consist of 11 pages LNCS plus references. There is no page limit on the list of references. If the paper should not appear in the proceedings, an additional 1-page abstract has to be submitted. * For submissions with an additional 1-page abstract, only the abstract is published in the proceedings. The abstracts might not be indexed in dblp. This option is designed for authors who wish to announce results that have been published elsewhere, or which the authors intend to submit or have already submitted to a venue with an incompatible prior/ concurrent publication policy. * All submissions may optionally include a clearly marked appendix (e.g., with additional proofs or evaluation data). The appendix will be read at the discretion of the reviewers and not included in the proceedings. The appendix does not need to be in LNCS format. * Submission page: https://easychair.org/conferences/?conf=dl2017 * Accepted papers and 1-page abstracts will be made available electronically in the CEUR Workshop Proceedings series (http://www.CEUR-ws.org/). * Accepted submissions, be they full papers or 1-page abstracts, will be selected for either oral or poster presentation at the workshop. Submissions will be judged solely based upon their content, and the type of submission will have no bearing on the decision between oral and poster presentation. Organisation * Alessandro Artale, Free University of Bozen-Bolzano (Programme co-Chair) * Birte Glimm, University of Ulm (Programme co-Chair) * Meghyn Bienvenu, University of Montpellier (Workshop co-Chair) * Marie-Laure Mugnier, University of Montpellier (Workshop co-Chair) Resources = * Information about submission, registration, travel information, etc., will be made available on the DL 2017 homepage: http://dl.kr.org/dl2017/ * The official description logic homepage is at http://dl.kr.org/ [[ Petri Nets World:]] [[
(PN) GCAI 2016 - Call for Participation
The 2nd Global Conference on Artificial Intelligence Berlin Germany, 29th September - 2nd October 2016 http://easychair.org/smart-program/GCAI2016/ Call for Participation The 2nd Global Conference on Artificial Intelligence (GCAI 2016) will be held at the Freie Universitaet Berlin from 29th September to 2nd October, 2016. The conference addresses all aspects of artificial intelligence. There will be 29 papers presented, tutorials on automated theorem proving in classical and non- classical logic, and three invited speakers ... Simon Colton, Falmouth University, and Goldsmiths, University of London, UK Computational Creativity Daniel Lee, University of Pennsylvania, USA Robotics and Machine Learning Toby Walsh, TU Berlin, Germany and UNSW/Data61, Australia Will AI end Jobs, Wars or Humanity? The full program is available at http://easychair.org/smart-program/GCAI2016/program.html Registration: http://easychair.org/smart-program/GCAI2016/Registration.html GCAI is organized by LRG (http://www.lrg.global) and the Freie Universitaet Berlin. [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) 7th ITP Conference
The 7th International Conference on Interactive Theorem Proving 22 to 27 August 2016 in Nancy, France https://itp2016.inria.fr Early registration deadline: 30 June Main conference: 22 August to 25 August (morning) Affiliated events: 25 August (afternoon) to 27 August ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications. The program committee accepted 27 regular papers and 5 rough diamonds this year: https://itp2016.inria.fr/program/ There will be invited talks by Viktor Kuncak (EPFL) Grant Olney Passmore (Aesthetic Integration and University of Cambridge) Nikhil Swamy (Microsoft Research) The following affiliated events will take place after the main conference: Coq Workshop 2016 Isabelle Workshop 2016 Mathematical Components, an Introduction Up-to-date information and online registration can be found at https://itp2016.inria.fr [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) CFP extended deadline - 2nd Global Conference on Artificial Intelligence
=== The 2nd Global Conference on Artificial Intelligence Berlin Germany, 29th September - 2nd October 2016 http://easychair.org/smart-program/GCAI2016/ *** Extended Submission Deadline *** *** (Abstract: 23rd June, Paper: 27th June) *** The 2nd Global Conference on Artificial Intelligence (GCAI 2016) will be held at the Freie Universitaet Berlin from 29th September to 2nd October, 2016. The conference, which addresses all aspects of artificial intelligence, is being organized by LRG (http://www.lrg.global) and the Freie Universitaet Berlin. The program chairs are Christoph Benzmueller, Raul Rojas, and Geoff Sutcliffe. SUBMISSION Submissions in all areas of Artificial Intelligence are welcome, including, but not limited to ... Foundations + Knowledge representation + Cognitive modeling + Perception + Search + Reasoning and programming + Machine learning + Constraints and uncertainty Architectures + Agents and distributed AI + Intelligent user interfaces + Natural language systems and linguistics + Information retrieval + Case-based reasoning + Affective computing + Robotics Applications + Aviation and aerospace + Education and tutoring systems + Games and entertainment + Medicine and healthcare + Management and manufacturing + World Wide Web + Security Implications + Philosophical foundations + Social impact and ethics + Evaluation of AI systems + AI education (EXTENDED) DATES + Abstract registration: 23rd June, 2016 + Submission: 27th June, 2016 + Notification: 1st August, 2016 + Final version: 15th August, 2016 + Early registration deadline: 15th August, 2016 + Conference: 29th September - 2nd October, 2016 SUBMISSION and PUBLICATION Submission is via EasyChair at https://easychair.org/conferences/?conf=gcai2016 The proceedings will be published by EasyChair Publications in the EPiC Series in Computing. The volume will be open access and authors will retain copyright. INVITED SPEAKERS + Daniel Lee, University of Pennsylvania, USA + Simon Colton, Falmouth University and Goldsmiths, University of London, UK PROGRAM COMMITTEE + Natasha Alechina (University of Nottingham) + Jose Julio Alferes (Universidade NOVA de Lisboa) + Serge Autexier (DFKI) + Roman Bartak (Charles University in Prague) + Peter Baumgartner (National ICT Australia) + Christoph Benzmüller (Freie Universität Berlin) - chair + Philippe Besnard (CNRS / IRIT) + Richard Booth (Cardiff University) + Oscar Corcho (Universidad Politécnica de Madrid) + Gabriella Cortellessa (CNR - National Research Council of Italy) + Mehdi Dastani (Utrecht University) + James Delgrande (Simon Fraser University) + Wolfgang Faber (University of Huddersfield) + Germain Forestier (Université de Haute Alsace) + Thom Frühwirth (University of Ulm) + Daniel Garijo (UPM) + Marco Gavanelli (University of Ferrara) + Luis Godo (Artificial Intelligence Research Institute, IIIA - CSIC) + Gianluigi Greco (University of Calabria) + Andreas Herzig (IRIT-CNRS) + Tomi Janhunen (Aalto University) + Ernesto Jimenez-Ruiz (University of Oxford) + Tommi Junttila (Aalto University School of Science) + Panagiotis Kanellopoulos (University of Patras and CTI "Diophantus") + Gabriele Kern-Isberner (Technische Universitaet Dortmund) + Roman Kontchakov (Birkbeck, University of London) + Jérôme Lang (LAMSADE) + Sanjiang Li (University of Technology Sydney) + Jean Lieber (LORIA - INRIA Lorraine) + Alberto Lluch Lafuente (Technical University of Denmark) + Ana Gabriela Maguitman (Universidad Nacional del Sur) + Robert Mattmüller (University of Freiburg) + Julian Mcauley (UC San Diego) + George Metcalfe (University of Bern) + Angelo Montanari (University of Udine) + Manuel Ojeda-Aciego (University of Malaga) + Magdalena Ortiz (Vienna University of Technology) + Sascha Ossowski (University Rey Juan Carlos) + LuÃs Moniz Pereira (Universidade Nova de Lisboa) + Radu-Emil Precup (Politehnica University of Timisoara) + Fabrizio Riguzzi (University of Ferrara) + Jussi Rintanen (Aalto University) + Raul Rojas (Freie Universität Berlin) - chair + Dumitru Roman (SINTEF) + Marco Roveri (FBK-irst) + Steven Schockaert (Cardiff University) + Gia Sirbiladze (Tbilisi State university) + Thomas Stützle (Université Libre de Bruxelles) + Geoff Sutcliffe (University of Miami) - chair + Jürgen Umbrich (Vienna University of Economy and Business) + Pascal Van Hentenryck (University of Michigan) + Martin Wehrle (University of Basel) + Stefan Woltran (TU Wien) + Inon Zuckerman (Ariel University) === [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailin
(PN) Verification Mentoring Workshop - Travel Scholarships
Call for Applications for VMW (Verification Mentoring Workshop) 2016 Verification Mentoring Workshop 2016 Call for Applications for Student Travel Scholarships We are organizing the second Verification Mentoring Workshop (VMW) 2016. It is co-located with the International Conference on Computer Aided Verification (CAV), to be held in Toronto, July 17-23, 2016. CAV is a premier conference in the area of verification, dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The goal of VMW is to attract early-stage graduate students to pursue research careers in the area of computer-aided verification and formal methods. Invited talks at the workshop will cover a broad overview of research topics in the area, the range of career options and perspectives (academia, industry, research labs, etc.), and insights into reviewing processes (for papers, grants, and job applications). We will provide travel scholarships to student participants (graduates, and rising senior undergraduates), where the scholarships will cover registration for VMW and CAV, accommodations, plus travel expenses. Participation of women and under-represented minorities is especially encouraged. The VMW workshop website http://i-cav.org/2016/vmw is now accepting applications. Important Dates: + Deadline for submission of applications: Extended to April 20, 2016 + Notification of travel scholarships awarded: May 1, 2016 + VMW Workshop: July 18, 2016 VMW 2016 is partially supported by Microsoft Research and the NSF (National Science Foundation, USA). More details on the VMW workshop and CAV conference can be found at http://i/~cav.org/2016/ Organizers of VMW 2016: + Aarti Gupta, Princeton, USA + Ruzica Piskac, Yale, USA + Andrey Rybalchenko (Chair), Microsoft Research, UK [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) AiML-2016: 1ST CALL FOR PAPERS
(sorry for multiple copies) AiML-2016: 1ST CALL FOR PAPERS 11TH INTERNATIONAL CONFERENCE ON ADVANCES IN MODAL LOGIC BUDAPEST, 29 AUGUST -- 2 SEPTEMBER 2016 http://phil.elte.hu/aiml2016/ Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http://www.aiml.net. AiML-2016 is the 11th conference in the series. TOPICS We invite submission on all aspects of modal logic, including: - history of modal logic - philosophy of modal logic - applications of modal logic - computational aspects of modal logic (complexity and decidability of modal and temporal logics, modal and temporal logic programming, model checking, model generation, theorem proving for modal logics) - theoretical aspects of modal logic (algebraic/categorical perspectives on modal logic, coalgebraic modal logic, completeness and canonicity, correspondence and duality theory, many-dimensional modal logics, modal fixed point logics, model theory of modal logic, proof theory of modal logic) - specific instances and variations of modal logic (description logics, modal logics over non-boolean bases, dynamic logics and other process logics, epistemic and deontic logics, modal logics for agent-based systems, modal logic and game theory, modal logic and grammar formalisms, provability and interpretability logics, spatial and temporal logics, hybrid logic, intuitionistic logic, substructural logics, computationally light fragments of all such logics) Papers on related subjects will also be considered. PAPER SUBMISSIONS There will be two types of submissions to AiML-2016: (1) Full papers for publication in the proceedings and presentation at the conference. (2) Short presentations intended for presentation at the conference but not for the published proceedings. Both types of papers should be submitted electronically using the EasyChair submission page at https://easychair.org/conferences/?conf=aiml16 At least one author of each accepted paper or short presentation must register for and attend the conference. (1) FULL PAPERS Authors are invited to submit, for presentation at the conference and publication in the proceedings, full papers reporting on original research and not submitted elsewhere. The proceedings of AiML-2016 will be published by College Publications http://www.collegepublications.co.uk in a volume to be made available at the conference. The submissions should be at most 15 pages, with an optional technical appendix of up to 5 pages, together with a plain-text abstract of 100-200 words. The submissions must be typeset in LaTeX, using the style files and template that will be provided on the AiML-2016 website http://phil.elte.hu/aiml2016/ in due time. We also ask authors of full papers to submit the abstract in plain text via EasyChair by 10 March. (2) SHORT PRESENTATIONS. These should be at most 5 pages. They may describe preliminary results, work in progress etc., and will be subject to light reviewing. The accepted submissions will be made available at the conference, and the authors will have the opportunity to give short presentations (of up to 15 minutes) on them. INVITED SPEAKERS INCLUDE: Kit Fine (New York University, USA) Sonja Smets (ILLC, Universiteit van Amsterdam) Yde Venema (ILLC, Universiteit van Amsterdam) LOCAL ORGANIZING COMMITTEE Tamas Bitai (Eotvos University, Budapest, Hungary) Reka Markovich (Eotvos University, Budapest, Hungary) Andras Mate (Eotvos University, Budapest, Hungary) Péter Mekis (Eotvos University, Budapest, Hungary) Attila Molnar (Eotvos University, Budapest, Hungary) Gergely Szekely (Alfred Rényi Institute of Mathematics, Hungarian Academy of Sciences) PROGRAMME COMMITTEE Natasha Alechina (University of Nottingham) Carlos Areces (FaMAF, Universidad Nacional de Córdoba) Philippe Balbiani (IRIT, Toulouse, France) Alexandru Baltag (FNWI ILLC) Lev Beklemishev (Steklov Mathematical Institute of Russian Academy of Sciences in Moscow) Thomas Bolander (Technical University of Denmark) Torben Brauner (Roskilde University, Denmark) Serenella Cerrito (Laboratoire IBISC, Evry France) Stéphane Demri (LSV, CNRS, ENS Cachan) David Fernandez-Duque (Instituto Tecnológico Autónomo de México) Melvin Fitting (Lehman College, CUNY, USA) David Gabelaia (gabelaia at gmail dot com) (The Free University of Tbilisi, Tbilisi, Georgia) Silvio Ghilardi (Università degli Studi di Milano, Italy) Valentin Goranko (Stockholm University) Rajeev Gore (The Australian National University) Andreas Herzig (IRIT, Toulouse, France) Rosalie Iemhoff (Utrecht University) Agi Kurucz (King's College London) Roman Kuznets (TU Wien) Martin Lange (University of Kassel, Germany) Carsten Lutz (Universität Bremen)
(PN) Artificial Intelligence and Theorem Proving
CALL FOR CONTRIBUTIONS 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016 April 3-6, 2016, Obergurgl, Austria http://aitp-conference.org Deadline: December 12, 2015 https://easychair.org/conferences/?conf=aitp2016 Background Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. Topics - AI and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving. - Common-sense reasoning and reasoning in science. - Alignment and joint processing of formal, semi-formal, and informal libraries. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods. Sessions and Speakers There will be three focused sessions on AI for ATP, ITP and mathematics, a (tutorial) session on modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. - AI and large-theory ATP/ITP. Confirmed speakers: Thomas C. Hales - AI and internal guidance of ATP. Confirmed speakers: Robert Veroff, Stephan Schulz - AI and automated understanding of informal and semi-formal mathematics. Confirmed speakers: Noriko Arai, Deyan Ginev, Takuya Matsuzaki, Jiri Vyskocil - Modern AI and big-data methods (tutorials/connections to ATP/ITP/math). Confirmed speakers: Sean Holden, Christian Szegedy Contributed talks We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2016) by 12 December 2015. The authors will be notified of acceptance/rejection by 23 December 2015. Camera-ready versions of the accepted contributions, due by 1 February 2016, will be published in an informal book of abstracts for distribution at the conference. Post-proceedings We will publish post-proceedings in an open-access series of conference proceedings, such as LIPIcs, JMLR, or EPiC. Submission to that volume will be open for everyone. Tentative submission deadline: May 2016. Programme committee Marcos Cramer (Universiy of Luxembourg) Thomas C. Hales (co-chair) (University of Pittsburgh) Tom Heskes (Radboud University Nijmegen) Sean Holden (University of Cambridge) Cezary Kaliszyk (co-chair) (University of Innsbruck) Ramana Kumar(University of Cambridge) John Lafferty (University of Chicago) Lawrence Paulson(University of Cambridge) Stephan Schulz (co-chair) (DHBW Stuttgart) Geoff Sutcliffe (University of Miami) Josef Urban (co-chair) (Czech Technical University in Prague) Location and Price The conference will take place from April 3 to April 6 in the stunning scenery of the Tyrolean Alps in the Obergurgl Conference Center (http://www.uz-obergurgl.at/) of the University of Innsbruck. Obergurgl is a picturesque village located at an altitude of 2000m, a 1-hour drive from Innsbruck. It offers a variety of winter-sport activities such as skiing, snowshoeing and hiking at this time of the year. The total price for accommodation, food and registration for the four days will be around 500 EUR. Organizers Cezary Kaliszyk and Josef Urban [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-20 Short Presentation Papers
=== The 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning Suva, Fiji, 23rd-28th November 2015 www.LPAR-20.info CALL FOR SHORT PRESENTATION PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The short presentation papers will be published electronically as a volume in the EPiC series, see http://www.easychair.org/publications/EPiC. The LaTeX and Microsoft Word templates for the EPiC series can be downloaded from http://www.easychair.org/publications/for_authors. Short papers may be up to 15 pages long, and must be submitted through the EasyChair system using the web page https://www.easychair.org/conferences/?conf=lpar20. Paper submission deadline: 19th October 2015 Notification of acceptance: 2nd November 2015 Final version: 9th November 2015 ... however, in order to facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately one week. Submit early, and submit often! === [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) FMCAD Student Forum - Call for Contributions
FMCAD 2015 STUDENT FORUM 2nd call for contributions FMCAD 2015, the fifteenth conference on the theory and applications of formal methods in hardware and system verification, will host the 3rd FMCAD Student Forum (September 28-30, 2015) providing a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community. IMPORTANT DATES Submission Deadline: June 21, 2015 Acceptance notification: July 19, 2015 Forum date: September 28-30, 2015 Details are provided on http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/student-forum.shtml Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. All submissions will be reviewed by a select group of program committee members. The event will consist of short presentations by the student authors of each accepted submission, and of a poster that will be on display throughout the duration of the conference. Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their poster and presentation to the FMCAD web site. The best contribution (determined by the committee based on the quality of the submission and the presentation) will be given public recognition and a certificate at the event. Limited funds will be available for travel assistance for students with accepted contributions. We kindly ask faculty members to help us advertise the event by displaying the posters available from the web-page in their departments. If you have questions, please contact the forum chair Georg Weissenbacher (Vienna University of Technology, Austria). For more details visit http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/index.shtml [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-20 in Fiji - Call for Papers and Workshops
The 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-20 University of the Pacific, Suva, Fiji http://www.LPAR-20.org CALL FOR PAPERS AND WORKSHOPS The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 20th LPAR will be held at the University of the South Pacific, Suva, Fiji in 2015 (see dates below). == Topics New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: + Abduction and interpolation methods + Automated reasoning + Constraint programming + Decision procedures + Description logics + Foundations of security + Hardware verification + Implementations of logic + Interactive theorem proving + Knowledge representation and reasoning + Logic and computational complexity + Logic and databases + Logic and games + Logic and machine learning + Logic and the web + Logic and types + Logic in artificial intelligence + Logic of distributed systems + Logic programming + Logical aspects of concurrency + Logical foundations of programming + Modal and temporal logics + Model checking + Non-monotonic reasoning + Ontologies and large knowledge bases + Probabilistic and fuzzy reasoning + Program analysis + Rewriting + Satisfiability checking + Satisfiability modulo theories + Software verification + Specification using logic + Unification theory == Submission Details Submissions of two kinds are welcome: - Regular papers that describe solid new research results. They can be up to 15 pages long in LNCS style, including figures and references, but excluding appendices (that reviewers are not required to read). - Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the LNCS style. Both types of papers must be electronically submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=lpar20 == Participation Prospective authors are required to register a title and an abstract a week before the paper submission deadline (see below). Authors of accepted papers are required to ensure that at least one of them will be present at the conference. More details about the venue and organisation can be found on the conference website. == Important Dates Abstract Submission: 30 June Paper Submission: 7 July Notification: 23 August Workshops: 23 November Conference: 24-28 November == Programme Committee Cyrille ValentinArtho AIST, Japan Franz BaaderTU Dresden, Germany Christel Baier TU Dresden, Germany Peter Baumgartner NICTA, Australia Armin Biere Johannes Kepler University, Austria Nikolaj Bjorner Microsoft Research, USA Lei Bu Nanjing University, China Franck Cassez Macquarie University, Australia Ansgar Fehnker University of the South Pacific Rajeev Gore Australian National University, Australia Tim Griffin University of Cambridge, UK Ralf Huuck NICTA and UNSW, Australia Kim Guldstrand Larsen Aalborg University, Denmark Dejan Jovanovic SRI International, USA Gerwin KleinNICTA and UNSW, Australia Dexter KozenCornell University, USA Rustan LeinoMicrosoft Research, USA Joe Leslie-Hurd Intel Corporation, USA Annabelle McIverMacquarie University, USA Kenneth McMillanMicrosoft Research, USA Marius MineaPolitehnica University of Timisoara, Romania Matteo Mio CNRS, ENS Lyon, France Prakash Panangaden McGill University, Canada Christine Paulin-MohringUniversit=C3=A9 Paris-Sud, France Andreas PodelskiUniversity of Freiburg, Germany Geoff Sutcliffe University of Miami, USA Gancho Vachkov The University of the south Pacific (USP), Fiji Ron Van Der Meyden UNSW, Australia Tomas VojnarBrno University of Technology, Czech Republic Andrei Voronkov University of Manchester, UK Toby Walsh NICTA and UNSW, Australia More to be announced ... CALL FOR WORKSHOPS LPAR-20 workshops will be held either as one-day or half-day events. If you would like to propose a workshop for LPAR-20, please
(PN) 3rd FMCAD Student Forum
FMCAD 2015 STUDENT FORUM FMCAD 2015, the fifteenth conference on the theory and applications of formal methods in hardware and system verification, will host the 3rd FMCAD Student Forum (September 28-30, 2015) providing a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community. IMPORTANT DATES Submission Deadline: June 21, 2015 Acceptance notification: July 19, 2015 Forum date: September 28-30, 2015 Details are provided on http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/student-forum.shtml Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. All submissions will be reviewed by a select group of program committee members. The event will consist of short presentations by the student authors of each accepted submission, and of a poster that will be on display throughout the duration of the conference. Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their poster and presentation to the FMCAD web site. The best contribution (determined by the committee based on the quality of the submission and the presentation) will be given public recognition and a certificate at the event. Limited funds will be available for travel assistance for students with accepted contributions. We kindly ask faculty members to help us advertise the event by displaying the posters available from the web-page in their departments. If you have questions, please contact the forum chair Georg Weissenbacher (Vienna University of Technology, Austria). For more details visit http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/index.shtml [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) TABLEAUX - Call for Papers
SECOND CALL FOR PAPERS TABLEAUX 2015 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods Wroclaw, Poland, September 21-24, 2015 http://tableaux2015.ii.uni.wroc.pl/ GENERAL INFORMATION TABLEAUX 2015 is the 24th in the series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods, and will be held in Wroclaw, Poland, during September 21-24, 2015. TABLEAUX 2015 will be co-located with the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015). The computer science institute of Wroclaw has a large experience in hosting international conferences. It has hosted the IEEE Symposium on Logic in Computer Science (LICS 2007), the 24th International Conference on Automated Deduction (CADE 2011), and the 22nd European Symposium on Algorithms (ALGO 2014). TOPICS Tableaux methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableaux methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. The conference series aims to bring together researchers interested in all aspects of tableaux - theoretical foundations, applications, and implementation techniques. * tableaux methods for classical and non-classical logics (e.g. modal, temporal, description, intuitionistic, substructural, fuzzy, paraconsistent logics) and their proof theoretic foundations. * related methods (model elimination, model checking, connection methods, resolution, BDDs). * sequent calculi for classical and non-classical logics, as tools for proof search and proof representation. * flexible, easily extendable, light weight methods for theorem proving. * novel types of calculi for theorem proving and verification in classical and non-classical logics. * systems, tools, implementations and applications (provers, logical frameworks, model checkers, ... ). * implementation techniques (data structures, efficient algorithms, performance measurement, extendibility, ... ). * extensions of tableaux procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs. * decision procedures, theoretically optimal procedures. * applications of automated deduction to mathematics, software development, protocol verification, or teaching. TABLEAUX 2015 also welcomes papers describing applications of tableaux procedures to real world examples. Such papers should be tailored to the tableaux community and should focus on the role of reasoning, and logical aspects of the solution. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 10 pages. Submissions will be reviewed by the PC, possibly will help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical prettyness, and possible implementability. For category B submissions, a working implementation must be available on the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings (within the LNAI series of Springer). For accepted papers in both of the categories, at least one author is required to attend the conference and present the paper. Further information and instructions about submissions can be found on the conference website http://tableaux2015.ii.uni.wroc.pl IMPORTANT DATES Abstract submission deadline: May 8th, 2015 Paper submission deadline:May 15th, 2015 Author Notification: July 1st, 2015 Final Version:July 17th 2015 Conference: September 21st-24th, 2015 PROGRAM COMMITTEE - Marc Bezem, University of Bergen, Norway Agata Ciabattoni, Vienna University of Technology, Austria David Delahaye, National Conservatory of Arts
(PN) Horn Clauses for Verification and Synthesis - Call for Papers
Call for Papers Horn Clauses for Verification and Synthesis (HCVS) July 19, 2015 - San Francisco, USA Submission deadlines: - paper submission: May 22, 2015 - paper notification: June 19, 2015 Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. This workshop aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences. Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas: - Analysis and verification of programs in various programming paradigms (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent) - Program synthesis - Program testing - Program transformation - Constraint solving - Type systems - Case studies and tools - Challenging problems We solicit regular papers describing theory and implementation of Horn-clause based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress and presentations covering previously published results that are of interest to the workshop. Invited speakers: - Ranjit Jhala, University of California at San Diego - Joxan Jaffar, National University of Singapore Program Committee: Elvira Albert (Complutense University of Madrid) Nikolaj Bjorner (Microsoft Research) Gregory J. Duck (National University of Singapore) Fabio Fioravanti (University of Chieti-Pescara) John Gallagher (Roskilde University and IMDEA-Software Madrid) Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University) - chair Radu Grigore (University of Oxford) Konstantin Korovin (Manchester University) Viktor Kuncak (EPFL) David Monniaux (CNRS/Verimag) Jorge A. Navas (NASA) - chair Corneliu Popeea (CQSE) Maurizio Proietti (IASI-CNR, Italy) Philipp Ruemmer (Uppsala University, Department of Information Technology) Andrey Rybalchenko (Microsoft Research) Valerio Senni (ALES srl) Peter Stuckey (University of Melbourne) Yakir Vizel (Princeton University) The submission format is up to 12 pages plus bibliography for regular papers and 1 to 3 pages (for work-in-progress), both in EPTCS format. Original accepted papers will be published electronically as a volume in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see http://www.eptcs.org/ Authors of accepted papers are required to ensure that at least one of them will be present at the workshop. Papers must be submitted through the EasyChair system using the web page: https://easychair.org/conferences/?conf=hcvs2015. [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) 3rd Workshop on Interpolation - Call for Papers
iPRA 2015 - THIRD WORKSHOP ON INTERPOLATION: FROM PROOFS TO APPLICATIONS CALL FOR CONTRIBUTIONS Date: July 18, 2015 Location: San Francisco, CA (co-located with CAV 2015) Web: http://forsyte.at/interpolation/ IMPORTANT DATES Submission deadline: May 7, 2015, AOE Notification:May 14, 2015 Workshop:July 18, 2015 ORGANISATION AND COMMITTEE Laura Kovacs and Georg Weissenbacher SCOPE Craig interpolation enjoys a continuing popularity in the field of verification. Historically, Craig's interpolation theorem has received ample attention in proof theory and mathematical logic as well as in complexity theory. The aim of the workshop is to bring together theoreticians and practitioners from different fields. We solicit submissions in form of an abstract of at most one page in PDF format. The authors of accepted abstracts are required to present their work at the workshop. There will be no published proceedings. We encourage submissions presenting work in progress, tools under development, as well as research of PhD students, such that the workshop can become a forum for active dialog between the groups involved in applications of interpolation. We also encourage contributions from outside the verification community. Presentations of recently published papers are also allowed and encouraged, but please indicate on your submission where the paper was published/presented. Relevant topics include (but are not limited to) applications of interpolation in: - Interpolating decision procedures - Proof theoretic approaches to interpolation - Proof systems and calculi for interpolation - Proof transformation techniques - Inductive Proofs - Logical Abduction - Interpolation techniques based on constraint solving, linear programming... - Alternative techniques for interpolation - Interpolation theorems (for theories and extensions, non-classical logic, ...) - Interpolation-based/Inductive invariant generation - Program analysis and verification - Tools for interpolation - Applications of Craig interpolation (verification, synthesis, automated reasoning, ...) - Complexity results and limitations ... SUBMISSION INSTRUCTIONS Abstracts (at most one page in PDF format) have to be submitted until May 7 via the EasyChair system: https://easychair.org/conferences/?conf=ipra15 The authors will be notified on May 14, 2015. There will be no formal workshop proceedings. FORMAT The workshop will feature - an invited talk by Arie Gurfinkel (SEI/CMU), - presentations (selected by a committee based on the submission of abstracts) by workshop participants, and - discussion and panel sessions. The program will be coordinated with the HCVS workshop, which takes place on July 19. REGISTRATION Registration for the workshop will be possible via the CAV registration site: http://i-cav.org/2015/ POSTER A poster is available on http://forsyte.at/interpolation. We kindly ask you to print and display a copy in your department/workplace. [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) Description Logics 2015 - Call for Papers
DL 2015: the 28th International Workshop on Description Logics, DL 2015 === The DL workshop is the major annual event of the description logic research community. It is the forum at which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences. The workshop will be held in Athens from June 7th to June 10th, 2015. Submission of papers under review for a conference with a double-blind submission policy == Extended abstracts of papers that are currently under revision for a conference with a double-blind submission policy (e.g., IJCAI) should be submitted anonymously, i.e., without names in the pdf file, to avoid violations of the double-blind submission policy. The names of the authors of such papers will not be revealed to the DL 2015 reviewers handling them. All other papers should list the author names in the pdf file, as usual for DL. Extended deadline == Paper registration deadline: March 9, 2015 (extended from March 2, 2015) Paper submission deadline: March 16, 2015 (extended from March 9, 2015) Notification of acceptance: April 17, 2015 Camera-ready copies: May 8, 2015 Workshop: June 7-10, 2015 Workshop Scope = We invite contributions on all aspects of description logics, including but not limited to: * Foundations of description logics: decidability and complexity of reasoning, expressive power, novel inference problems, inconsistency management, reasoning techniques, and modularity aspects * Extensions of description logics: closed-world and nonmonotonic reasoning, epistemic reasoning, temporal and spatial reasoning, procedural knowledge, query answering, reasoning over dynamic information * Integration of description logics with other formalisms: object-oriented representation languages, database query languages, constraint-based programming, logic programming, and rule-based systems * Applications and use areas of description logics: ontology engineering, ontology languages, databases, ontology-based data access, semi-structured data, graph structured data, linked data, document management, natural language, learning, planning, Semantic Web, and cloud computing * Systems and tools around description logics: reasoners, software tools for and using description logic reasoning (e.g. ontology editors, database schema design, query optimisation, and data integration tools), implementation and optimisation techniques, benchmarking, evaluation, modelling Invited Speakers = * Carsten Lutz (TU Bremen) * Axel Polleres (TU Wien) * Maarten de Rijke (University of Amsterdam) Submissions == * Submissions may be either full papers of up to 11 pages (excluding references) presenting original research or extended abstracts of at most 3 pages (excluding references). There is no page limit on the list of references. * All submissions must be formatted in the Springer LNCS style. * Extended abstracts of papers under review for a conference with a double-blind submission policy should be submitted anonymously. * Extended abstracts are designed only for authors who wish to announce results that have been published elsewhere, or which the authors intend to submit or have already submitted to a venue with an incompatible prior / concurrent publication policy. Papers presenting original research should be submitted as regular submissions. * A clearly marked appendix (e.g., with additional proofs or evaluation data) may optionally be appended. It will be read at the discretion of the reviewers and not included in the proceedings. It does not need to be in LNCS format. * Authors submitting extended abstracts are encouraged to include such an appendix, with sufficient material (e.g. copy of the already published paper or technical report) to judge the scientific merit of the work described in the extended abstract. * Submission page: http://www.easychair.org/conferences/?conf=dl2015 * Accepted papers and extended abstracts will be made available electronically in the CEUR Workshop Proceedings series (http://www.CEUR-ws.org/). * Accepted submissions, be they full papers or extended abstracts, will be selected for either oral or poster presentation at the workshop. Submissions will be judged solely based upon their content, and the type of submission will have no bearing on the decision between oral and poster presentation. Organisation == * Diego Calvanese, Free University of Bozen-Bolzano (Programme co-Chair) * Boris Konev, University of Liverpool (Programme co-Chair) * Giorgos Stamou, National Technical University of Athens (Workshop co-Chair) * Giorgos Stoilos, National Technical University of Athens (Workshop co-Chair) Resources = *
(PN) TESTS AND PROOFS - Deadline extended
* * 9th International Conference * on * TESTS AND PROOFS (TAP 2015) * * http://tap2015.in.tum.de/ * * Part of STAF 2015, L'Aquila, Italy, July 20-24, 2015 * http://www.disim.univaq.it/staf2015/ * * * Call for Papers * * Abstract submission: February 23, 2015 (extended) * Paper submission:February 27, 2015 (extended) * Scope = The TAP conference is devoted to the synergy of proofs and tests, to the application of techniques from both sides and their combination for the advancement of software quality. Testing and proving seem to be orthogonal techniques: Once a program has been proven to be correct then additional testing seems pointless; however, when such a proof in not feasible, then testing the program seems to be the only option. This view has dominated the research community for a long time, and has resulted in distinct communities pursuing the different research areas. The development of both approaches has led to the discovery of common issues and to the realization of potential synergy. Perhaps the use of model checking in testing was one of the first signs that a counterexample to a proof may be interpreted as a test case. Recent breakthroughs in deductive techniques such as satisfiability modulo theories, abstract interpretation, and interactive theorem proving have paved the way for new and practically effective methods of powering testing techniques. Moreover, since formal, proof-based verification is costly, testing invariants and background theories can be helpful to detect errors early and to improve cost effectiveness. Summing up, in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. The TAP conference aims to bring together researchers and practitioners working in the converging fields of testing and proving by offering a generous forum for the presentation of ongoing research, for tutorials on established technologies and for informal discussions. Topics of Interest == Topics of interest cover theory definitions, tool constructions and experimentations, and include among others: - Bridging the gap between concrete and symbolic techniques, e.g. using proof search in satisfiability modulo theories solvers to enhance various testing techniques - Transfer of concepts from testing to proving (e.g., coverage criteria) and from proving to testing - Program proving with the aid of testing techniques - Verification and testing techniques combining proofs and tests - Generation of test data, oracles, or preambles by deductive techniques such as: theorem proving, model checking, symbolic execution, constraint logic programming - Model-based testing and verification - Generation of specifications by deduction - Automatic bug finding - Debugging of programs combining static and dynamic analysis - Case studies combining tests and proofs - Domain specific applications of testing and proving to new application domains such as validating security protocols, vulnerability detection of programs, security - Testing of verification environments and reasoning engines like solvers and theorem provers - New approaches such as crowd-sourcing and serious games to infer intended semantics and assess correctness - Formal frameworks - Tool descriptions and experience reports Important Dates: Abstract submission: February 23, 2015 (extended) Paper submission: February 27, 2015 (extended) Notification: April 13, 2015 Camera-ready version: May 3, 2015 STAF conferences: July 20-24, 2015 Program Co-Chairs: === Jasmin C. Blanchette (TU Muenchen, Inria) Nikolai Kosmatov (CEA LIST) Program Committee: == Bernhard K. Aichernig Dirk Beyer Nikolaj Bjorner Jasmin C. Blanchette Achim D. Brucker Koen Claessen Robert Clariso Marco Comini Catherine Dubois Juhan Ernits Gordon Fraser Angelo Gargantini Christoph Gladisch Martin Gogolla Arnaud Gotlieb Reiner Haehnle Bart Jacobs Thierry Jeron Jacques Julliand Gregory Kapfhammer Nikolai Kosmatov Victor Kuliamin Panagiotis Manolios Karl Meinke Alexandre Petrenko Andrew Reynolds Martina Seidl Nikolai Tillmann T.H. Tse Margus Veanes Luca Vigano Burkhart Wolff Fatiha Zaidi Submission: === Please submit your papers via EasyChair: https://www.easychair.org/conferences/?conf=tap2015 [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:
(PN) CADE-25 Final Call for Papers
Berlin Program Committee Co-Chairs: Amy Felty University of Ottawa Aart MiddeldorpUniversity of Innsbruck Workshop, Tutorial, and Competition Co-Chairs: Jasmin Blanchette Technische Universität München Andrew ReynoldsEPFL Lausanne Publicity and Web Chair: Julian Röder Freie Universität Berlin Program Committee Carlos Areces Universidad Nacional de Córdoba Alessandro Armando University of Genova Christoph Benzmüller Freie Universität Berlin Josh Berdine Microsoft Research Jasmin Blanchette Technische Universität München Marta Cialdea MayerUniversita di Roma Tre Stephanie Delaune CNRS Gilles Dowek Inria Amy Felty University of Ottawa Reiner Hähnle Technical University of Darmstadt Stefan Hetzl Vienna University of Technology Marijn Heule The University of Texas at Austin Nao Hirokawa JAIST Ullrich HustadtUniversity of Liverpool Deepak Kapur University of New Mexico Gerwin Klein NICTA and UNSW Laura Kovács Chalmers University of Technology Carsten Lutz Universität Bremen Assia Mahboubi Inria Aart MiddeldorpUniversity of Innsbruck Albert OliverasTechnical University of Catalonia Nicolas PeltierCNRS Brigitte Pientka McGill University Ruzica Piskac Yale University André Platzer Carnegie Mellon University Andrew ReynoldsEPFL Lausanne Christophe Ringeissen LORIA-INRIA Renate Schmidt University of Manchester Stephan Schulz DHBW Stuttgart Georg Struth University of Sheffield Geoff SutcliffeUniversity of Miami Alwen Tiu Nanyang Technological University Freek Wiedijk Radboud University Nijmegen [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) CADE-25 Workshops- Calls for Papers
** The Fourth International Workshop on Proof eXchange for Theorem Proving (PxTP) == http://pxtp15.lri.fr Background == The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and also collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture. Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation and communication methods, standards, protocols, and programming interfaces. The workshop welcomes the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement. Topics == Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are: - applications that integrate reasoning tools (ideally with certification of the result); - translations between logics, proof systems, models; - distribution of proof obligations among heterogeneous reasoning tools; - algorithms and tools for checking and importing (replaying, reconstructing) proofs; - proposed formats for expressing problems and solutions for different classes of logic solvers (SAT, SMT, QBF, first-order logic, higher-order logic, typed logic, rewriting, etc.); - meta-languages, logical frameworks, communication methods, standards, protocols, and APIs connected to problems, proofs, and models; - comparison, refactoring, and optimization of proofs; - practical experiences, case studies, feasibility studies; - applications relying on importing proofs from automatic theorem provers, such as certified static analysis, proof-carrying code, or certified compilation; - data structures and algorithms for improved proof production in solvers (e.g., efficient proof representations). Submissions === Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages). Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers should describe previously unpublished work, and must be prepared using the LaTeX EPTCS class (http://style.eptcs.org/). Papers will be submitted via EasyChair, at the PxTP'2015 workshop page (http://www.easychair.org/conferences/?conf=pxtp2015). Accepted full papers will appear in an EPTCS volume. Important dates === - Abstract submission: Thu, May 7, 2015 - Paper submission: Thu, May 14, 2015 - Notification: Tue, June 16, 2015 - Camera ready versions due: Thu, June 25, 2015 - Workshop: August 2-3, 2015 Invited speakers (joint with the AMI 2015 workshop) === - Georges Gonthier (Microsoft Research) - Bart Jacobs (KU Leuven) Program committee = - Jesse Alama (Vienna University of Technology) - Peter Baumgartner (NICTA) - Jasmin Blanchette (TU Muenchen) - Guillaume Burel (CEDRIC, ENSIIE) - Evelyne Contejean (LRI, CNRS, Universite Paris Sud) - Cezary Kaliszyk (University of Innsbruck), co-chair - Ramana Kumar (University of Cambridge) - Dale Miller (Inria / LIX, Ecole polytechnique) - Bruno Woltzenlogel Paleo (Vienna University of Technology) - Andrei Paskevich (LRI, Universite Paris Sud), co-chair - Damien Pous (LIP, CNRS, ENS Lyon) - Geoff Sutcliffe (University of Miami) - Laurent Thery (Inria) - Cesare Tinelli (University of Iowa) - Josef Urban (Radboud University Nijmegen) Previous PxTP editions == - PxTP 2011 (http://pxtp2011.loria.fr/), affiliated with CADE-23 - PxTP 2012 (http://pxtp2012
(PN) TABLEAUX/FroCoS Call for Workshops
*** Apologies for multiple copies *** FIRST CALL FOR WORKSHOPS TABLEAUX/FroCoS 2015 The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods and The International Symposium on Frontiers of Combining Systems Wroclaw, Poland, September 20-25, 2015 GENERAL INFORMATION TABLEAUX 2015 and FroCoS 2015 will take place in Wroclaw, Poland, from September 20 to September 25, 2015. Workshops and tutorials will be held on September 19/20 and/or September 25. In the present call, we solicit proposals for workshops that are related to the two main conferences. Tutorials will be solicited in a separate call. Possible topics of workshops (the list is non-exhaustive) are: * automated reasoning with analytic tableaux and other methods (theory and applications) * model checking and BDDs * light-weight, flexible theorem proving methods * novel calculi for verification of mathematics and programs * classical and non-classical logics (modal, description, intuitionistic, linear, temporal, many-valued...) * combination of logics * implementation techniques: Data structures, efficient algorithms, performance measurement * combination and integration methods in SAT and SMT solving * combination of decision procedures, satisfiability procedures, constraint solving techniques, or logical frameworks * combinations and modularity in ontologies, term rewriting, knowledge representation, natural language semantics, and other areas * application of theorem proving and combination methods in teaching, verification, or security analysis The purpose of a workshop is to offer an opportunity for the presentation of novel ideas, ongoing research, and to discuss the state of the art of a given area in a less formal but more focused way than at the main conferences. Workshops are also a good opportunity for young researchers to present their own work in a friendly atmosphere. The format of a workshop is left to the organizers, with possible lengths being half a day, a full day, or two days. PROPOSAL SUBMISSION In order to submit a workshop proposal, please send a description of one or two pages in pdf format by email to Hans de Nivelle (nive...@ii.uni.wroc.pl). The proposal must at least contain the following information: * title of the workshop * organizers + contact person * expected number of participants * whether the workshop is by invitation only or open. * planned duration (1/2 day, 1 day, 2 days) * are there planned proceedings? * special requirements? The deadline for submitting workshop proposals is *** MARCH 2 2015 ***. Workshop proposals will be reviewed by the TABLEAUX and FroCoS chairs Carsten Lutz, Hans de Nivelle, and Silvio Ranise, possibly with help of additional reviewers. Decisions will be made within three weeks. Additional questions can be directed to any of the PC chairs (Carsten Lutz, Hans de Nivelle and Silvio Ranise). MORE INFORMATION For more information on the two events, please refer to the webpages http://tableaux2015.ii.uni.wroc.pl/ http://frocos2015.ii.uni.wroc.pl/ [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) 10th Ershov Informatics Conference, Call for Papers
CALL FOR PAPERS PSI: 10th Ershov Informatics Conference 25 - 27 August 2015, Innopolis, Kazan, Russia http://easychair.org/smart-program/PSI2015/ The Ershov Informatics Conference (the PSI Conference Series, 10th edition) is the premier international forum in Russia for research and applications in computer, software and information sciences. The conference brings together academic and industrial researchers, developers and users to discuss the most recent topics in the field. PSI provides an ideal venue for setting up research collaborations between the rapidly growing Russian informatics community and its international counterparts, as well as between established scientists and younger researchers. Local Organizers Tanya Stanko Innopolis University Inna Baskakova Innopolis University Publicity Chairs Timur Tsiunchuk Innopolis University Salvatore Distefano Politecnico di Milano Conference Chairs Bertrand Meyer ETH, Zurich Irina Virbitskaite A.P. Ershov Institute, Novosibirsk Steering Committee Dines Bjorner Technical University of Denmark Manfred Broy Technische Universitaet Muenchen Victor Ivannikov Institute for System Programming, Russian Academy of Sciences Ugo Montanari University of Pisa Programme Committee Chairs Manuel Mazzara Innopolis University Andrei Voronkov The University of Manchester Keynote speakers Hans-Ulrich Heiss, TUB, Germany Jane Hillston, University of Edinburgh, UK Helmut Veith, Vienna University of Technology, Austria Conference Topics 1. Foundations of Program and System Development and Analysis * Specification, validation, and verification techniques. * Program analysis, transformation and synthesis. * Semantics, logic and formal models of programs. * Partial evaluation, mixed computation, abstract interpretation, compiler construction. * Theorem proving and model checking. * Concurrency theory. * Static program analysis. * Modeling and analysis of real-time and hybrid systems. * Computer models and algorithms for bioinformatics. 2. Programming Methodology and Software Engineering * Object-oriented, aspect-oriented, component-based and generic programming. * Programming by contract. * Program and system construction for parallel and distributed computing. * Constraint programming. * Multi-agent technology. * System re-engineering and reuse. * Integrated programming environments. * Software architecture. * Software development and testing. * Model-driven system/software development. * Agile software development. * Software engineering methods and tools. * Service engineering, service oriented architecture. * Reverse engineering. * Reflection techniques. * Software bugs, aging and reliability models and countermeasures. * Program understanding and visualization. 3. Information Technologies * Data models. * Database and information systems. * Data mining, analytics. * Knowledge-based systems and knowledge engineering. * Bioinformatics engineering. * Ontologies and semantic Web. * Digital libraries, collections and archives, Web publishing. * Peer-to-peer data management. More generally, the conference welcomes novel scientific contributions in software-related areas, and application papers showing practical applications of research results. Important Dates * April 16, 2015: abstract submission * April 23, 2015: submission deadline * May 31, 2015: notification of acceptance * August 25-27, 2015: the conference dates * November 1, 2015: camera ready papers due Programme Committee Members Farhad Arbab, CWI and Leiden University, Netherlands David Aspinall, Univ. of Edinburgh, UK Marcello Maria Bersani, Politecnico di Milano, Italy Eike Best, Univ. of Oldenburg, Germany Nikolaj Bjrner, Microsoft Research, Redmond, USA Andrea Calì, Birbeck College, UK Mauro Caporuscio, Linnaeus University, Sweden Néstor Cataño, Madeira Univ., Portugal Gabriel Ciobanu, Romanian Academy, Iasi, Romania Volker Diekert, Univ. Stuttgart, Germany Salvatore Distefano, Politecnico di Milano, Italy Nicola Dragoni, DTU, Denmark and Örebro Univ., Sweden Schahram Dustdar, Vienna Univ. Technology, Austria Dieter Fensel, STI Innsbruck, Austria Carlo Furia, ETH, Switzerland Carlo Ghezzi, Politecnico di Milano, Italy Sergei Gorlatch, Univ. Muenster, Germany Jan Friso Groote, Eindhoven Univ. Tech., The Netherlands Arie Gurfinkel, Carnegie Mellon Univ., US Cliff Jones, Newcastle Univ., UK Joost-Pieter Katoen, RWTH Aachen Univ., Germany Konstantin Korovin, Univ. Manchester, UK Maciej Koutny, Newcastle Univ., UK Laura Kovacs, Chalmers Univ. Tech., Gothenburg, Sweden Gregory Kucherov, CNRS/LIGM, Marne-la-Vallee, France Johan Lilius, Abo Akademi Univ., Turku, Finland Anthony Widjaja Lin, Yale-NUS College, Singapore Zhiming Liu, Birmingham City University Jan Madsen, DTU Copenhagen, Denmark Rupak Majumdar, MPI, Kaiserslautern, Germany Klaus Meer, Tech. Univ. Cottbus, Germany Hernán Melgratti, Univ. de Buenos Aires, Argentina Torben Mogensen, Univ. Copenhagen, Denmark
(PN) CICM Call for Papers
Call for Papers Conference on Intelligent Computer Mathematics CICM 2015 13-17 July 2015 Washington DC, USA Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas. CICM has been held annually as a joint meeting since 2008, co-locating related conferences and workshops to advance work in these subjects. Previous meetings have been held in Birmingham (UK 2008), Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011), Bremen (Germany 2012), Bath (UK 2013), and Coimbra (Portugal 2014). This is a (short version of the) call for papers for CICM 2015, which will be held in Washington, D.C., 13-17 July 2015. The full version of the CFP is available from the conference web page at http://cicm-conference.org/2015/cicm.php ** The principal tracks of the conference will be: ** * Calculemus (Symbolic Computation and Mechanised Reasoning) Chair: Jacques Carette * DML (Digital Mathematical Libraries) Chair: Volker Sorge * MKM (Mathematical Knowledge Management) Chair: Cezary Kaliszyk * Systems and Data Chair: Florian Rabe Publicity chair is Serge Autexier. The local arrangements will be coordinated by the Local Arrangements Chairs, Bruce R. Miller (National Institute of Standards and Technology, USA) and Abdou Youssef (The George Washington University, Washington, D.C.), and the overall programme will be organized by the General Programme Chair, Manfred Kerber (U. Birmingham, UK). As in previous years, it is anticipated that there will be a number co-located workshops, including one to mentor doctoral students giving presentations. We also solicit for project descriptions and work-in-progress papers. ** Important Dates ** Conference submissions: Abstract submission deadline: 16 February 2015 Submission deadline: 23 February 2015 Reviews sent to authors:6 April2015 Rebuttals due: 9 April2015 Notification of acceptance:13 April2015 Camera ready copies due: 27 April2015 Conference: 13-17 July 2015 Work-in-progress and Doctoral Programme submissions: Submission deadline: (Doctoral: Abstract+CV) 4 May 2015 Notification of acceptance:25 May 2015 Camera ready copies due:1 June 2015 [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) CADE-25 Call for Papers, etc.
to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. At CADE-25 we also intend to award the best student paper (details will follow). IMPORTANT DATES Workshop/Tutorials/System Competitions: Submission deadline: 14 November 2014 Notification: 28 November 2014 Papers: Abstract deadline:16 February 2015 Submission deadline: 23 February 2015 Rebuttal phase: 15-18 April 2015 Notification: 26 April 2015 Final version:17 May 2015 Workshops and Tutorials: 1 August to 3 August (morning) 2015 Competitions: 1 to 7 August 2015 Conference: 3 August (afternoon) to 7 August 2015 SUBMISSION INSTRUCTIONS Proposals for workshops, tutorials, and system competitions should be uploaded via https://easychair.org/conferences/?conf=cade25workshopstutor Papers should be submitted via https://easychair.org/conferences/?conf=cade25 CADE-25 ORGANIZERS Conference Chair: Christoph Benzmüller Freie Universität Berlin Program Committee Co-Chairs: Amy Felty University of Ottawa Aart MiddeldorpUniversity of Innsbruck Workshop, Tutorial, and Competition Co-Chairs: Jasmin Blanchette Technische Universität München Andrew ReynoldsEPFL Lausanne Publicity and Web Chair: Julian Röder Freie Universität Berlin Program Committee Carlos Areces Universidad Nacional de Córdoba Alessandro Armando University of Genova Christoph Benzmüller Freie Universität Berlin Josh Berdine Microsoft Research Jasmin Blanchette Technische Universität München Marta Cialdea MayerUniversita di Roma Tre Stephanie Delaune CNRS Gilles Dowek Inria Amy Felty University of Ottawa Reiner Hähnle Technical University of Darmstadt Stefan Hetzl Vienna University of Technology Marijn Heule The University of Texas at Austin Nao Hirokawa JAIST Ullrich HustadtUniversity of Liverpool Deepak Kapur University of New Mexico Gerwin Klein NICTA and UNSW Laura Kovács Chalmers University of Technology Carsten Lutz Universität Bremen Assia Mahboubi Inria Aart MiddeldorpUniversity of Innsbruck Albert OliverasTechnical University of Catalonia Nicolas PeltierCNRS Brigitte Pientka McGill University Ruzica Piskac Yale University André Platzer Carnegie Mellon University Andrew ReynoldsEPFL Lausanne Christophe Ringeissen LORIA-INRIA Renate Schmidt University of Manchester Stephan Schulz DHBW Stuttgart Georg Struth University of Sheffield Geoff SutcliffeUniversity of Miami Alwen Tiu Nanyang Technological University Freek Wiedijk Radboud University Nijmegen [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) CAV Call for Papers
Call for Papers 27th International Conference on Computer Aided Verification (CAV 2015) July 18-24 2015, San Francisco, California http://i-cav.org/2015/ Aims and Scope CAV 2015 is the 27th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as biological systems and computer security. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer LNCS series. A selection of papers will be invited to a special issue of Formal Methods in System Design and the Journal of the ACM. Topics of interest include but are not limited to: *Algorithms and tools for verifying models and implementations *Hardware verification techniques *Deductive, compositional, and abstraction techniques for verification *Program analysis and software verification *Verification methods for parallel and concurrent hardware/software systems *Testing and run-time analysis based on verification technology *Applications and case studies in verification *Decision procedures and solvers for verification *Mathematical and logical foundations of practical verification tools *Verification in industrial practice *Algorithms and tools for system synthesis *Hybrid systems and embedded systems verification *Verification techniques for security *Formal models and methods for biological systems Paper Submission Submissions should contain original research and sufficient detail to assess the merits and relevance of the contribution. We welcome papers on theory, case studies and comparisons with existing experimental research, tool papers, as well as combinations of new theory with experimental evaluation. Similar to last year, we welcome both long tool papers and short papers of any kind. Tool papers should describe system and implementation aspects of a tool with a large (potential) user base (experiments not required, rehash of theory strongly discouraged). Papers describing tools that have already been presented (in any conference) will be accepted only if significant and clear enhancements to the tool are reported and implemented. Submissions reporting on case studies in an industrial context are strongly invited, and should describe details, weaknesses, and strengths in sufficient depth. Papers reproducing and comparing existing results experimentally do not require new theoretical insights. Examples of contributions of such papers are evaluations of existing results in a superior experimental setting and comparisons of methods that have not previously been thoroughly experimentally compared. Papers can be submitted in either a regular or a short format. *Regular Papers should not exceed 15 pages in LNCS format, not counting references. *Short Papers should not exceed 6 pages, not counting references. Short papers are encouraged for any subject that can be described within the page limit, and in particular for novel ideas without an extensive experimental evaluation. Accepted short papers will be accompanied by short presentations. An appendix can provide additional material such as details on proofs or experiments. The appendix is not guaranteed to be read or taken into account by the reviewers and it should not contain information necessary for the understanding and the evaluation of the presented work. Papers will be accepted or rejected in the category in which they were submitted, there will be no demotions from a regular to a short paper. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. Papers must be submitted in PDF format. Submission is done via EasyChair. Deadlines Deadlines are anywhere on earth *Abstract submission: January 30 2015 *Paper submission (firm): February 6 2015 *Author feedback/rebuttal period: March 23-26 2015 *Notification of acceptance/rejection: April 17 2015 *Final version due: May 1 2015 Chairs Daniel Kroening, University of Oxford, UK. Corina Pasareanu, Carnegie Mellon Silicon Valley/NASA Ames, USA. Program Committee Aws Albarghouthi, University of Wisconsin-Madison, USA Jade Alglave, University College London, UK Domagoj Babic, Google, USA Clark Barrett, New York University, USA Armin Biere, Johannes Kepler University, Austria Roderick Bloem, Graz
(PN) CADE-25 CFP/CFW/CFT/CFC
to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award. At CADE-25 we also intend to award the best student paper (details will follow). IMPORTANT DATES Workshop/Tutorials/System Competitions: Submission deadline: 14 November 2014 Notification: 28 November 2014 Papers: Abstract deadline:16 February 2015 Submission deadline: 23 February 2015 Rebuttal phase: 15-18 April 2015 Notification: 26 April 2015 Final version:17 May 2015 Workshops and Tutorials: 1 August to 3 August (morning) 2015 Competitions: 1 to 7 August 2015 Conference: 3 August (afternoon) to 7 August 2015 SUBMISSION INSTRUCTIONS Proposals for workshops, tutorials, and system competitions should be uploaded via https://easychair.org/conferences/?conf=cade25workshopstutor Papers should be submitted via https://easychair.org/conferences/?conf=cade25 CADE-25 ORGANIZERS Conference Chair: Christoph Benzmüller Freie Universität Berlin Program Committee Co-Chairs: Amy Felty University of Ottawa Aart MiddeldorpUniversity of Innsbruck Workshop, Tutorial, and Competition Co-Chairs: Jasmin Blanchette Technische Universität München Andrew ReynoldsEPFL Lausanne Publicity and Web Chair: Julian Röder Freie Universität Berlin Program Committee Carlos Areces Universidad Nacional de Córdoba Alessandro Armando University of Genova Christoph Benzmüller Freie Universität Berlin Josh Berdine Microsoft Research Jasmin Blanchette Technische Universität München Marta Cialdea MayerUniversita di Roma Tre Stephanie Delaune CNRS Gilles Dowek Inria Amy Felty University of Ottawa Reiner Hähnle Technical University of Darmstadt Stefan Hetzl Vienna University of Technology Marijn Heule The University of Texas at Austin Nao Hirokawa JAIST Ullrich HustadtUniversity of Liverpool Deepak Kapur University of New Mexico Gerwin Klein NICTA and UNSW Laura Kovács Chalmers University of Technology Carsten Lutz Universität Bremen Assia Mahboubi Inria Aart MiddeldorpUniversity of Innsbruck Albert OliverasTechnical University of Catalonia Nicolas PeltierCNRS Brigitte Pientka McGill University Ruzica Piskac Yale University André Platzer Carnegie Mellon University Andrew ReynoldsEPFL Lausanne Christophe Ringeissen LORIA-INRIA Renate Schmidt University of Manchester Stephan Schulz DHBW Stuttgart Georg Struth University of Sheffield Geoff SutcliffeUniversity of Miami Alwen Tiu Nanyang Technological University Freek Wiedijk Radboud University Nijmegen [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) 4th International SAT/SMT Summer School
=== CALL FOR PARTICIPATION Fourth International SAT/SMT Summer School Semmering, Austria, July 10-12, 2014 http://satsmt2014.forsyte.at/ === REGISTRATION: The registration deadline for the summer school is April 19, 2014. Full details of the registration procedure as well as travel and accommodation grants are available at the school website (http://satsmt2014.forsyte.at/). ABOUT: Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers have become the backbone of numerous applications in computer science, such as automated verification, artificial intelligence, program synthesis, security, product configuration, and many more. The summer school covers the foundational and practical aspects of SAT and SMT technologies and their applications. Besides providing a well structured introduction to SAT and SMT, this year's edition of the SAT/SMT Summer School covers timely topics and novel applications such as - parallel solvers, - non-linear arithmetic in SMT, - the IC3 model checking paradigm, - hardware and software verification, - proofs and Craig interpolation, - and cryptography, presented by distinguished speakers and experts in these fields. In addition to the theory sessions, we will have practicals in which the participants will work state-of-the-art tools and solvers. The fourth edition follows the schools that took place at MIT (SAT/SMT Solver Summer School 2011), at Fondazione Bruno Kessler (SAT/SMT School 2012) in Trento, Italy, and Aalto University in Espoo, Finland in 2013. The school location and schedule has been chosen to integrate nicely with the Vienna Summer of Logic (VSL 2014, seehttp://vsl2014.at/). As a reminder, VSL 2014 includes, among many other events: * the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) * the 26th International Conference on Computer Aided Verification (CAV 2014) * the 12th International Workshop on Satisfiability Modulo Theories (SMT 2014) * the 7th International Joint Conference on Automated Reasoning (IJCAR 2014) The Summer School program will feature four lectures per day, with the first two days dedicated to SAT and SMT, and the last to special topics. Two of the lectures will be organized as tutorials giving hands-on experience on SAT/SMT-based modelling. List of invited lectures: * Introduction to SAT, Daniel Le Berre * Practical Session SAT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila * Interpolation in SAT SMT, Philipp R?mmer * Parallel SAT Solving, Christoph Wintersteiger * Proofs in SAT and CSP, Ofer Strichman * Introduction to SMT, Alberto Griggio * Non-linear Arithmetic in SMT, Leonardo de Moura * Practical Session SMT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila * SMT for Cryptography Software Verification, Chao Wang * Hardware Verification with IC3, Fabio Somenzi * Software Verification with IC3, Nikolaj Bj?rner A more detailed program is available at the school website (http://satsmt2014.forsyte.at/). Organizers: Clark Barrett (New York University) Pascal Fontaine (Inria, Loria, University of Lorraine, France) Dejan Jovanovi? (SRI, U.S.) Georg Weissenbacher (TU Wien, Austria) [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) Vienna Summer of Logic Announcement
**Vienna Summer of Logic Announcement** In the summer of 2014, Vienna will host the largest event in the history of logic. The Vienna Summer of Logic (VSL) will consist of twelve large conferences and numerous workshops, attracting an expected number of 2500 researchers from all over the world. The conferences and workshops will deal with the main theme, logic, from three important aspects: logic in computer science, mathematical logic and logic in artificial intelligence. This unique event will be organized by the Kurt Goedel Society at Vienna University of Technology from July 9 to 24, 2014 (see website for more details: http://vsl2014.at) *Keynote Speakers* The VSL keynote speakers are Franz Baader (Technische Universitaet Dresden), Edmund Clarke (Carnegie Mellon University), Christos Papadimitriou (University of California, Berkeley) and Alex Wilkie (University of Manchester). Dana Scott (Carnegie Mellon University) will speak in the opening session. *Logic in Computer Science / Federated Logic Conference (FLoC)* - 26th International Conference on Computer Aided Verification (CAV) - 27th IEEE Computer Security Foundations Symposium (CSF) - 30th International Conference on Logic Programming (ICLP) - 7th International Joint Conference on Automated Reasoning (IJCAR) - 5th Conference on Interactive Theorem Proving (ITP) - Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th ACM/IEEE Symposium on Logic in Computer Science (LICS) - 25th International Conference on Rewriting Techniques and Applications (RTA) joint with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA) - 17th International Conference on Theory and Applications of Satisfiability Testing (SAT) - FLoC Workshops - FLoC Olympic Games (System Competitions) *Mathematical Logic* - Logic Colloquium 2014 - Logic, Algebra and Truth Degrees 2014 - The Infinity Workshop - Kurt Goedel Fellowship Competition *Logic in Artificial Intelligence* - 14th International Conference on Principles of Knowledge Representation and Reasoning (KR) - 27th International Workshop on Description Logics (DL) - 15th International Workshop on Non-Monotonic Reasoning (NMR) - International Workshop on Knowledge Representation for Health Care 2014 (KR4HC) *Kurt Goedel Research Prize Fellowship Competition* At the Vienna Summer of Logic, the Kurt Goedel Society will award three fellowship prizes endowed with 100.000 Euro each to the winners of the Kurt Goedel Research Prize Fellowship Competition Logical Mind: Connecting Foundations and Technology. *FLoC Olympic Games - Citius, Maius, Potentius* The Federated Logic Conference (FLoC) 2014 will host the 1st FLoC Olympic Games. Intended as a new FLoC tradition, the Games will bring together a multitude of established solver competitions by different research communities. In addition to the competitions, the Olympic Games will facilitate the exchange of expertise between communities, and increase the visibility and impact of state-of-the-art solver technology. The winners in the competition categories will be awarded Kurt Goedel medals at the FLoC Olympic Games award ceremonies. [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) Essays in Memory of Mark Stickel
CALL FOR PAPERS Making Automated Reasoning Practical: Essays in Memory of Mark Stickel Submission Deadline: March 1st, 2014 AIM This is a book of collected articles presenting research in all aspects of automated reasoning, in particular the design of automated reasoning systems and their applications. A common theme behind Mark Stickel's work was developing techniques for building better automated reasoning systems. His discoveries were ground-breaking and include AC-unification, reasoning modulo a theory, term indexing, and thorough development of the SNARK and PTTP provers. In 2002 he received the Herbrand award for all his work, the highest award in automated reasoning (http://www.cadeinc.org/). We would like to honour Mark's achievements by editing a Festschrift comprised of articles in the spirit of his research approach: developing fundamental techniques driven by practical applications and informed by rigorous theory. SCOPE We invite high-quality submissions on the general topic of automated reasoning and its applications, especially but not exclusively to the design of automated theorem proving systems, with connections to any of Mark Stickel's research areas: * Automated theorem proving, including deductive and abductive reasoning * Implementation of and practice with automated reasoners * Algorithmics for automated reasoners: unification, matching, rewriting, indexing * Integration of general-purpose reasoning with external procedures * Spatial and temporal reasoning * Inference control, theory reasoning, semantic guidance for automated reasoners * Application of automated reasoners in mathematics, logic, program synthesis, natural language, and natural sciences * SAT-solving * Applications related to formal methods PUBLICATION DETAILS It is planned that the book will be published as an LNAI Festschrift with Springer. SUBMISSION INSTRUCTIONS While it is expected that most of the papers will be regular technical papers, a few papers that combine scientific content with recollections of Mark Stickel's work and personality, as can be written by those who worked with him, are also sought. All papers will be refereed by anonymous peer reviewers, and read by the editors, according to the highest standards in terms of originality, significance, technical quality, and readability. Submissions must be in English and standard conforming pdf format. They must be unpublished and not submitted for publication elsewhere. However, significantly extended versions of papers published at conferences are welcome. Submissions of any length will be considered, but final versions may be limited by the editors depending on the totality of submissions. Authors are strongly encouraged to produce their papers in LaTeX. Formatting instructions and the LNCS style files can be obtained via http://www.springer.de/comp/lncs/authors.html. Electronic submission via EasyChair is open at https://www.easychair.org/conferences/?conf=festschriftmarkstick . SUBMISSION DEADLINE: March 1st, 2014 In order to facilitate the planning of the book, authors are invited to notify the editors as soon as possible of their intention to submit with proposed topic and length. Early submission would be especially helpful for completing the review process sooner. EDITORS Peter Baumgartner NICTA and Australian National University, http://users.cecs.anu.edu.au/~baumgart/ Richard Waldinger SRI International, http://www.ai.sri.com/~waldinge/ [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-19 - Calls for Short Papers and Workshop Papers
The 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning CALL FOR SHORT PAPERS and WORKSHOP PAPERS Stellenbosch, South Africa, 14-19 December 2013 www.LPAR-19.info The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 19th LPAR will be held in Stellenbosch, South Africa. --- * SHORT PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short papers reporting on interesting work in progress or providing system descriptions. They need not be original. Extended or revised versions of the short papers may be submitted concurrently with or after LPAR to another conference or a journal. Short papers are limited in length to 8 pages in the EasyChair format. Accepted papers will be published electronically as a volume in the EPiC series, see http://www.easychair.org/publications/?page=38379010. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The LaTeX, Microsoft Word and LibreOffice templates for the EPiC series may be downloaded from http://www.easychair.org/publications/?page=1594225690. Short papers must be submitted through the EasyChair system using the web page https://www.easychair.org/conferences/?conf=lpar19 Paper submission deadline: October 14th, 2013 Notification of acceptance: October 28th, 2013 Final version: November 11th, 2013 --- * WORKSHOP PAPERS LPAR-19 includes five associated workshops: + IWIL-10 - The 10th International Workshop on the Implementation of Logics Submission deadline: October 14, 2013 + APS-7 - The 7th International Workshop on Analytic Proof Systems Submission deadline: October 14, 2013 + ALCS - The 1st International Workshop on Algebraic Logic in Computer Science Submission deadline: passed + LRCM - The 1st Workshop on Logics and Reasoning for Conceptual Models Submission deadline: October 14, 2013 + ALFA-2 - The 2nd Workshop on Automata, Logic, Formal languages, and Algebra Submission deadline: passed Submissions are still being accepted for three of the workshops. For further details, please refer to the workshop web pages that are linked from the LPAR-19 web pages at www.LPAR-19.info . === [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-19 in South Africa - Paper Deadline
=== LPAR-19 CALL FOR PAPERS === The 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning Stellenbosch, South Africa, 14-19 December 2013 www.LPAR-19.info The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 19th LPAR will be held in Stellenbosch, South Africa. Logic is a fundamental organizing principle in nearly all areas in Computer Science. It runs a multifaceted gamut from the foundational to the applied. At one extreme, it underlies computability and complexity theory and the formal semantics of programming languages. At the other extreme, it drives billions of gates every day in the digital circuits of processors of all kinds. Logic is in itself a powerful programming paradigm, but it is also the quintessential specification language for anything ranging from real-time critical systems to networked infrastructures. Logical techniques link implementation and specification through formal methods such as automated theorem proving and model checking. Logic is also the stuff of knowledge representation and artificial intelligence. Because of its ubiquity, logic has acquired a central role in Computer Science education. Topics -- New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: * Abduction and interpolation methods * Automated reasoning * Constraint programming * Decision procedures * Description logics * Foundations of security * Hardware verification * Implementations of logic * Interactive theorem proving * Knowledge representation and reasoning * Logic and computational complexity * Logic and databases * Logic and games * Logic and machine learning * Logic and the web * Logic and types * Logic in artificial intelligence * Logic of distributed systems * Logic programming * Logical aspects of concurrency * Logical foundations of programming * Modal and temporal logics * Model checking * Non-monotonic reasoning * Ontologies and large knowledge bases * Probabilistic and fuzzy reasoning * Program analysis * Rewriting * Satisfiability checking * Satisfiability modulo theories * Software verification * Specification using logic * Unification theory Programme Chairs * Ken McMillan * Aart Middeldorp * Andrei Voronkov Conference Chairs * Bernd Fischer * Geoff Sutcliffe Workshop Chair -- * Laura Kovacs Submission Details -- Submissions of two kinds are welcome: * Regular papers that describe solid new research results. They can be up to 15 pages long in LNCS style, including figures and references, but excluding appendices (that reviewers are not required to read). * Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the LNCS style. Both types of papers can be electronically submitted in PDF via EasyChar: http://www.easychair.org/conferences/?conf=lpar19. Prospective authors are required to register a title and an abstract a week before the paper submission deadline (see below). Participation - Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Important Dates --- * Abstract submission: 22nd July * Paper submission: 2nd August * Notification of acceptance: 27th September * Camera-ready papers: 9th October * Conference: 14th-19th December === LPAR-19 WORKSHOPS === LPAR-19 will be preceded by four workshops in specialised areas of logic: * The 10th International Workshop on the Implementation of Logics - IWIL http://www.eprover.org/EVENTS/IWIL-2013.html * The 7th International Workshop on Analytic Proof Systems - APS http
(PN) 10th IWIL Workshop, in South Africa
10th International Workshop on the Implementation of Logics http://www.eprover.org/EVENTS/IWIL-2013.html The 10th International Workshop on the Implementation of Logics will be held on December 14th, 2013, colocated with the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Stellenbosch, South Africa. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, and non-monotonic logics + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Practical constraint handling + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full papers (up to 15 pages). Submissions should be made via EasyChair at http://www.easychair.org/conferences/?conf=iwil2012 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. Proceedings will be published as EasyChair Proceedings. If number and quality of the submissions warrant it, we plan to produce a special issue of a recognized journal on the topic of the workshop. Important Dates: Submission of papers/abstracts: October 14th, 2013 Notification of acceptance: November 11th, 2013 Camera ready versions due: December 2nd, 2013 Workshop:December 14th, 2013 Program committee: Stephan Schulz (Co-Chair) TU München Geoff Sutcliffe (Co-Chair) University of Miami Boris Konev (Co-Chair) University of Liverpool Leonardo de Moura Microsoft Research Peter Baumgartner NICTA/Australian National University Uwe WaldmannMPI für Informatik Guillaume Burel ENSIIE/Cedric Andrew Reynolds University of Iowa Tommi Junttila Aalto University Konstantin Korovin The University of Manchester Graham SteelINRIA [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-19 CFP and Workshops
=== LPAR-19 1st CALL FOR PAPERS CALL FOR WORKSHOP PROPOSALS === The 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning Stellenbosch, South Africa, 14-19 December 2013 www.LPAR-19.info This is the first call for papers for LPAR-19 and a call for workshop proposals. Information about workshop proposals is included at the end of this call. The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 19th LPAR will be held in Stellenbosch, South Africa. Logic is a fundamental organizing principle in nearly all areas in Computer Science. It runs a multifaceted gamut from the foundational to the applied. At one extreme, it underlies computability and complexity theory and the formal semantics of programming languages. At the other extreme, it drives billions of gates every day in the digital circuits of processors of all kinds. Logic is in itself a powerful programming paradigm, but it is also the quintessential specification language for anything ranging from real-time critical systems to networked infrastructures. Logical techniques link implementation and specification through formal methods such as automated theorem proving and model checking. Logic is also the stuff of knowledge representation and artificial intelligence. Because of its ubiquity, logic has acquired a central role in Computer Science education. Topics -- New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: * Abduction and interpolation methods * Automated reasoning * Constraint programming * Decision procedures * Description logics * Foundations of security * Hardware verification * Implementations of logic * Interactive theorem proving * Knowledge representation and reasoning * Logic and computational complexity * Logic and databases * Logic and games * Logic and machine learning * Logic and the web * Logic and types * Logic in artificial intelligence * Logic of distributed systems * Logic programming * Logical aspects of concurrency * Logical foundations of programming * Modal and temporal logics * Model checking * Non-monotonic reasoning * Ontologies and large knowledge bases * Probabilistic and fuzzy reasoning * Program analysis * Rewriting * Satisfiability checking * Satisfiability modulo theories * Software verification * Specification using logic * Unification theory Programme Chairs * Ken McMillan * Aart Middeldorp * Andrei Voronkov Conference Chairs * Bernd Fischer * Geoff Sutcliffe Workshop Chair -- * Laura Kovacs Submission Details -- Submissions of two kinds are welcome: * Regular papers that describe solid new research results. They can be up to 15 pages long in LNCS style, including figures and references, but excluding appendices (that reviewers are not required to read). * Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the LNCS style. Both types of papers can be electronically submitted in PDF via EasyChar: http://www.easychair.org/conferences/?conf=lpar19. Prospective authors are required to register a title and an abstract a week before the paper submission deadline (see below). Participation - Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Important Dates --- * Abstract submission: 22nd July * Paper submission: 2nd August * Notification of acceptance: 27th September * Camera-ready papers: 9th October * Conference: 14th-19th December Workshop Proposals -- LPAR-19 workshops will be held on 14th December either as one-day or half-day events. If you would like to propose a workshop for LPAR-19, please contact the workshop chair via email (lkov...@complang.tuwien.ac.at
(PN) CADE-24 Workshops
Call for Papers Workshops at CADE-24 -- Lake Placid, New York, 9-10 June, 2013 Short CFPs for the following CADE-24 workshops are attached: ADDCT - Automated Deduction: Decidability, Complexity, Tractability ARSEC - Automated Reasoning in Security ARiSVe - Automated Reasoning in Software Verification ESARAI - Empirically Successful Automated Reasoning with AI KInAR - Knowledge Intensive Automated Reasoning PxTP - Proof Exchange for Theorem Proving For the Workshop Methods for Modalities (M4M) respective Information will be distributed soon. Moreover, CADE-24 will host a StarExec meeting. = ADDCT == ADDCT - Automated Deduction: Decidability, Complexity, Tractability Decidability, and especially complexity and tractability of logical theories is extremely important for a large number of applications. Although general logical formalisms (such as predicate logic or number theory) are undecidable, decidable theories or decidable fragments thereof (sometimes even with low complexity) often occur in mathematics, in program verification, in the verification of reactive, real time or hybrid systems, as well as in databases and ontologies. It is therefore important to identify such decidable fragments and design efficient decision procedures for them. It is equally important to have uniform methods (such as resolution, rewriting, tableaux, sequent calculi, ...) which can be tuned to provide algorithms with optimal complexity. The goal of ADDCT is to bring together researchers interested in - identifying (fragments of) logical theories which are decidable, identifying fragments thereof which have low complexity, and analyzing possibilities of obtaining optimal complexity results with uniform tools; - analyzing decidability in combinations of theories and possibilities of combining decision procedures; - efficient implementations for decidable fragments; - application domains where decidability resp. tractability are crucial. Full Paper submission: March 26, 2013 Notification: April 26, 2013 Final versions: May 10, 2013 Workshop: June 10, 2013 More details: http://userpages.uni-koblenz.de/~sofronie/addct-2013/ = ARSEC == ARSEC - Automated Reasoning in Security Automated reasoning methods have become increasingly critical in many areas of security, from analyzing cryptographic protocols for flaws to analyzing access-control and privacy policies. This interaction is proving to be mutually beneficial: automated reasoning methods are finding new applications in security; and new automated reasoning methods, developed for security applications, are enriching the tools available to all areas of automated reasoning. ARSEC will bring together researchers interested in automated reasoning and security to present recent work (including work in progress) and to discuss new ideas and trends in the field. Possible topics include, but are not limited to: - Security Protocols - Security Policies - Privacy and Confidentiality - Intrusion Detection - Automated Reasoning techniques such as Paramodulation, Rewriting, Unification and Satisfiability Modulo Theories (SMT). Paper Submission: March 25th Workshop: June 9th 2013 More details: http://www.cs.albany.edu/~marshall/ARSEC/ = ARiSVe = ARiSVe - Automated Reasoning in Software Verification 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. Invited speaker: K. Rustan M. Leino (Microsoft Research) 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 More details: http://arisve2013.lri.fr = ESARAI = ESARAI - Empirically Successful Automated Reasoning with Artificial Intelligence The Empirically Successful Automated Reasoning with Artificial Intelligence (ESARAI) workshop will bring together two complementary groups of researchers: researchers in Automated Reasoning who employ Artificial Intelligence tools and
(PN) CADE-24 Workshop CFPs
Call for Papers Workshops at CADE-24 -- Lake Placid, New York, 9-10 June, 2013 Short CFPs for the following CADE-24 workshops are attached: ADDCT - Automated Deduction: Decidability, Complexity, Tractability ARiSVe - Automated Reasoning in Software Verification ESARAI - Empirically Successful Automated Reasoning with AI KInAR - Knowledge Intensive Automated Reasoning PxTP - Proof Exchange for Theorem Proving StarExec For the following two CADE-24 workshops respective information will be distributed soon: Methods for Modalities (M4M), Automated Reasoning in Crypto-Protocol Analysis = ADDCT == ADDCT - Automated Deduction: Decidability, Complexity, Tractability Decidability, and especially complexity and tractability of logical theories is extremely important for a large number of applications. Although general logical formalisms (such as predicate logic or number theory) are undecidable, decidable theories or decidable fragments thereof (sometimes even with low complexity) often occur in mathematics, in program verification, in the verification of reactive, real time or hybrid systems, as well as in databases and ontologies. It is therefore important to identify such decidable fragments and design efficient decision procedures for them. It is equally important to have uniform methods (such as resolution, rewriting, tableaux, sequent calculi, ...) which can be tuned to provide algorithms with optimal complexity. The goal of ADDCT is to bring together researchers interested in - identifying (fragments of) logical theories which are decidable, identifying fragments thereof which have low complexity, and analyzing possibilities of obtaining optimal complexity results with uniform tools; - analyzing decidability in combinations of theories and possibilities of combining decision procedures; - efficient implementations for decidable fragments; - application domains where decidability resp. tractability are crucial. Full Paper submission: March 26, 2013 Notification: April 26, 2013 Final versions: May 10, 2013 Workshop: June 10, 2013 More details: http://userpages.uni-koblenz.de/~sofronie/addct-2013/ = ARiSVe = ARiSVe - Automated Reasoning in Software Verification 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. Invited speaker: K. Rustan M. Leino (Microsoft Research) 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 More details: http://arisve2013.lri.fr = ESARAI = ESARAI - Empirically Successful Automated Reasoning with Artificial Intelligence The Empirically Successful Automated Reasoning with Artificial Intelligence (ESARAI) workshop will bring together two complementary groups of researchers: researchers in Automated Reasoning who employ Artificial Intelligence tools and techniques to support their automated reasoning research, and researchers in Artificial Intelligence who employ Automated Reasoning tools and techniques to support the artificial intelligence research. The workshop will offer mutually beneficial interactions, through the exposure of the two sides of the research to all. Additionally, the workshop will provide a focussed forum where the many interfaces between these two research fields can be presented and discussed. The workshop is soliciting research, position, applications and system description papers on combinations of AI and AR. Additionally, the workshop includes system and application demonstrations. Demonstrations of systems and applications described in paper presentations, and demonstrations of systems and applications without an accompanying paper, are both encouraged. Submission deadline - 22nd April Notification of acceptance - 13th May Final versions due - 20th May Workshop - 9th or 10th June More details: http://www.cs.miami.edu/~geoff/Conferences/ESARAI/ = KInAR == KInAR -
(PN) CADE-24 CFP and Workshops
Apologies for multiple copies -- CADE-24: CALL FOR PAPERS 24th International Conference on Automated Deduction June 9-14, 2013, Lake Placid, New York, USA http://www.cade-24.info/ Submission Deadline: 14 January 2013 CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference program features invited talks, paper presentations, system descriptions, workshops, tutorials, and system competitions, including the CADE ATP System Competition (CASC). CADE-24 invites high-quality submissions on the general topic of automated reasoning, including foundations, applications, implementations and practical experiences. * Logics of interest include: propositional, first-order, equational, classical, higher-order, non-classical, constructive, modal, temporal, many-valued, description, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof. * Paradigms of interest include: theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integrations. * Methods of interest include: resolution, superposition or paramodulation, completion, saturation, term rewriting, decision procedures and their combinations, model elimination, connection method, inverse method, tableaux, induction, proof planning, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including unification, matching, orderings, indexing, proof presentation and explanation, and search plans or strategies for inference control, including semantic guidance and AI-related methods. * Applications of interest include: analysis, verification and synthesis of software and hardware, formal methods, computer mathematics, computational logic, declarative programming, knowledge representation, deductive databases, natural language processing, computational linguistics, ontology reasoning, robotics, planning, and other areas of artificial intelligence. Detailed information on satellite events will be published in separate calls and on the conference website. PUBLICATION AND SUBMISSION The proceedings of the conference will be published in the Springer LNAI/LNCS series. Submissions can be made in the categories 'regular paper' (max 15 pages) and 'system description' (max 7 pages). Full system descriptions that provide in-depth presentation of original ideas in an implemented system can be submitted as regular papers. There is an expectation that proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments be available, via a reference to a website, or in an appendix of the paper. Reviewers will be encouraged to consider these additional materials, however it will be at their discretion to do it. All papers will be evaluated according to the highest standards in terms of originality, significance, technical quality, and readability. Submissions must be in English and standard conforming pdf format. Submissions must be unpublished and not submitted for publication elsewhere. Authors are strongly encouraged to produce their papers in LaTeX. Formatting instructions and the LNCS style files can be obtained via http://www.springer.de/comp/lncs/authors.html. The page for electronic submission via EasyChair is https://www.easychair.org/conferences/?conf=cade24. IMPORTANT DATES Title and abstract must be submitted before the paper. Abstract submission: 7 January 2013 Paper submission: 14 January 2013 Notification: 11 March 2013 Final version: 1 April 2013 Workshops and Tutorials: 9-10 June 2013 Competitions:9-14 June 2013 Conference: 11-14 June 2013 ORGANIZERS Conference Co-Chairs: Christopher A. Lynch Clarkson University Neil V. Murray University at Albany - SUNY Program Committee Chair: Maria Paola Bonacina Universita` degli Studi di Verona Workshop and Competition Chair: Christoph Benzmueller Freie Universitaet Berlin Tutorial Chair: Peter Baumgartner NICTA and Australian National University Publicity and Web Chair: Grant Olney Passmore Cambridge University and Edinburgh University PROGRAM COMMITTEE Alessandro Armando Universita` degli Studi di Genova FBK Trento, Italy Peter BaumgartnerNICTA Australian National University, Australia Christoph BenzmuellerFreie Universitaet Berlin, Germany Maria Paola Bonacina Universita` degli Studi di Verona, Italy (Chair) Cristina Borralleras Universitat de Vic, Spain Thierry Boy De La Tour Universite' de Grenoble, France Evelyne
(PN) CSL 2011 Call for Papers and Workshops
-- CALL FOR PAPERS AND WORKSHOP PROPOSALS CSL 2011 20th Annual Conference of the European Association for Computer Science Logic Bergen, Norway September 12-15, 2011 GENERAL INFORMATION Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. The Ackermann Award for 2011 will be presented to the recipients at CSL 2011. SCOPE Topics of interest include (but are not limited to): - automated deduction and interactive theorem proving - constructive mathematics and type theory - equational logic and term rewriting - automata and games, game semantics - modal and temporal logic - model checking - decision procedures - logical aspects of computational complexity - finite model theory - computational proof theory - logic programming and constraints - lambda calculus and combinatory logic - domain theory, - categorical logic and topological semantics - database theory - specification, extraction and transformation of programs - logical foundations of programming paradigms - logical aspects of quantum computing - verification and program analysis - linear logic - higher-order logic - nonmonotonic reasoning PROCEEDINGS The proceedings will be published in the series LIPIcs, Leibniz International Proceedings in Informatics. Each paper accepted by the Program Committee (PC) must be presented at the conference by one of the authors, and a final copy must be prepared according to LIPIcs guidelines (http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/). PAPER SUBMISSION Authors are invited to submit papers of not more than 15 pages in LIPIcs style presenting work not previously published. Papers are to be submitted through EasyChair: http://www.easychair.org/conferences/?conf=csl2011. Submitted papers must be in English and provide sufficient detail to allow the PC to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written intro- duction which is directed at all members of the program committee. Submission is in two phases with dates as given below. Papers must not be submitted concurrently to another conference with refereed proceedings; The PC chair should be informed of closely related work submitted to a conference or journal by March 19, 2011. Papers authored or coauthored by members of the PC are not allowed. WORKSHOPS Proposals for satellite workshops on more specialized topics are welcome and can be sent to cs...@eacsl.org IMPORTANT DATES Submission of title and abstract: March 27, 2011 Submission of full paper:April 3, 2011 Notification: May 30, 2011 Final paper due: June 17, 2011 Conference: September 12-15, 2011 PROGRAM COMMITTEE Samson Abramsky (Oxford) Andrea Asperti (Bologna) Franz Baader (Dresden) Matthias Baaz (Vienna) Johan van Benthem (Amsterdam/Stanford) Marc Bezem (Bergen, chair) Patrick Blackburn (Nancy) Andreas Blass (Michigan) Jan van den Bussche (Hasselt) Thierry Coquand (Gothenburg) Nachum Dershowitz (Tel Aviv) Valentin Goranko (Copenhagen) Erich Graedel (Aachen) Wiebe van der Hoek (Liverpool) Bart Jacobs (Nijmegen) Reinhard Kahle (Lisbon) Stephan Kreutzer (Oxford) Viktor Kuncak (Lausanne) Daniel Leivant (Indiana) Benedikt Loewe (Amsterdam) Jean-Yves Marion (Nancy) Eugenio Moggi (Genova) Albert Rubio (Barcelona) Anton Setzer (Swansea) Alex Simpson (Edinburgh) John Tucker (Swansea) Pawel Urzyczyn (Warsaw) Helmut Veith (Vienna) Andrei Voronkov (Manchester) ORGANIZING COMMITTEE Isolde Adler Marc Bezem Magne Haveraaen Michal Walicki Uwe Wolter CONFERENCE ADDRESS CSL 2011, Department of Informatics, University of Bergen, P.O.Box 7803, N-5020 Bergen, Norway http://www.eacsl.org/csl11 - [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) CSL 2010 - 2nd Call for Papers
Second Call for Papers CSL 2010 Annual Conference of the European Association for Computer Science Logic August 23-27, 2010, Brno, Czech Republic http://mfcsl2010.fi.muni.cz/csl Submission (title abstract): March 26, 2010 Submission (full paper):April 2, 2010 Notification: May 17, 2010 Final papers: June 6, 2010 Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. The 19th EACSL Annual Conference on Computer Science Logic (CSL 2010) and the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010) are federated and organized in parallel at the same place. The federated MFCS CSL 2010 conference has common plenary sessions and social events for all participants. The technical program and proceedings of MFCS 2010 and CSL 2010 are prepared independently. The MFCS CSL 2010 conference is accompanied by satellite workshops on more specialized topics. Suggested topics of interest include (but are not limited to) automated deduction and interactive theorem proving, constructive mathematics and type theory, equational logic and term rewriting, automata and games, modal and temporal logic, model checking, decision procedures, logical aspects of computational complexity, finite model theory, computational proof theory, logic programming and constraints, lambda calculus and combinatory logic, categorical logic and topological semantics, domain theory, database theory, specification, extraction and transformation of programs, logical foundations of programming paradigms, verification and program analysis, linear logic, higher-order logic, nonmonotonic reasoning. Proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of the LNCS series. Each paper accepted by the Programme Committee must be presented at the conference by one of the authors, and a final copy must be prepared according to Springer's guidelines. Submitted papers must be in Springer's LNCS style and of no more than 15 pages, presenting work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or journal by March 19, 2010. Papers authored or coauthored by members of the Programme Committee are not allowed. Papers will be submitted through the conference website. Submitted papers must be in English and provide sufficient detail to allow the Programme Committee to assess the merits of the papers. Full proofs may appear in a technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the program committee. The Ackermann Award for 2010 will be presented to the recipients at CSL'10. There will be a Special Issue of the Journal LMCS (Logical Methods in Computer Science) based on selected papers of CSL 2010. *** Programme Committee Armin Biere (Linz) Lars Birkedal (ITU, Denmark) Nikolaj Bjorner (Redmond) Manuel Bodirsky (Paris) Mikolaj Bojanczyk (Warsaw) Iliano Cervesato (Doha) Krishnendu Chatterjee (Klosterneuburg) Agata Ciabattoni (Vienna) Anuj Dawar (Cambridge, co-chair) Azadeh Farzan (Toronto) Georg Gottlob (Oxford) Martin Hofmann (Munich) Orna Kupferman (Jerusalem) Christof Loeding (Aachen) Joao Marques-Silva (Dublin) Tobias Nipkow (Munich) Prakash Panangaden (Montreal) R. Ramanujam (Chennai) Simona Ronchi della Rocca (Torino) Alex Simpson (Edinburgh) Pascal Tesson (Quebec) Helmut Veith (Vienna, co-chair) Yde Venema (Amsterdam) *** CSL/MFCS Plenary Speakers David Basin (Zurich) Herbert Edelsbrunner (Klosterneuburg) Erich Gr?adel (Aachen) Joseph Sifakis (Gieres) *** CSL Invited Speakers Peter O?Hearn (London) Jan Krajicek (Prague) Andrei Krokhin (Durham) Andrey Rybalchenko (Munich) Viktor Kuncak (Lausanne) *** Organizing Committee Jan Bouda (Brno, chair) *** Conference address MFCSL 2010 Faculty of Informatics Masaryk University, Botanicka 68a, 60200 Brno Czech Republic mfcsl2...@fi.muni.cz [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR-17 in Indonesia - Calls for Papers and Workshop Proposals
=== LPAR-17 CALL FOR PAPERS CALL FOR WORKSHOP PROPOSALS === The 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning Yogyakarta, Indonesia - October 10th-15th, 2010 http://www.computational-logic.org/lpar-17/Home.html The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 17th LPAR will be held in Yogyakarta, Indonesia. Logic is a fundamental organizing principle in nearly all areas in Computer Science. It runs a multifaceted gamut from the foundational to the applied. At one extreme, it underlies computability and complexity theory and the formal semantics of programming languages. At the other extreme, it drives billions of gates every day in the digital circuits of processors of all kinds. Logic is in itself a powerful programming paradigm, but it is also the quintessential specification language for anything ranging from real-time critical systems to networked infrastructures. Logical techniques link implementation and specification through formal methods such as automated theorem proving and model checking. Logic is also the stuff of knowledge representation and artificial intelligence. Because of its ubiquity, logic has acquired a central role in Computer Science education. Topics -- New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: * Automated reasoning * Verification * Interactive theorem proving and proof assistants * Model checking * Implementations of logic * Satisfiability modulo theories * Rewriting and unification * Logic programming * Satisfiability checking * Constraint programming * Decision procedures * Logic and games * Logic and the Web * Ontologies and large knowledge bases * Logic and databases * Modal and temporal logics * Program analysis * Foundations of security * Description logics * Non-monotonic reasoning * Uncertainty reasoning * Logics for vague and inconsistent data * Specification using logic * Logic in artificial intelligence * Logic and types * Logical foundations of programming * Logical aspects of concurrency * Logic and computational complexity * Knowledge representation and reasoning * Logic of distributed systems Programme Chairs * Chris Fermueller * Andrei Voronkov Submission Details -- Submissions of two kinds are welcome: * Regular papers that describe solid new research results. They can be up to 15 pages long in LNCS style, including figures and references, but excluding appendices (that reviewers are not required to read). * Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the LNCS style. Both types of papers can be electronically submitted in PDF via EasyChar: http://www.easychair.org/conferences/?conf=lpar17. Prospective authors are required to register a title and an abstract a week before the paper submission deadline (see below). Workshop Proposals -- LPAR-17 workshops will be held on October 10, either as one-day or half-day events. If you would like to propose a workshop for LPAR-17, please contact the workshop chair, Laura Kovacs, via email, by the proposal deadline (see below). Workshop proposals should contain the following data: * Name of the workshop. * Brief description of the workshop, including workshop topics. * Valid web address of the workshop. * Contact information of the workshop organizers. * An estimate of the audience size. * Proposed format of the workshop (for example, regular talks, tool demos, poster presentations, etc.). * Duration of the workshop (one-day or half-day). * Potential invited speakers (if any). * Procedures for selecting papers and participants. * Special technical or AV needs. Note that workshops will have to be financially
(PN) LPAR-16 deadline extended
CALL FOR PAPERS LPAR-16 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning April 25 - May 1, 2010 Dakar, Senegal http://www.lpar.net/lpar-16/ SUBMISSION DEADLINE EXTENDED TO 13th JANUARY The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 16th edition will be held in Dakar, Senegal. Logic is a fundamental organizing principle in nearly all areas in Computer Science. It runs a multifaceted gamut from the foundational to the applied. At one extreme, it underlies computability and complexity theory and the formal semantics of programming languages. At the other, it drives billions of gates every day in the digital circuits of processors of all kinds. Logic is in itself a powerful programming paradigm but it is also the quintessential specification language for anything ranging from real-time critical systems to networked infrastructures. Logical techniques link implementation and specification through formal methods such as automated theorem proving and model checking. Logic is also the stuff of knowledge representation and artificial intelligence. Because of its ubiquity, logic has acquired a central role in Computer Science education. Topics -- New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: * Automated reasoning * Verification * Interactive theorem proving and proof assistants * Model checking * Implementations of logic * Satisfiability modulo theories * Rewriting and unification * Logic programming * Satisfiability checking * Constraint programming * Decision procedures * Logic and the Web * Ontologies and large knowledge bases * Logic and databases * Modal and temporal logics * Program analysis * Foundations of security * Description logics * Non-monotonic reasoning * Specification using logics * Logic in artificial intelligence * Logic and types * Logical foundations of programming * Logical aspects of concurrency * Logic and computational complexity * Knowledge representation and reasoning * Logic of distributed systems Programme Chairs * Ed Clarke * Andrei Voronkov Programme Committee --- * Rajeev Alur * Matthias Baaz * Peter Baumgartner * Armin Biere * Nikolaj Bjorner * Iliano Cervesato * Agata Ciabattoni * Hubert Comon-Lundh * Nachum Dershowitz * Juergen Giesl * Guillem Godoy * Georg Gottlob * Jean Goubault-Larrecq * Reiner Haehnle * Claude Kirchner * Michael Kohlhase * Konstantin Korovin * Laura Kovacs * Orna Kupferman * Leonid Libkin * Aart Middeldorp * Luke Ong * Frank Pfenning * Andreas Podelski * Andrey Rybalchenko * Helmut Seidl * Geoff Sutcliffe * Ashish Tiwari * Toby Walsh * Christoph Weidenbach Submission Details -- Submissions of two kinds are welcome: * Regular papers containing new results; * Experimental papers describing implementation or evaluation of systems. All submitted papers must be original, and not submitted concurrently to a journal or another conference. The page limit for all papers is 15 pages using the EasyChair class file that can be obtained at http://www.easychair.org/easychair.zip. All papers must be submitted through the EasyChair system using the Web page http://www.easychair.org/conferences/?conf=3Dlpar16 Important Dates --- * Paper submission: January 13, 2010 * Notification of acceptance: March 1, 2010 * Proceedings version: March 15, 2010 * Short papers submission: March 17, 2010 * Short papers notification: March 25, 2010 * Conference: April 25-May 1, 2010 [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies
(PN) IJCAR in Australia, 1 month to go
--- IJCAR 2008 - The 4th International Joint Conference on Automated Reasoning Sydney, Australia, 10th - 15th August, 2008 http://2008.IJCAR.org ONLY ONE MONTH TO GO ... DOWN UNDER --- Call for Participation -- IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications. IJCAR 2008 is the 4th International Joint Conference on Automated Reasoning, and is a merger of the following leading conferences and workshops: + CADE (Conference on Automated Deduction), + FroCoS (Symposium on Frontiers of Combining Systems), + FTP (Workshop on First-order Theorem Proving) + TABLEAUX (Conference on Analytic Tableaux and Related Methods) Registration, accomodation, and travel/visa information is on the IJCAR 2008 web pages. - Book your flight to Sydney today! - --- Scientific Program -- + Presentation of 4 invited talks - Hubert Comon-Lundh, Nachum Dershowitz, Aarti Gupta, Carsten Lutz + Presentation of 26 regular research papers + Presentation of 13 system descriptions + Presentation of the Herbrand Award to Prof. Edmund Clarke, CMU. + Four workshops, four tutorials, the CADE ATP System Competition (CASC-J4) --- Social Events - + Welcome reception at the conference hotel. + Excursion to the amazing Blue Mountains + Conference banquet + CASQ-J4 - the CADE Squash Competition --- Contact: Peter Baumgartner (conference chair) [EMAIL PROTECTED] --- [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) IJCAR 2008 in Australia
--- IJCAR 2008 - The 4th International Joint Conference on Automated Reasoning Sydney, Australia, 10th - 15th August, 2008 http://2008.IJCAR.org --- Call for Participation -- IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications. IJCAR 2008 is the 4th International Joint Conference on Automated Reasoning, and is a merger of the following leading conferences and workshops: + CADE (Conference on Automated Deduction), + FroCoS (Symposium on Frontiers of Combining Systems), + FTP (Workshop on First-order Theorem Proving) + TABLEAUX (Conference on Analytic Tableaux and Related Methods) Registration, accomodation, and travel/visa information is on the IJCAR 2008 web pages. Book your flight to Sydney today! --- Scientific Program -- + Presentation of 4 invited talks + Presentation of 26 regular research papers + Presentation of 13 system descriptions + Presentation of the Herbrand Award to Prof. Edmund Clarke, CMU. + Four workshops, four tutorials, the CADE ATP System Competition (CASC-J4) --- Invited Speakers + Hubert Comon-Lundh Challenges in the Automated Verification of Security Protocols + Nachum Dershowitz Canonicity + Aarti Gupta Software Verification: Roles and Challenges for Automatic Decision Procedures + Carsten Lutz Query Answering in Description Logics --- Workshops, Tutorials There will be four workshops and four tutorials before IJCAR, 10th and 11th August. See their individual WWW pages, linked from the IJCAR WWW pages for more information. + Workshops - The 5th International Verification Workshop (VERIFY'08) - Practical Aspects of Automated Reasoning/ Evaluation of Systems for Higher Order Logic (PAAR/ESHOL) - Complexity, Expressibility, Decidability in Automated Reasoning (CEDAR'08) - Constraints in Formal Verification + Tutorials - Introduction to Nominal Isabelle - Christian Urban - Formal Methods in Use at Galois, Inc. - Joe Hurd - SMT Solvers in Program Analysis and Verification - Nikolaj Bjorner and Leonardo de Moura - Coalgebraic Logics and Applications (COALA) - Dirk Pattinson --- Social Events - + Welcome reception at the conference hotel. + Excursion to the amazing Blue Mountains + Conference banquet + CASQ-J4 - the CADE Squash Competition All are included in the conference package, as well as refreshment breaks and lunches for all main conference days. --- Student Travel Awards - Two award schemes that provide sponsorhips to support student attendance at IJCAR are available. See the IJCAR 2008 WWW pages for details. We are also organizing room sharing at the conference hotel. --- Contact: Peter Baumgartner (conference chair) [EMAIL PROTECTED] --- [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR submission deadline extended
, or to compare implemented systems. They can be at most 8 pages long in the LNCS style. Both types of papers can be electronically submitted by visiting http://www.easychair.org/conferences/?conf=lpar2008. Prospective authors are required to register a title andan abstract a week before the paper submission deadline (see below). As with the previous editions, the proceedings of LPAR'08 will be published in Springer-Verlag's Lecture Notes in Computer Science series. They will be available at the conference. In keeping with the tradition of LPAR, researchers and practioners are encouraged to report on interesting work in progress by submitting abstracts of up to 5 LNCS pages, to be selected for a short-paper session. These abstracts will not be printed in the proceedings of LPAR'08 and they have a separate submission deadline (see below). Participation - Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will be removed from the proceedings. Important Dates (updated) - Abstract submission deadline: 06 June 2008 - STRICT! Paper submission deadline:16 June 2008 - STRICT! Notification of acceptance: 29 August 2008 Camera-ready papers: 19 September 2008 Short paper submission deadline: 26 September 2008 LPAR'08 Workshops:22 November 2008 LPAR 2008:23-27 November 2008 Program Committee - * Franz Baader, TU Dresden (Germany) * Matthias Baaz, TU Vienna (Austria) * Peter Baumgartner, National ICT (Australia) * Josh Berdine, MSR Cambridge (UK) * Armin Biere,Johannes Kepler University (Austria) * Iliano Cervesato, Carnegie Mellon University (Qatar) - chair * Sagar Chaki,Carnegie Mellon SEI (US) * Hubert Comon-Lundh, ENS Cachan (France) * Javier Esparza, TU Munich (Germany) * Roberto Giacobazzi, University of Verona (Italy) * Jürgen Giesl, RWTH Aachen (Germany) * Orna Grumberg, Technion (Israel) * Thomas Henzinger, EPFL (Switzerland) * Joxan Jaffar, NUS (Singapore) * Claude Kirchner,INRIA LORIA (France) * Stephan Kreutzer, Oxford University (UK) * Orna Kupferman, Hebrew University (Israel) * Alexander Leitsch, TU Vienna (Austria) * Nicola Leone, University of Calabria (Italy) * Heiko Mantel, TU Darmstadt (Germany) * Cathy Meadows, Naval Research Laboratory (US) * Aart Middeldorp,University of Innsbruck (Austria) * John Mitchell, Stanford University (US) * Andreas Podelski, University of Freiburg (Germany) * Sanjiva Prasad, IIT Delhi (India) * Alexander Razborov, Russian Academy of Sciences (Russia) * Andrey Rybalchenko, MPI-SWS (Germany) * Ulrike Sattler, University of Manchester (UK) * Torsten Schaub, University of Potsdam (Germany) * Carsten Schürmann, IT University of Copenhagen (Denmark) * Helmut Seidl, TU Munich (Germany) * Henny Sipma,Stanford University (US) * Geoff Sutcliffe,University of Miami (US) * Ashish Tiwari, SRI (US) * Helmut Veith, TU Darmstadt (Germany) - chair * Andrei Voronkov,University of Manchester (UK) - chair Contact Information --- Email: [EMAIL PROTECTED] Web page: http://www.qatar.cmu.edu/lpar08 [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) LPAR Call for Papers
Lecture Notes in Computer Science series. They will be available at the conference. In keeping with the tradition of LPAR, researchers and practioners are encouraged to report on interesting work in progress by submitting abstracts of up to 5 LNCS pages, to be selected for a short-paper session. These abstracts will not be printed in the proceedings of LPAR'08 and they have a separate submission deadline (see below). Participation - Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will be removed from the proceedings. Important Dates --- Abstract submission deadline: 26 May 2008 Paper submission deadline:06 June 2008 Notification of acceptance: 29 August 2008 Camera-ready papers: 19 September 2008 Short paper submission deadline: 26 September 2008 LPAR'08 Workshops:22 November 2008 LPAR 2008:23-27 November 2008 Program Committee - * Franz Baader, TU Dresden (Germany) * Matthias Baaz, TU Vienna (Austria) * Peter Baumgartner, National ICT (Australia) * Josh Berdine, MSR Cambridge (UK) * Armin Biere,Johannes Kepler University (Austria) * Iliano Cervesato, Carnegie Mellon University (Qatar) - chair * Sagar Chaki,Carnegie Mellon SEI (US) * Hubert Comon-Lundh, ENS Cachan (France) * Javier Esparza, TU Munich (Germany) * Orna Grumberg, Technion (Israel) * Thomas Henzinger, EPFL (Switzerland) * Joxan Jaffar, NUS (Singapore) * Juergen Giesl, RWTH Aachen (Germany) * Claude Kirchner,INRIA LORIA (France) * Stephan Kreutzer, Oxford University (UK) * Orna Kupferman, Hebrew University (Israel) * Alexander Leitsch, TU Vienna (Austria) * Nicola Leone, University of Calabria (Italy) * Cathy Meadows, Naval Research Laboratory (US) * Heiko Mantel, TU Darmstadt (Germany) * John Mitchell, Stanford University (US) * Aart Middeldorp,University of Innsbruck (Austria) * Andreas Podelski, University of Freiburg (Germany) * Sanjiva Prasad, IIT Delhi (India) * Alexander Razborov, Russian Academy of Sciences (Russia) * Andrey Rybalchenko, MPI-SWS (Germany) * Ulrike Sattler, University of Manchester (UK) * Carsten Schuermann, IT University of Copenhagen (Denmark) * Helmut Seidl, TU Munich (Germany) * Henny Sipma,Stanford University (US) * Geoff Sutcliffe,University of Miami (US) * Ashish Tiwari, SRI (US) * Helmut Veith, TU Darmstadt (Germany) - chair * Andrei Voronkov,University of Manchester (UK) - chair Contact Information --- Email: [EMAIL PROTECTED] Web page: http://www.qatar.cmu.edu/lpar08 [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
(PN) Automated Reasoning in Mathematics
--- The CICM Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM) Call for Papers - Submission Deadline - Monday 5th May -- The CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM) will be held as part of the Conferences on Intelligent Computer Mathematics, in Birmingham, United Kingdom, 26th July - 2nd August, 2008. See the WWW page ... http://www.cs.miami.edu/~geoff/Conferences/ESARM/ This workshop will bring together practioners and researchers who are concerned with the development and application of automated reasoning for mathematics. The workshop will discuss only really running systems and applications, and not theoretical ideas that have not yet been translated into working software. More details are on the WWW page. Submission of papers for presentation at the workshop, and proposals for system and application demonstrations at the workshop, are now invited. Submissions will be refereed, and a balanced program of high-quality contributions will be selected. The selected contributions will be printed as workshop proceedings, and will also be published electronically. The submission deadline is 5th May, notification of acceptance is on 13th June, and final versions are due 7th July. Submission details are on the WWW page. We hope that you will submit a paper, and be part of ESARM. --- [[ Petri Nets World:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ:]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies:]] [[ petrinet@informatik.uni-hamburg.de ]]
