- finite-model-theory - lists.rwth-aachen.de

Call for Papers: JLAMP Special Issue on Relational and Algebraic Methods in Computer Science
by Walter Guttmann 10 Dec '18

10 Dec '18

OPEN CALL FOR PAPERS FOR JOURNAL SPECIAL ISSUE Relational and Algebraic Methods in Computer Science Special Issue of the Journal of Logical and Algebraic Methods in Programming (JLAMP) http://www.ramics-conference.org/ramics-2018-jlamp-cfp.pdf IMPORTANT DATES: Submission Deadline: 31 March 2019 Notification of Acceptance: late 2019/early 2020 TOPICS: Relational and algebraic methods belong to the core of computer science. This special issue aims to showcase the variety and relevance of recent developments in this field ranging from theory to applications. We invite submissions of high-quality original research articles in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to: * Theory - algebras such as semigroups, residuated lattices, semirings, Kleene algebras, relation algebras and quantales - their connections with program logics and other logics - their formalisation with theorem provers - their use in the theories of automata, concurrency, formal languages, games, networks and programming languages - the development of algebraic, algorithmic, category-theoretic, coalgebraic and proof-theoretic methods for these theories * Applications - tools and techniques for program correctness, specification and verification - quantitative and qualitative models and semantics of computing systems and processes - algorithm design, automated reasoning, network protocol analysis, social choice, optimisation and control - industrial applications While we welcome substantially extended versions of papers published in the proceedings of the RAMiCS 2018 conference (Springer LNCS 11194, https://www.springer.com/gp/book/9783030021481), this call is open to anyone interested in the field of relational and algebraic methods. SUBMISSION INSTRUCTIONS: All submissions will be evaluated solely with respect to their novelty, significance and technical quality according to the high standards of JLAMP. They must be in PDF format, adhere to the standard JLAMP guide for authors https://www.elsevier.com/journals/journal-of-logical-and-algebraic-methods-… and be uploaded on Elsevier's online EVISE system https://www.evise.com/profile/#/JLAMP/login selecting the issue type VSI: RAMiCS 2018 Deviation from these requirements may lead to immediate rejection. GUEST EDITORS: Jules Desharnais (Université Laval, Québec, Canada) Walter Guttmann (University of Canterbury, New Zealand) Stef Joosten (Open University of the Netherlands)

1 0

[fm-announcements] SPIN 2019 in Beijing - Call for Papers and Participation
by Havelund, Klaus (348B) 08 Dec '18

08 Dec '18

SPIN 2019 24th International Symposium on Model Checking of Software Beijing, China, July 15-19, 2019 https://conf.researchr.org/home/spin-2019 Co-located with ISSTA 2019 ________________________________ The 26th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation. Topics of interest include, but are not limited to: * Formal verification techniques for automated analysis of software * Formal analysis for modeling languages, such as UML/state charts * Formal specification languages, temporal logic, design-by-contract * Model checking * Automated theorem proving, including SAT and SMT * Verifying compilers * Abstraction and symbolic execution techniques * Static analysis and abstract interpretation * Combination of verification techniques * Modular and compositional verification techniques * Verification of timed and probabilistic systems * Automated testing using advanced analysis techniques * Combination of static and dynamic analyses * Derivation of specifications, test cases, or other useful material via formal analysis * Case studies of interesting systems or with interesting results * Engineering and implementation of software verification and analysis tools * Benchmark and comparative studies for formal verification and analysis tools * Formal methods education and training * Insightful surveys or historical accounts on topics of relevance to the symposium ________________________________ Invited Speakers ________________________________ Kim G. Larsen, Aalborg University Kuldeep S. Meel, National University of Singapore Call for Papers The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, empirical evaluation, and education. History: The SPIN symposium originated as a workshop focusing on explicit state model checking, specifically as related to the Spin model checker. However, over the years it has evolved to a broadly scoped symposium for software analysis using any automated techniques, including model checking, automated theorem proving, and symbolic execution. An overview of the previous SPIN symposia (and early workshops) can be found at: http://spinroot.com/spin/symposia. SPIN 2019 will be organized as an ACM SIGSOFT event, colocated with the International Symposium on Software Testing and Analysis (ISSTA 2019): https://conf.researchr.org/home/issta-2019. ________________________________ Submission Guidelines ________________________________ The contributions to SPIN 2019 will be published as ACM Proceedings, and should be submitted in the ACM Conference Format: https://www.acm.org/publications/proceedings-template (please use the sigconf template). Submissions must be original and should not have been published previously or be under consideration for publication while being evaluated for this symposium. Authors are required to adhere to the ACM Policy and Procedures on Plagiarism and the ACM Policy on Prior Publication and Simultaneous Submissions. * We are soliciting three categories of papers: * Full Research Papers describing fully developed work and complete results (16 pages – references are not included in this limit); * Short Papers presenting tools, technology, experiences with lessons learned, new ideas, work in progress with preliminary results, and novel contributions to formal methods (6 pages – references are not included in this limit). * Tool Demo Papers presenting the foundations, capabilities, application domains and relevant examples using the tools, with a clear description of what is expected to be shown in a live demonstration (4 pages to describe the tool foundations, features and use examples, plus an appendix explaining the content of the demo). Papers should be submitted via the EasyChair SPIN 2019 submission website: https://easychair.org/conferences/?conf=spin19. A selection of papers will be invited to a special issue of the International Journal on Software Tools for Technology Transfer (STTT). ________________________________ Important Dates ________________________________ * Please keep in mind the following dates for submission: * Paper Submission: April 5th, 2019 (23:59:59 Anywhere on Earth) * Author Notification: April 27th, 2019 * Camera-Ready Paper: May 2019 * Symposium: July 15-19, 2019 --- To opt-out from this mailing list, send an email to fm-announcements-request(a)lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner(a)lists.nasa.gov

