Klaus Havelund | 26 Oct 15:26 2014

[fm-announcements] NFM 2015 - final call for papers


The 7th NASA Formal Methods Symposium


27 – 29 April 2015
Pasadena, California, USA

Paper Submission: *** 10 Nov 2014 ***


The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.


Topics of interest include, but are not limited to:

Model checking
Theorem proving
SAT and SMT solving
Symbolic execution
Static analysis
Runtime verification
Program refinement
Compositional verification
Modeling and specification formalisms
Model-based development
Model-based testing
Requirement engineering
Formal approaches to fault tolerance
Security and intrusion detection
Applications of formal methods to aerospace systems
Applications of formal methods to cyber-physical systems
Applications of formal methods to human-machine interaction analysis


Dino Distefano
Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.

Viktor Kuncak
Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.

Rob Manning
Chief Engineer at NASA/JPL.


Paper Submission: 10 Nov 2014
Paper Notifications: 12 Jan 2015
Camera-ready Papers: 9 Feb 2015
Symposium:   27 – 29 April 2015


The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.


There are two categories of submissions:

- Regular papers describing fully developed work and complete results (15 pages)
- Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results  
 (6 pages)

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer’s Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.


Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Rajeev Joshi, NASA Jet Propulsion Laboratory


Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Yvonne Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK


Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
hol-info mailing list
hol-info <at> lists.sourceforge.net
Ruy de Queiroz | 26 Oct 13:50 2014

WoLLIC 2015 - Call for Papers

[Please circulate. Apologies for cross-postings.]

WoLLIC 2015
22nd Workshop on Logic, Language, Information and Computation 
July 20th-23rd, 2015
Bloomington, IN, USA

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) 
Sociedade Brasileira de Computação (SBC) 
Sociedade Brasileira de Lógica (SBL)

School of Informatics and Computing, Indiana University, USA
Program in Pure and Applied Logic, Indiana University, USA
Centro de Informática, Universidade Federal de Pernambuco, Brazil 