1 0

Call for Applications: Helmut Veith Stipend for Female Master´s Students in Computer Science at TU Wien - November 30, 2019
by Mihaela Rozman 06 Dec '18

06 Dec '18

Helmut Veith Stipend for Women in Computer Science Deadline: November 30, 2019 Female students in the field of computer science (CS) who plan to pursue (or are currently pursuing) one of the masters programs in Computer Science at the Vienna University of Technology TU Wien taught in English are invited to apply for the annually awarded Helmut Veith Stipend. The annually awarded Helmut Veith Stipend for female master students is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. Professor Helmut Veith (1971-2016). The Helmut Veith Stipend was established with generous support of TU Wien, Wolfgang Pauli Institute and with contributions by family and friends of the late Helmut Veith. BENEFITS -EUR 6000 per year -Waiver of tuition fees at TU Wien LOCATION OF MASTER STUDY For study in Austria, at Vienna University of Technology TU Wien FOR FIELD OF STUDY Applicants must be eligible for admission to one of the masters programs in computer science at Vienna University of technology - TU Wien that are taught in English. In 2018/2019 and 2019/2020 those are: Master in Logic and Computation Master in Business Informatics European Master in Computational Logic Master in Computer Engineering (Technische Informatik) Master in Data Science Master in Media and Human-Centered Computing APPLICATION Applications for funding can be filed after, before or in parallel with the admissions process. Your application must be submitted electronically to master(a)logic-cs.at as a single PDF document, by November 30, 2019. DEADLINE November 30, 2018. INQUIRES Electronically to master(a)logic-cs.at WEBSITE http://www.vcla.at/helmut-veith-stipend/

1 0

WORDS 2019, 1st call for papers
by Words 2019 28 Nov '18

28 Nov '18

*We apologize if you received this email several times. To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line.* WORDS 2019 12th International Conference Loughborough, September 9–13, 2019 http://words2019.lboro.ac.uk *Announcement* WORDS is a biannual international conference covering the mathematical theory of words (sequences of symbols) from all points of view: combinatorial, algebraic, algorithmic, as well as its applications to biology, linguistics, physics, and others. The previous WORDS conferences have taken place in Rouen (1997, 1999), Palermo (2001), Turku (2003, 2013), Montreal (2005, 2017), Marseille (2007), Salerno (2009), Prague (2011), and Kiel (2015). The 12th International Conference on Words, WORDS 2019 will take place on September 9-13 2019 at Loughborough University, UK (http://www.lboro.ac.uk/departments/compsci/). Co-chairs of this edition are Robert Mercaș and Daniel Reidenbach. *Invited Speakers* Antonio Restivo (Palermo) Florin Manea (Kiel) Svetlana Puzynina (St. Petersburg) Antonio Restivo (Palermo) Gwenaël Richomme (Montpellier) Aleksi Saarela (Turku) Kristina Vuskovic (Leeds) *Program Committee* Marie-Pierre Béal (Paris) Srecko Brlek (Montreal) Émilie Charlier (Liège) Volker Diekert (Stuttgart) Gabriele Fici (Palermo) Anna Frid (Marseille) Amy Glen (Murdoch) Štěpán Holub (Prague) Shunsuke Inenaga (Kyushu) Robert Mercas (Loughborough) co-chair Dirk Nowotka (Kiel) Jarkko Peltomäki (Turku) Edita Pelantová (Prague) Narad Rampersad (Winnipeg) Daniel Reidenbach (Loughborough) co-chair Jeffrey Shallit (Waterloo) Arseny Shur (Yekaterinburg) *Important dates* Submission deadline: April 12, 2019 Notification to authors: May 20, 2019 Deadline for final versions: June 3, 2019 Conference: September 9–13, 2019 *Submission guidelines* Submitted papers should not exceed 12 pages and be prepared according to the following guidelines and LNCS-style LaTeX2e. All proofs omitted due to space constraints should be given in an appendix or made accessible through a reliable link to a freely available electronic preprint (updated before submission). These will be read at the discretion of the program committee. Only original submission which have not been submitted for publication elsewhere will be considered. Papers should be submitted electronically in PDF through the EasyChair system: https://easychair.org/conferences/?conf=words2019 *Contact* Words2019(a)lboro.ac.uk The conference is organised by the Department of Computer Science, School of Science, Loughborough University, UK.

1 0

FSCD 2019 Second Call for Papers
by Sandra Alves 27 Nov '18

27 Nov '18