School of Informatics and Computing, Indiana University, USA 

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-second WoLLIC will be held at the School of Informatics and Computing, Indiana University, from July 20th to 23rd, 2015. 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), the Sociedade Brasileira de Computação (SBC), and the Sociedade Brasileira de Lógica (SBL).

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. 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. They must not exceed 10 pages (in font 10 or higher), 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. Papers must be submitted electronically at the WoLLIC 2015 EasyChair website. (Please go to http://wollic.org/wollic2015/instructions.html for instructions.) A title and single-paragraph abstract should be submitted by Feb 8, 2015, and the full paper by Feb 15, 2015 (firm date). Notifications are expected by Mar 22, 2015, and final papers for the proceedings will be due by Apr 5, 2015 (firm date).

The proceedings of WoLLIC 2015, 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 as a special post-conference WoLLIC 2015 issue of a scientific journal (to be confirmed).


ASL sponsorship of WoLLIC 2015 will permit ASL student members to apply for a modest travel grant (deadline: May 1st, 2015). See http://www.aslonline.org/studenttravelawards.html for details.

Feb 8, 2015: Paper title and abstract deadline 
Feb 15, 2015: Full paper deadline 
Mar 22, 2015: Author notification
Apr 5, 2015: Final version deadline (firm)

Juliana Küster Filipe Bowles (U St Andrews, Scotland)
Guillaume Brunerie (ENS Ulm, France) (TBC)
Ann Copestake (U Cambridge, UK) (TBC)
Robin Cooper (U Gothenburg, Sweden)
Nikos Galatos (U Denver, USA)
Achim Jung (U Birmingham, UK)
Sara  Kalvala (U Warwick, UK)
Elham Kashefi (Edinburgh U, Scotland)
Peter Lefanu Lumsdaine (Institute for Advanced Study, USA)
Ian Mackie (U Sussex, UK)
Gerard de Melo (Tsinghua University, China)
Vivek Nigam (Federal U of Paraíba, Brazil)
Valeria de Paiva (Nuance Comm, USA) (CHAIR) 
Luiz Carlos 
Pereira  (PUC-Rio, Brazil)
Elaine Pimentel (Federal U of Rio Grande do Norte, Brazil)
Alexandra Silva (Radboud Nijmegen U, The Netherlands)
Carolyn Talcott (SRI International, USA)
Josef Urban (Radboud Nijmegen U, The Netherlands)
Laure Vieu (IRIT-Toulouse, France) (TBC)
Renata Wasserman (U São Paulo, Brazil)
Anna Zamansky (U Haifa, Israel)

Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Angus Macintyre, Luke Ong, Hiroakira Ono, Ruy de Queiroz.

Daniel Leivant (Indiana U) (Local co-chair)
Larry Moss (Indiana U) (Local co-chair)
Anjolina G. de Oliveira (U Fed Pernambuco) 
Ruy de Queiroz (U Fed Pernambuco) (co-chair)

Contact one of the Co-Chairs of the Organising Committee.


hol-info mailing list
hol-info <at> lists.sourceforge.net
Cvetan Dunchev | 24 Oct 18:16 2014

CROSS_applied thm.

Dear colleagues and friends,

I would like to inform you about the following problem: I want to use  
the CROSS_applied theorem from the pred_setTheory:


Despite the fact that the theory is loaded, I got the following  
message in the console:
! Toplevel input:
! CROSS_applied;
! ^^^^^^^^^^^^^
! Unbound value identifier: CROSS_applied

and when I have a look at the corresponding source file, indeed such a  
theorem does not exist. Does anybody have an explanation about that?

Best regards,
Cvetan Dunchev

Piotr Trojanek | 23 Oct 13:00 2014

HOL Light-style parsing in HOL4

Dear all,

is it possible to use HOL4 parser in a similar way to `parse_preterm`
from HOL Light?

In HOL Light one can easily build a parser for HOL terms embedded in a
custom language (see hol_light/Examples/prog.ml). In HOL4 it seems
only possible to modify the term grammar (e.g. with add_rule), which
is much less flexible.


Piotr Trojanek

Ramana Kumar | 23 Oct 19:58 2014

omitting a constant from pretty-printing

Hi all,

I would like to add a pretty-printing rule to completely omit a constructor and only print its argument. (I understand this means the resulting output won't parse back to the same input without type inference help.) Is it possible to do this in any way short of making a userprinter?

To be concrete, I have the following:

Datatype`mlstring = strlit (char list)`

and I would like the printer to print


rather than

strlit "hello"

in my HOL-munged LaTeX output. (Userprinters are very difficult to use with the munger, so I would like to avoid them if possible.)

hol-info mailing list
hol-info <at> lists.sourceforge.net
S B Cooper | 22 Oct 22:42 2014

CiE 2015: Evolving Computability, Bucharest, June 29 - July 3, 2015

      COMPUTABILITY IN EUROPE 2015: Evolving Computability
                   Bucharest, Romania
                    June 29 - July 3


Submission Deadline for LNCS:                 11 January 2015
Notification of authors:                         9 March 2015
Deadline for final revisions:                    6 April 2015

CiE 2015 is the 11th conference organized by CiE (Computability
in Europe), a European association of mathematicians, logicians,
computer scientists, philosophers, physicists and others
interested in new developments in computability and their
underlying significance for the real world. Previous meetings
have taken place in Amsterdam (2005), Swansea (2006), Siena
(2007), Athens (2008), Heidelberg (2009), Ponta Delgada (2010),
Sofia (2011), Cambridge (2012), Milan (2013) and Budapest (2014).

Evolution of the universe, and us within it, invite a parallel
evolution in understanding. The CiE agenda - fundamental and
engaged - targets the extracting and developing of computational
models basic to current challenges.  From the origins of life, to
the understanding of human mentality, to the characterising of
quantum randomness - computability theoretic questions arise in
many guises.  The CiE community, this coming year meeting for the
first time in Bucharest, carries forward the search for
coherence, depth and new thinking across this rich and vital
field of research.

In all cases we are looking for fundamental and theoretical
submissions. In line with other conferences in this series, CiE
2015 has a broad scope and provides a forum for the discussion of
theoretical and practical issues in Computability with an
emphasis on new paradigms of computation and the development of
their mathematical theory.

We particularly invite papers that build bridges between
different parts of the research community.

For topics covered by the conference, please visit


  * John Reif (Duke Unversity)
  * Steve Simpson (Pennsylvania State University)


  * Ann Copestake (University of Cambridge)
  * Mircea Dumitru (University of Bucharest, Public Lecture)
  * Pawel Gawrychowski (Max-Planck-Institut fuer Informatik)
  * Julia Knight (University of Notre Dame)
  * Anca Muscholl (Universite Bordeaux)
  * Gheorghe Paun (Romanian Academy)
  * Alexander Razborov (University of Chicago
       and Steklov Mathematical Institute)
  * Vlatko Vedral (University of Oxford)


  * Representing streams
     (Organizers: Joerg Endrullis and Dimtri Hendriks)
  * Automata, logic and infinite games
     (Organizers: Dietmar Berwanger and Ioana Leustean)
  * Reverse mathematics
     (Organizers: Damir Dzhafarov and Alberto Marcone)
  * Classical computability theory
     (Organizers: Marat Arslanov and Steffen Lempp)
  * Bio-inspired computation
     (Organizers: Andrei Paun and Petr Sosik)
  * History and philosophy of computing
     (Organizers: Christine Proust and Marco Benini)


  * Marat Arslanov (Kazan)           * Jeremy Avigad (Pittsburgh)
  * Veronica Becher (Buenos Aires)   * Arnold Beckmann (Swansea)
  * Laurent Bienvenu (Paris)         * Alessandra Carbone (Paris)
  * Gabriel Ciobanu (Iasi)           * S Barry Cooper (Leeds)
  * Laura Crosilla (Leeds)           * Liesbeth De Mol (Ghent)
  * Walter Dean (Warwick)            * Volker Diekert (Stuttgart)
  * Damir Dzhafarov (Storrs, Connecticut)
  * Peter van Emde Boas (Amsterdam)  * Rachel Epstein (Harvard)
  * Johanna Franklin (Hempstead, NY) * Neil Ghani (Glasgow)
  * Joel David Hamkins (New York)    * Rosalie Iemhoff (Utrecht)
  * Emmanuel Jeandel (LORIA)         * Natasha Jonoska (Tampa, FL)
  * Antonina Kolokolova (St.John's, NL)
  * Antonin Kucera (Prague)          * Oliver Kutz (Magdeburg)
  * Benedikt Loewe (Hamburg & Amsterdam)
  * Jack Lutz (Ames, IA)             * Florin Manea (Kiel)
  * Alberto Marcone (Udine)          * Radu Mardare (Aalborg)
  * Joe Miller (Madison, WI)
  * Russell Miller (Flushing, NY)    * Mia Minnes (La Jolla, CA)
  * Victor Mitrana (Bucharest, co-chair)
  * Ian Pratt-Hartmann (Manchester)  * Dag Normann (Oslo)
  * Mehrnoosh Sadrzadeh (London)     * Anne Smith (St Andrews)
  * Mariya Soskova (Sofia, co-chair) * Susan Stepney (York)
  * Paul Spirakis (Patras & Liverpool)
  * Jacobo Toran (Ulm)               * Marius Zimand (Towson, MD)

The PROGRAMME COMMITTEE cordially invites all researchers
(European and non-European) in computability related areas to
submit their papers (in PDF format, max 10 pages using the LNCS
style) for presentation at CiE 2015.

The submission site
is open.

For submission instructions consult

The CONFERENCE PROCEEDINGS will be published by LNCS, Springer


CiE 2015 http://fmi.unibuc.ro/CiE2015/

ASSOCIATION COMPUTABILITY IN EUROPE http://www.computability.org.uk
CiE Conference Series http://www.illc.uva.nl/CiE
CiE Membership Application Form http://www.lix.polytechnique.fr/CIE
Computability (Journal of CiE) http://www.computability.de/journal/
CiE on FaceBook https://www.facebook.com/AssnCiE
Association CiE on Twitter https://twitter.com/AssociationCiE

Michael Winter | 20 Oct 21:19 2014

CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

                           CALL FOR PAPERS

                  15th International Conference on
    Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

            28 September to 1 October 2015, Braga, Portugal
                  URL:  http://ramics2015.di.uminho.pt
         PDF: http://ramics2015.di.uminho.pt/RAMiCS15-CFP.pdf


 We invite submissions in the general area of Relational and Algebraic 
 Methods  in Computer Science. Special focus will lie on formal methods 
 for software engineering, logics of programs and links with neighbouring 

 Particular topics of interest for the conference cover,
 but are not limited to:

 * Algebraic approaches to
   - specification, development, verification, and analysis of programs
     and algorithms
   - computational logic, in particular logics of programs, modal and
     dynamic logics, interval and temporal logics
   - semantics of programming languages

 * Applications in fields such as
   - relational formal methods such as B or Z, tabular methods
   - information systems
   - graph theory and combinatorial optimisation
   - games, automata and language theory
   - spatio-temporal reasoning, knowledge acquisition
   - preference and scaling methods, computational social choice,
     social software

 * Theoretical foundations and supporting tools, including
   - mechanised and automated reasoning, decision procedures
   - process algebras, fixed point calculi, idempotent semirings,
     quantales, allegories
   - dynamic algebras, cylindric algebras and their applications in 


 Since 1994, the RelMiCS meetings on Relational Methods in Computer 
 Science have been a main forum for researchers who use the calculus of 
 relations and similar algebraic formalisms as methodological and 
 conceptual tools. The AKA workshop series on Applications of Kleene 
 algebra started with a Dagstuhl seminar in 2001 and was co-organised 
 with the RelMiCS conference until 2009. Since 2011, joint RAMiCS 
 conferences continue to encompass the scope of both RelMiCS and AKA.

 The predecessors of this conference were held in Dagstuhl (January 
 1994), Parati (September 1995), Hammamet (January 1997), Warsaw 
 (September 1998), Quebec (January 2000), Dagstuhl (February 2001), 
 Oisterwijk (October 2001), Malente (April 2003), St. Catharines 
 (January 2005), Manchester (September 2006), Frauenwoerth (April 2008), 
 Doha (November 2009), Rotterdam (June 2011), Cambridge UK (September 
 2012) and Marienstatt im Westerwald (April 2014).

 Student Program

 The conference will be accompanied by a PhD training program. Details 
 will be published in due time in a special call and on the conference 

 Proceedings and Submission

 All papers will be formally reviewed. We plan to publish the
 proceedings in the series Lecture Notes in Computer Science ready at
 the conference. Submissions must be in English, in Postscript or PDF
 format, and provide sufficient information to judge their merits.
 They must be unpublished and not submitted for publication elsewhere. 
 They should not exceed 16 pages in Springer LNCS style (accepted
 papers must be produced with LaTeX). Additional material may be
 provided by a clearly marked appendix or a reference to a manuscript
 on a website. This may be considered at the discretion of the PC.
 Deviation from these requirements may cause immediate rejection.
 One author of each accepted paper is expected to present the paper
 at the conference.

 Submission is via EasyChair at the following address:
 Formatting instructions and the LNCS styled files can be obtained via:

 As for the earlier conferences of this series, it is also intended to
 publish a selection of the best papers in revised and extended form in
 a special issue of the Journal of Logic and Algebraic Methods in
 Programming (JLAMP).

 Important Dates

     Title and abstract submission:                 March 18 2015
     Submission of full papers:                     March 26 2015
     Notification:                                  June  05 2015
     Final versions due (firm deadline):            July  10 2015

     Conference:                   September 28 - October 01 2015

 Programme Committee

     Rudolf Berghammer     (Kiel, Germany)
     Jules Desharnais      (Laval U., Canada)
     Marcelo Frias         (Buenos Aires, Argentina)
     Stephen Givant        (Mills College, USA)
     Hitoshi Furusawa      (Kagoshima, Japan)
     Timothy G. Griffin    (Cambridge, UK)
     Walter Guttmann       (Canterbury, New Zealand)
     Robin Hirsch          (London, UK)
     Peter Hoefner         (NICTA, Australia; Publicity chair)
     Ali Jaoua             (Doha, Qatar)
     Peter Jipsen          (Chapman U., USA)
     Wolfram Kahl          (McMaster U., Canada)
     Rodger Maddux         (Iowa State U., USA)
     Ali Mili              (NJIT, U. Heights, USA)
     Bernhard Moeller      (U. Augsburg, Germany)
     Martin E. Mueller     (U. Augsburg, Germany)
     Jose N. Oliveira      (U. Minho, Portugal; General chair)
     Ewa Orlowska          (Warsaw, Poland)
     Agnieszka Rusinowska  (Univ. Paris 1, France)
     Gunther Schmidt       (Munich, Germany)
     Renate Schmidt        (Manchester, UK)
     Isar Stubbe           (U. Littoral-Cote-d'Opale, France)
     Michael Winter        (Brock U., Canada; PC chair)


 Steering Committee

     Rudolf Berghammer  (Kiel, Germany)
     Jules Desharnais   (Laval U., Canada)
     Ali Jaoua          (Doha, Qatar)
     Peter Jipsen       (Chapman U., USA)
     Bernhard Moeller   (U. Augsburg, Germany)
     Jose N. Oliveira   (U. Minho, Portugal)
     Ewa Orlowska       (Warsaw, Poland)
     Gunther Schmidt    (Munich, Germany)
     Michael Winter     (Brock U., Canada)


 Organising Committee

     Jose N. Oliveira    (U. Minho, Portugal; General chair)
     Michael Winter      (Brock U., Canada; PC chair)
     Luis S. Barbosa     (U. Minho, Portugal)
     Manuel A. Cunha     (U. Minho, Portugal)
     Antonio N. Ribeiro  (U. Minho, Portugal)

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Ramana Kumar | 16 Oct 18:18 2014

Theorems Produced by Type Definitions

Hi all,

There has been an interesting discussion on the OpenTheory mailing list recently regarding how to simplify the two theorems produced by a type definition in HOL Light and remove their free variables. The latest message in the thread, which shows the  suggestions by Mario Carneiro can be found here: http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.

I'm cross-posting to this list because I think using Mario's suggestions would be an improvement to both HOL Light and Opentheory. I hope the respective authors of those systems might agree and implement the changes, and that anyone else with an interest might voice their opinion.

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Geoff Sutcliffe | 15 Oct 14:34 2014

CADE-25 Call for Papers, etc.



25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015


Submission deadlines:

   14 November 2014 (workshops/tutorials/competitions)
16/23 February 2015 (papers)

CADE is the major international forum at which research on all aspects of
automated deduction is presented. The 25th jubilee edition will feature
a special session on the past, present, and future of automated deduction

  Ursula Martin      University of Oxford
  Frank Pfenning     Carnegie Mellon University
  David Plaisted     University of North Carolina at Chapel Hill
  Andrei Voronkov    University of Manchester

as invited speakers. In addition, there will be invited presentations by

  Ulrich Furbach     University of Koblenz
  Edward Zalta       Stanford University


Workshop proposals for CADE-25 are solicited. Both well-established
workshops and newer ones are encouraged. Similarly, proposals for workshops
with a tight focus on a core automated reasoning specialization, as well as
those with a broader, more applied focus, are very welcome.

Please provide the following information in your application document:

+ Workshop title.
+ Names and affiliations of organizers.
+ Proposed workshop duration (from half a day to two days) and preferred
+ Brief description of the goals and the scope of the workshop. Why is the
  workshop relevant for CADE?
+ Is the workshop new or has it met previously? In the latter case
  information on previous meetings should be given (e.g., links to the
  program, number of submissions, number of participants).
+ What are the plans for publication?


Tutorial proposals for CADE-25 are solicited. Tutorials are expected to be
half-day events, with a theoretical or applied focus, on a topic of interest
for CADE-25. Proposals should provide the following information:

+ Tutorial title.
+ Names and affiliations of organizers.
+ Brief description of the tutorial's goals and topics to be covered.
+ Whether or not a version of the tutorial has been given previously.

CADE will take care of printing and distributing notes for tutorials that
would like this service.


The CADE ATP System Competition (CASC), which evaluates automated theorem
proving systems for classical logics, has become an integral part of the
CADE conferences.

Further system competition proposals are solicited. The goal is to foster
the development of automated reasoning systems in all areas relevant for
automated deduction in a broader sense. Proposals should include the
following information:

+ Competition title.
+ Names and affiliations of organizers.
+ Duration and schedule of the competition.
+ Room/space requirements.
+ Description of the competition task and the evaluation procedure.
+ Is the competition new or has it been organized before?
  In the latter case information on previous competitions should be given.
+ What computing resources are required and how will they be provided?


High-quality submissions on the general topic of automated deduction,
including foundations, applications, implementations, and practical
experiences are solicited.

* Logics of interest include propositional, first-order, equational,
  higher-order, classical, description, modal, temporal, many-valued,
  constructive, other non-classical, 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

* Methods of interest include resolution, superposition, completion,
  saturation, term rewriting, decision procedures, model elimination,
  connection methods, tableaux, sequent calculi, natural deduction, as
  well as their supporting algorithms and data structures, including
  matching, unification, orderings, induction, indexing techniques, proof
  presentation and explanation, proof planning.

* Applications of interest include program analysis, verification and
  synthesis of software and hardware, formal methods, computational logic,
  computer mathematics, natural language processing, computational
  linguistics, knowledge representation, ontology reasoning, deductive
  databases, declarative programming, robotics, planning, and other areas
  of AI.

Submissions can be made in the categories regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages for regular
papers and 10 pages for system descriptions. Submissions must be unpublished
and not submitted for publication elsewhere. They will be judged on
relevance, originality, significance, correctness, and readability. System
descriptions should contain a link 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 


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).


Workshop/Tutorials/System Competitions:

Submission deadline:      14 November 2014
Notification:             28 November 2014


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


Proposals for workshops, tutorials, and system competitions should be
uploaded via


Papers should be submitted via



Conference Chair:
  Christoph Benzmüller   Freie Universität Berlin

Program Committee Co-Chairs:
  Amy Felty              University of Ottawa
  Aart Middeldorp        University of Innsbruck

Workshop, Tutorial, and Competition Co-Chairs:
  Jasmin Blanchette      Technische Universität München
  Andrew Reynolds        EPFL 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 Mayer    Universita 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 Hustadt        University 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 Middeldorp        University of Innsbruck
  Albert Oliveras        Technical University of Catalonia
  Nicolas Peltier        CNRS
  Brigitte Pientka       McGill University
  Ruzica Piskac          Yale University
  André Platzer          Carnegie Mellon University
  Andrew Reynolds        EPFL Lausanne
  Christophe Ringeissen  LORIA-INRIA
  Renate Schmidt         University of Manchester
  Stephan Schulz         DHBW Stuttgart
  Georg Struth           University of Sheffield
  Geoff Sutcliffe        University of Miami
  Alwen Tiu              Nanyang Technological University
  Freek Wiedijk          Radboud University Nijmegen

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
hol-info mailing list
hol-info <at> lists.sourceforge.net
Geoff Sutcliffe | 13 Oct 18:44 2014

NETYS 2015 Call for Papers


**NETYS 2015**
**May 13-15, 2015, AGADIR, MOROCCO**

*Aim and Scope:**
NETYS aims to bring together researchers and engineers from both the 
theory and practice of distributed and networked systems. The scope of 
the conference covers all aspects related to the design and the 
development of these systems, including, but not restricted to, 
multi-core architectures, concurrent and distributed algorithms, 
parallel/concurrent/distributed programming, distributed databases, 
cloud systems, networks, security, formal verification, etc.

NETYS will provide a forum to report on best practices and novel 
algorithms, results and techniques on networked systems. Original 
contributions as well as experience papers on the principles, design, 
implementation, modeling, analysis, verification, and application of 
networked systems are solicited. Specific concepts common to different 
forms of such systems are most welcome.

NETYS is coupled with the METIS Spring School which aims at introducing 
young researchers to the domain of distributed and networked systems 
through tutorials on basics, as well as lectures on new research topics 
and current trends in this domain.

*Paper submission:**
Submissions should contain original research and sufficient detail to 
assess the merits and relevance of the contribution. NETYS welcomes 
papers on theory, case studies and comparisons with existing 
experimental research, tools, as well as combinations of new theory with 
experimental evaluation.

NETYS is soliciting two forms of papers: full and short papers. Full 
papers are allowed a maximum of 15 pages in Springer's LNCS format, 
whereas short papers are allowed a maximum of 5 pages (in the same 
format), both in the submission and in the proceedings. A full paper 
submission might be accepted as such, as a short paper or a poster. A 
short paper may be accepted as such or as a poster.

Posters will be presented at the conference to reflect work in progress 
and will not lead to a publication in the proceedings. Authors are given 
the option to accept or not the type in which their paper is selected 
for acceptance.


Springer's Lecture Notes in Computer Science series will publish the 
proceedings of the conference (www.springer.com/lncs). It is required 
that each accepted paper be presented at the conference by one of its 

The Computing Journal could publish extended versions of selected papers 

Awards will be given to the best paper and the best student paper. A 
paper is eligible for the best student paper award if at least one of 
its authors is a full-time student at the time of submission. This 
should be indicated in the submission.

*Submission instructions:*

All submissions should follow the LNCS template. Submitted papers must 
be written in English. Full papers are allowed a maximum of 15 pages in 
LNCS format, whereas short papers are allowed a maximum of 5 pages, both 
in the submission and in the proceedings. Papers exceeding these limits 
may be rejected without review.

Paper submission will be handled by EasyChair, so please make sure that 
you have an active account. The papers must be submitted electronically at:

*Important dates**
- Abstract submission deadline: January 5, 2015
- Paper submission deadline: January 9, 2015
- Acceptance notification: March 9, 2015
- Camera ready copy due: April 10, 2015
- Conference: May 13-15, 2015


/_General Co-chairs_:/
Mohammed Erradi        ENSIAS, Rabat, Morocco
Rachid Guerraoui       EPFL, Switzerland

/_Program Co-chairs_:/
Ahmed Bouajjani        Univ. Paris Diderot, France
Hugues Fauconnier      Univ. Paris Diderot, France

/_Program Committee_:/
Parosh Aziz Abdulla    Univ. Uppsala, Sweden
Joffroy Beauquier      Univ. Paris 11, France
Gregor Bochmann        Univ. Ottawa, Canada
Carole Delporte        Univ. Paris Diderot, France
Amr El Abbadi          UCSB, USA
Khaldoun El Agha       Univ. Paris 11, France
Mohamed El Koutbi      ENSIAS, Rabat, Morocco
Boualem Benatallah     Univ. New South Wales, Australia
Mohamed El Kamili      USMBA, Fes, Morocco
Bernd Freisleben       Univ. Marburg, Germany
Mohamed Gouda          Univ. Texas at Austin
Vincent Gramoli        Univ. Sydney, Australia
Seif Haridi            SICS, Sweden
Maurice Herlihy        Brown Univ., USA
Claude Jard            Univ. Nantes, France
Zahi Jarir             Univ. Cadi Ayyad, Morocco
Anne-Marie Kermarrec   INRIA, Rennes, France
Rupak Majumdar         MPI-SWS, Germany
Stephan Merz           INRIA, Nancy, France
Louise Moser           UCSB, USA
Hassan Mountassir      Univ. Franche-Comt?, France
Guevara Noubir         Northeastern Univ., USA
Andreas Podelski       Univ. Freiburg, Germany
Shaz Qadeer            Microsoft Research, USA
Vivien Quema           INPG, Grenoble, France
Sergio Rajsbaum        UNAM, Mexico
Ganesan Ramalingam     Microsoft Research, India
Michel Raynal          IRISA, Rennes, France
Alexander Shvartsman   Univ. Connecticut, USA
Sebastian Tixeuil      Univ. Pierre et Marie Curie, France
Martin Vechev          ETH Zurich, Switzerland

_/Organizing Committee/_:
Khadija Bakkouch       IRFC, Rabat
Abdellah Boulouz       Univ. Ibn zohr, Agadir
Mohammed Erradi        ENSIAS, UM5S, Rabat
Zahi Jarir             Univ. Cadi Ayyad, Marrakech
Mohammed Ouzzif        ESTC, UH2M, Casablanca

_/Students Committee/_:
Meryeme Ayache        ENSIAS, UM5S, Rabat
Yahya Benkaouz        ENSIAS, UM5S, Rabat

Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
Sophie Tison | 13 Oct 08:17 2014

RTA 2015 - First Call For Papers

              RTA 2015 - CALL FOR PAPERS 
           26th International Conference on
        29 June - 1 July, 2015, Warsaw, Poland 
      co-located with TLCA, as part of RDP 2015

RTA is the major forum for the presentation of research on all 
aspects of rewriting.  Topics of interest include:

* Foundations: string, term, net and graph rewriting; higher-order
rewriting; binding techniques; constrained rewriting and deduction;
categorical and infinitary rewriting; stochastic rewriting;
higher-dimensional rewriting; tree automata; confluence; 
termination; complexity; modularity; equational logic; 
universal algebra; rewriting logic; rewriting calculi.

* Algorithmic aspects and implementation: strategies; matching;
unification; anti-unification; narrowing; completion; parallel
execution; certification of rewriting properties; abstract machines;
automated (non)termination and confluence provers; automated
complexity analysis; system descriptions.

* Applications of rewriting: programming languages (functional, 
logic, object-oriented and other programming paradigms); type 
systems; program analysis, transformation and optimisation; 
rewriting models of programs; semantics; process calculi; 
functional calculi; explicit substitution; constraint solving; 
symbolic and algebraic computation; theorem proving; 
proof checking; system modelling; system synthesis and 
verification; XML queries and transformations; cryptographic 
protocols; security policies; systems biology; linguistics; 
rewriting in education.

Important Dates:
# Submission: title and abstract: 30 January 2015
              full paper: 6 February 2015
# Rebuttal period: 19-21 March 2015  
# Notification:    8 April 2015
# Final version:  25 April 2015

Submission and publication:
The RTA 2015 proceedings will be published by LIPIcs (Leibniz
International Proceedings in Informatics). Papers should present
original work, and should be submitted via Easychair:
Papers should be at most 15 pages (10 for system descriptions) 
in the style described in:
This year we particularly welcome submissions on applications of
rewriting. Application papers are regular papers (15 pages); their
originality is judged based on the novelty of the application or the
depth of the rewriting methods applied. 
System description papers present new software tools in which 
rewriting plays an important role, or significantly new versions 
of such tools. The paper should also include an evaluation of the 

Programme Committee:
M. Ayala-Rincon, U. Brasilia
H. Cirstea, Loria Nancy
S. Delaune, ENS Cachan
A. Di Pierro, U. Verona
G. Dowek, Inria
M. Fernandez, KCL, chair
J. Giesl, RWTH Aachen U.
M. Hanus, CAU Kiel
D. Kesner, U. Paris-Diderot
T. Kutsia, Johannes Kepler U. Linz
J. Levy, IIIA-CSIC Barcelona
S. Lucas, Polytechnic U. Valencia
C. Lynch, Clarkson U.
I. Mackie, E. Polytechnique
G. Moser, U. Innsbruck
D. Plump, U. York
F. van Raamsdonk, VU Amsterdam
K. Rose, Two Sigma, US
M. Sakai, Nagoya U.
A. Scedrov, U. Pennsylvania
M. Schmidt-Schauss, U. Frankfurt
C. Schuermann, ITU Copenhagen	
P. Selinger, Dalhousie U.
P. Severi, U. Leicester
K. Ueda, Waseda U.

Conference Chair:
Aleksy Schubert
Warsaw University

For more information, please contact the PC chair:
Maribel.Fernandez <at> kcl.ac.uk

Pr. Sophie Tison (RTA publicity chair)
LIFL - University of Lille- CNRS
sophie.tison <at> lifl.fr

Attachment (smime.p7s): application/pkcs7-signature, 3818 bytes
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
hol-info mailing list
hol-info <at> lists.sourceforge.net