(Apologies for multiple copies of this announcement. Please circulate.) --------------- Updated information: Invited speakers --------------- CALL FOR PAPERS Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019) 24 -- 30 June 2019, Dortmund, Germany http://easyconferences.eu/fscd2019/ <http://easyconferences.eu/fscd2019/> IMPORTANT DATES --------------- All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered. Titles and Short Abstracts: 8 February 2019 Full Papers: 11 February 2019 Rebuttal period: 28 March -- 1 April 2019 Authors Notification: 8 April 2019 Final version for proceedings: 22 April 2019 FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation (e.g. quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g. blockchain protocols or deep learning algorithms). Suggested, but not exclusive, list of topics for submission are: 1. Calculi: Rewriting systems, Lambda calculus, Concurrent calculi, Logics, Type theory, Homotopy type theory, Logical frameworks, Quantum calculi 2. Methods in Computation and Deduction: Type systems; Induction and coinduction; Matching, unification, completion and orderings; Strategies; Tree automata; Model checking; Proof search and theorem proving; Constraint solving and decision procedures 3. Semantics: Operational semantics; Abstract machines; Game Semantics; Domain theory; Categorical models; Quantitative models 4. Algorithmic Analysis and Transformations of Formal Systems: Type inference and type checking; Abstract interpretation; Complexity analysis and implicit computational complexity; Checking termination, confluence, derivational complexity and related properties; Symbolic computation 5. Tools and Applications: Programming and proof environments; Verification tools; Proof assistants and interactive theorem provers; Applications in industry (e.g. design and verification of critical systems); Applications in other sciences (e.g. biology) 6. Semantics and verification in new challenging areas: Certification; Security; Blockchain protocols; Data bases; Deep learning and machine learning algorithms; Planning INVITED SPEAKERS ----------- * Beniamino Accattoli (INRIA, Paris, France) https://sites.google.com/site/beniaminoaccattoli/ <https://sites.google.com/site/beniaminoaccattoli/> * Amy Felty (University of Ottawa, Canada) http://www.site.uottawa.ca/~afelty/ <http://www.site.uottawa.ca/~afelty/> * Sarah Winkler (University of Innsbruck, Austria) http://cl-informatik.uibk.ac.at/users/swinkler/ <http://cl-informatik.uibk.ac.at/users/swinkler/> * Hongseok Yang (KAIST, Korea) https://sites.google.com/view/hongseokyang/ <https://sites.google.com/view/hongseokyang/> PUBLICATION ----------- The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. SUBMISSION GUIDELINES --------------------- Submissions can be made in two categories. Regular research papers are limited to 15 pages (including references, with the possibility to add an annex for technical details, e.g.\ proofs) and must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages (including references) and must present new software tools in which FSCD topics play an important role, or significantly new versions of such tools. Submissions must be formatted using the LIPIcs style files and submitted via EasyChair. Complete instructions on submitting a paper can be found on the conference web site: http://easyconferences.eu/fscd2019/ <http://easyconferences.eu/fscd2019/> BEST PAPER AWARD BY JUNIOR RESEARCHERS -------------------------------------- The program committee will consider declaring this award to a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. Other authors should declare to the PC Chair that at least 50% of contribution is made by the junior researcher(s). SPECIAL ISSUE ------------- Authors of selected papers will be invited to submit an extended version for a special issue of Logical Methods in Computer Science. PROGRAM COMMITTEE ----------------- H. Geuvers, Radboud U. Nijmegen (Chair) Z. Ariola, U. of Oregon M. Ayala Rincón, U. of Brasilia A. Bauer, U. of Ljubljana F. Bonchi, U. of Pisa S. Broda, U. of Porto U. Dal Lago, U. of Bologna & Inria U. De'Liguoro, U. of Torino D. Kapur, U. of New Mexico P. Dybjer, Chalmers U. of Technology M. Fernandez, King's College London J. Giesl, RWTH Aachen N. Hirokawa, JAIST S. Lucas, U. Politecnica de Valencia A. Middeldorp, U. of Innsbruck F. Pfenning, Carnegie Mellon U. B. Pientka, McGill U. J. van de Pol, Aarhus U. & U. of Twente F. van Raamsdonk, VU Amsterdam C. Schürmann, ITU Copenhagen P. Severi, U. of Leicester A. Silva, U. College London S. Staton, Oxford U. T. Streicher, TU Darmstadt A. Stump, U. of Iowa N. Tabareau, Inria S. Tison, U. of Lille A. Tiu, Australian National U. T. Tsukada, U. of Tokyo J. Urban, CTU Prague P. Urzyczyn, U. of Warsaw J. Waldmann, Leipzig U. of Applied Sciences CONFERENCE CHAIR ---------------- Jakob Rehof, TU Dortmund LOCAL WORKSHOP CHAIR -------------------- Boris Düdder, U. of Copenhagen STEERING COMMITTEE WORKSHOP CHAIR -------------------------------- J. Vicary, Oxford U. PUBLICITY CHAIR --------------- Sandra Alves , Porto U. FSCD STEERING COMMITTEE ----------------------- S. Alves (Porto U.), M. Ayala-Rincón (Brasilia U.) C. Fuhs (Birkbeck, London U.) D. Kesner (Chair, Paris U.) H. Kirchner (Inria) N. Kobayashi (U. Tokyo) C. Kop (Radboud U. Nijmegen) D. Miller (Inria) L. Ong (Chair, Oxford U.) B. Pientka (McGill U.) S. Staton (Oxford U.)

1 0

Postdoc & PhD positions at Univ. of Bremen
by Sebastian Maneth 26 Nov '18

26 Nov '18

The Database Group at University of Bremen announces: - one position at the level of Postdoc - one position at the level of PhD student Both positions are initally for the duration of 3 years, and can be extended by two more years. The positions include a teaching load of 4h per week during teaching periods. For further questions and applications please contact: maneth(a)uni-bremen.de More details on these positions can be found below (details for the PhD position are in German, but non German speakers may apply). Best regards, Sebastian Maneth --- (1) PostDoc Position: At the University of Bremen in the department of mathematics and informatics there is a full PostDoc position - under the condition of job release – available, commencing at the earliest convenience, for a duration of initially three years. The position is at the level of Wissenschaftliche/r Mitarbeiter/in Entgeltgruppe 13 TV-L within the group "databases" headed by prof. Sebastian Maneth. The research topics of this group lie at the intersection of databases, formal methods, and automata theory. The position is funded by the university and includes a teaching load of 4 hours per week during teaching periods (teaching may be in English). The employment is fixed-term and governed by the Act of Academic Fixed-Term Contract, §2 I (Wissenschaftszeitvertragsgesetz – WissZeitVG). Therefore, candidates may only be considered for appointment if they still have the respective qualification periods available in accordance with § 2 (1) WissZeitVG. Besides teaching the main tasks of the position are to carry out research and to publish research results within the areas mentioned below. The position serves for further scientific qualification with the aim of habilitation. Qualification: a PhD in computer science or mathematics and research experience in at least on of the following areas: - formal methods and automata - databases - algorithms We expect good programming skills and eagerness to carry out and/or coordinate programming tasks. We specifically support the employment of women and encourage qualified female researchers to apply. Disabled applicants with equal qualification will be favoured for the positions. Applicants with a migration background are welcome. Please send your application (consisting of a cover letter stating the name of a referee who is willing to write a letter of recommendation, your CV, your motivation to work in this area, your master's thesis, copies of transcripts showing your courses and grades) until 7th December 2018 by indicating the job A294/18 to (applications sent after this date will also be considered): Universitaet Bremen Fachbereich Mathematik/Informatik Prof. Dr. Sebastian Maneth Bibliothekstrasse 1 28359 Bremen GERMANY or in electronic form (one PDF file) to maneth(a)uni-bremen.de We kindly ask you to send us only copies of your application documents (no folders) because they will not be returned for economic reasons. --- (2) PhD position An der Universität Bremen ist im Fachbereich 3 (Mathematik und Informatik) zum nächstmöglichen Termin (vorbehaltlich der Stellenfreigabe) befristet auf drei Jahre eine ganze Stelle zu besetzen: Wissenschaftliche/r Mitarbeiter/in Informatik - Entgeltgruppe 13 TV-L Die Befristung erfolgt zur wissenschaftlichen Qualifikation nach § 2 Abs. 1 WissZeitVG (Wissenschaftszeitvertragsgesetz). Demnach können nur Bewerberinnen und Bewerber berücksichtigt werden, die noch in dem entsprechenden Umfang über Qualifizierungszeiten nach § 2 Abs. 1 WissZeitVG verfügen. Die Stelle ist der Arbeitsgruppe „Datenbanken“ (DB) von Prof. Sebastian Maneth zugeordnet, deren Forschungsgebiete unter anderem Datenkomprimierung, formale Methode und die Anwendung von Automatentheorie innerhalb der Datenbanken umfassen. Es handelt sich um eine aus Mitteln der Universität finanzierte Landesstelle, die mit einer Lehrverpflichtung von 4 SWS verbunden ist. Die Stelle ist für Promovierende geeignet und kann für die eigene wissenschaftliche Qualifikation genutzt werden (Promotion). Die Stelleninhaberin/der Stelleninhaber soll die AG DB in Forschung und Lehre verstärken. In der Lehre wird Engagement bei der Durchführung von Tutorien zu Grundlehrveranstaltungen in Datenbanken erwartet. Bei vorhandener Qualifikation können auch eigene Lehrveranstaltungen angeboten werden. Voraussetzung ist ein abgeschlossenes Hochschulstudium (Master) der Informatik oder eine vergleichbare Qualifikation. Gute Grundkenntnisse in mindestens einem der folgenden für die AG derzeit relevanten Forschungsthemen sind erforderlich: - formale Methoden (z.B. Transducer) für “data wrangling” - automatische Lernverfahren für Datensäuberungs- und “wrangling”-Prozesse - Transformationen und Abfragen auf heterogenen Daten - Schemasprachen für Graphdaten (z.B. RDF) - Algorithmen auf Grammatik-komprimierten Graphen. Es werden gute Programmierkenntnisse in einer der Programmiersprachen Scala, C++ oder Java erwartet, so wie das Interesse und die Bereitschaft Programmieraufgaben innerhalb der obigen Forschungsthemen zu übernehmen und/oder zu koordinieren. Die Universität Bremen fördert die Einstellung von Frauen. Es wird begrüßt, wenn sich der Anteil von Frauen erhöht. Aus diesem Grund fordern wir vor allem qualifizierte Wissenschaftlerinnen nachdrücklich auf, sich zu bewerben. Schwerbehinderten Bewerberinnen/Bewerbern wird bei gleicher Eignung der Vorrang gegeben. Bewerbungen von Menschen mit einem Migrationshintergrund sind willkommen. Weitere Nachfragen und Bewerbungen mit den üblichen Unterlagen richten Sie bitte unter Angabe der Kennziffer A237/18 bis zum 07.12.2018 an (Bewerbung die nach dem Datum eingehen werde auch berücksichtigt): Universität Bremen Fachbereich Mathematik/Informatik Prof. Dr. Sebastian Maneth Bibliothekstraße 1 28359 Bremen oder in elektronischer Form (in einer pdf-Datei) an maneth(a)uni-bremen.de Bewerbungen werden auch nach der Frist berücksichtigt, bis die Stelle besetzt ist. Wir bitten Sie, uns von Ihren Bewerbungsunterlagen nur Kopien (keine Mappen) einzureichen, da wir sie nicht zurücksenden können. Bewerbungs- und Vorstellungskosten werden nicht erstattet. ---

1 0

World Logic Day: January 14 / Day of birth of Alfred Tarski and of death of Kurt Gödel
by jean-yves beziau 23 Nov '18

23 Nov '18

Creation of the World Logic Day: January 14 Day of birth of Alfred Tarski and of death of Kurt Gödel See details in "Logic Prizes et Cætera": https://link.springer.com/article/10.1007/s11787-018-0215-6 Jean-Yves Beziau Editor-in-Chief Logica Universalis

1 0

VerifyThis at ETAPS 2019: Announcement + Call for Problems
by VerifyThis 22 Nov '18

22 Nov '18

******************************************************************************* VerifyThis Verification Competition 2019 ACCOUNCEMENT AND CALL FOR PROBLEMS Competition to be held at ETAPS 2019 http://verifythis.ethz.ch ******************************************************************************** Get involved, even if you cannot participate in the competition: provide a challenge! IMPORTANT DATES Problems submission deadline: 28 January 2019 Competition: 6 and 7 April 2019 ABOUT THE COMPETITION VerifyThis 2019 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019) on 6 and 7 April 2019. It is the 8th event in the VerifyThis competition series. Information on previous events and participants can be found at http://verifythis.ethz.ch The aims of the competition are: - to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion - to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others. The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness and elegance. CALL FOR PROBLEMS To be able to offer a broad and diverse set of verification challenges, we are collecting submissions of ideas for verification challenges and problems. We welcome both problems of academic interest as well as challenges based on themes that are relevant in industry. We encourage suggestions at any level of detail, including submissions without a fully worked out verification task. - a problem may contain an informal statement of the algorithm to be implemented (optionally with complete or partial pseudocode) and the requirement(s) to be verified - a problem should be solvable, at least in part, within a 60-90 minute time slot - submission of reference solutions is welcome but not mandatory - problems mainly suitable for specific languages or tools should be clearly identified as such - problems that contain several subproblems or other means of difficulty scaling are especially welcome - the organizers reserve the right (but no obligation) to use the problems in the competition, either as submitted or with modifications - submissions from (potential) competition participants are allowed Problems from previous competitions can be seen at http://verifythis.ethz.ch Submissions are to be sent by email to verifythis(a)cs.nuim.ie by the date indicated above. PRIZES The submission most interesting and suitable for the competition will receive a prize. ORGANIZERS * Claire Dross, AdaCore, France * Carlo A. Furia, Universit�� della Svizzera Italiana (USI), Switzerland * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter M��ller, ETH Z��rich, Switzerland CONTACT Email: verifythis(a)cs.nuim.ie Web: http://verifythis.ethz.ch

1 0

26th WoLLIC 2019 (Utrecht, The Netherlands) - Call for Papers
by Ruy de Queiroz 21 Nov '18

21 Nov '18

[Please circulate. Apologies for multiple copies.] CALL FOR PAPERS WoLLIC 2019 26th Workshop on Logic, Language, Information and Computation July 2nd to 5th, 2019 Utrecht, The Netherlands ORGANISATION Utrecht University, Faculty of Humanities, The Netherlands (host university) Centro de Informática, Universidade Federal de Pernambuco, Brazil CALL FOR PAPERS WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-fifth WoLLIC will be held at Utrecht University, The Netherlands, from July 2nd to 5th, 2019. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) (TBC), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL). Just before and after the main WoLLIC 2019 event, Utrecht University will host two satellite workshops: -Proof Theory in Logic on 1-2 July 2019. This workshop on the role of structural proof theory in the study of logics will consist of invited talks by researchers in that area. -Compositionality in formal and distributional models of natural language semantics, on July 6 2019. The workshop programs will be announced end of December 2018 via the WoLLIC 2019 website (https://wollic2019.sites.uu.nl). Attendance of these satellite workshops is free, but registration is required. PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; proof mining, type theory, effective learnability; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection; foundations of mathematics; philosophy of mathematics; philosophical logic; philosophy of language. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. Articles should be written in the LaTeX format of LNCS by Springer (see authors instructions at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0). They must not exceed 12 pages, with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. (At least one author is required to pay the registration fee before granting that the paper will be published in the proceedings.) Papers must be submitted electronically at the WoLLIC 2019 EasyChair website. (Please go to http://wollic.org/wollic2019/instructions.html for instructions.) A title and single-paragraph abstract should be submitted by Feb 22, 2019, and the full paper by Feb 26, 2019 (firm date). Notifications are expected by April 5, 2019, and final papers for the proceedings will be due by April 15, 2019 (firm date). PROCEEDINGS The proceedings of WoLLIC 2019, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published (after a new round of reviewing) as a special post-conference WoLLIC 2019 issue of a scientific journal (to be confirmed). INVITED SPEAKERS (TBA) STUDENT GRANTS ASL sponsorship of WoLLIC 2019 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2019). See http://www.aslonline.org/studenttravelawards.html for details. IMPORTANT DATES Feb 22, 2019: Paper title and abstract deadline Feb 26, 2019: Full paper deadline April 5, 2019: Author notification Apr 15, 2019: Final version deadline (firm) PROGRAMME COMMITTEE Raffaella Bernardi (University of Trento) Nick Bezhanishvili (University of Amsterdam) Giuseppe Greco (Utrecht University) Philippe de Groote (INRIA Nancy) Rosalie Iemhoff (Utrecht University) (Co-CHAIR) Roberto Maieli (Department of Mathematics and Physics, University "Roma Tre”) Michael Moortgat (Utrecht University) (Co-CHAIR) Richard Moot (CNRS (LIRMM) & University of Montpellier) Larry Moss (Indiana University Bloomington) Sara Negri (University of Helsinki) Carlo Nicolai (King's College London) Valeria de Paiva (Nuance Comms and University of Birmingham) Alessandra Palmigiano (Delft University of Technology) Ruy de Queiroz (Centro de Informatica, Univ Federal de Pernambuco) Yde Venema (University of Amsterdam) Fan Yang (University of Helsinki) STEERING COMMITTEE Samson Abramsky, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Juliette Kennedy, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Lawrence Moss, Luke Ong, Hiroakira Ono, Valeria de Paiva, Ruy de Queiroz, Jouko Väänänen. (Former Member: Grigori Mints (deceased).) ORGANISING COMMITTEE Giuseppe Greco (Utrecht University, The Netherlands) (Local co-chair) Anjolina G. de Oliveira (Univ Federal de Pernambuco, Brasil) Ruy de Queiroz (Univ Federal de Pernambuco, Brasil) (co-chair) SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) European Association for Theoretical Computer Science (EATCS) European Association for Computer Science Logic (EACSL) ACM Special Interest Group on Logic and Computation (ACM-SIGLOG) (TBC) Sociedade Brasileira de Computação (SBC) Sociedade Brasileira de Lógica (SBL) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE http://wollic.org/wollic2019/

1 0

1st Logic Prizes Contest : Papers of all the Winners now on-line
by jean-yves beziau 19 Nov '18

19 Nov '18

The 1st Logic Prizes Contest was organized during UNILOG'2018 (6th World Congress and School in Universal Logic) in Vichy, France, June 16-26, 2018. There was the participation of winners of 9 different countries. All the contestants presented their work during a special session Sunday 24. And it was decided which was the best paper among the 9 by a jury formed by 7 world famous logicians. The winning paper as well as the other ones have been published in a special issue of Logica Universalis (Birkhäuser / Springer Nature) This issue is freely accessible to anybody: https://www.springer.com/birkhauser/mathematics/journal/11787?detailsPage=p… Jean-Yves Beziau Editor-in-Chief Logica Universalis

1 0