Re: [isabelle] journals on theorem proving



The Journal Of Automated Reasoning that Larry mentions addresses verification, in particular of software (see the latest JAR issue) and security (a special issue on security is in preparation).

Tobias

li yongjian wrote:
Hi,
   Could you please also introduce some journals that relates the
fielf of applying theorem proving technique to verfication of
hardware, security, software?

regards!
yjl


---------- Forwarded message ----------
From: Lawrence Paulson <lp15 at cam.ac.uk>
Date: Fri, May 23, 2008 at 5:09 PM
Subject: Re: [isabelle] journals on theorem proving
To: li yongjian <lyj238 at gmail.com>
Cc: cl-isabelle-users at lists.cam.ac.uk


The primary journal in the field of theorem proving is the Journal Of
Automated Reasoning. There is also the ACM Transactions On
Computational Logic. The Journal of Computer Security is not primarily
concerned with theorem proving.
Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623    Fax: +44(0)1223 334678





On 23 May 2008, at 03:46, li yongjian wrote:

Dear all:
 Recently, our library request us to provide some information on the
field of journals on theorem proving .

 Could you please provide some international journal
on theorem proving or security.

From Larry's work on trace theory on security protocol, I know
Journal of computer security.

But could you please provide more, which either publish papers on
theorem proving or security, or theorem proving techniques or relating
the two things?


Thanks in advance.
regards!




Yongjian Li
2008-05-23


------------------------------------------------------------------------

BEGIN:VCARD
VERSION:3.0
N:Paulson;Lawrence;;;
FN:Lawrence Paulson
ORG:University of Cambridge;Computer Laboratory
TITLE:Professor of Computational Logic
EMAIL;type=INTERNET;type=WORK:lp15 at cam.ac.uk
EMAIL;type=INTERNET;type=WORK;type=pref:Larry.Paulson at cl.cam.ac.uk
TEL;type=WORK;type=pref:01223 334623
TEL;type=CELL:07774 017623
TEL;type=CELL:50623
TEL;type=WORK;type=FAX:01223 334678
item1.ADR;type=WORK;type=pref:;;William Gates Building;15 JJ Thomson Avenue;CAMBS;CB3 0FD;United Kingdom
item1.X-ABADR:uk
item2.URL;type=pref:http\://www.cl.cam.ac.uk/users/lcp/
item2.X-ABLabel:_$!<HomePage>!$_
X-AIM;type=WORK;type=pref:LawrenceCPaulson
PHOTO;BASE64:
  TU0AKgAAGAaAOdjJx/wKCO+BwVepR/tZaoR/t5jKV/vdnK2KxN/r1Smt/oxGEp/rVOFJ/xctP9Sp
  SRMZax5zs6IM5jHOGr2bOeXw1SyZvTiIzWKtaIPeiRWZTcxv9OJyRM5ex6JHuT1F/q2eyqstagTF
  GP93s6vxKxsaIN6k2iGOdrV+vQWxRta0slGMYv8AXkAWGCTGGRav2HAsa1wlzr2CReqK1OUtaqXH
  JSUqWSv89nscyPIXKPLVW5PKyuRGsximNqWUwKpUCw1SG1TDzbGSZOJSTVzYWabzle7mbWiqMbev
  /hVSoVTcRFnQypxGgT/kUKsSm9AC0RCBRCw9q4wK1s6+s6KS6IVilsZW7LJP9CIQhP+63cxnPMnP
  MZb7oyWZb3UxOJShDfqAx7QJSiaTJ0pZSqyThGNu1hrL/CKCt0n6bMepZWlapY9kY95ap24qGt0h
  ybImpauJyZzjKE6rmms3SYuw3SwoZGqwGsxJjK+l0Ls2pqUva975sy+KPtslT/vY/pCQ8m6YRWuU
  gjmkQ9jWzJCD2kwlCklIYhykQchy0xKEIjyaJm4aoJs47iFrNjdRBBSss8lMMNOpZnJ2hzVuiqjq
  xgiFAxHGbBu4ty4rQr6aONN7NKWSkkCULTTPakz0TYoDhI9Bc8lrAyskoRibMuiAYiEkUvpEBAUs
  zL6UhDMS8AQDB/1azIMBCEMkqlHaqqpRURqoXsNyW98OpEldL2LNbdpPFq9TQm8eFq4Jexms5jWB
  RMaW5GaqQIf4xyu9g5vfHtCOUs8ok4QibCFVB/hjU5/hDVp/ggFL3gxegABCu9/LuCF6ARWJ/1o0
  1YszfK7zEu72pS5K2K/Qb0QMoDk2a6ars+qqPUBCq4xg2Cku25Vh0cXtHRkuCqIQ4NiyEf9RJNNq
  JUEwlbXvU9Uhy94IX+f4MX1WwcpMDFZXzn+iYQvGgLwAAIYPoIAVpg+C3ro2ZyRlUzuGl0UW1dVh
  H+NY9ruSjKl6qzquEm1B5Zkx3qOqCPa6kdiuvseRpPYuLKvtRW7sVqIDHcdZ6lpt9JNguAaxoC71
  ikWlamu9acdXa86lqPMgBWum85oUwXEMaRNrPOv0dNtMK02klQW6i9UjS6duzk7iKsl0z5DdecIh
  tyGp3Cygtgtt5Vln1U3gvFc4Poep4TemBszxt8elL/K6dXemgRp/NVnz/n89hN41akTH9+1HiIKn
  bKJNJr30m0zqj2/r0KXvW+bXwbz+FsRwCrvqfcRtYrcijg5BirtL5mUxHve+1VWrVXtvPcg85+bz
  XQr8eovwvDVGnvcao+KD7QWkEiaiaaEo/whM+LAVYk5HhrCtJMSs95omoF5Y2no36JDhlcNWTZYh
  HmwQEKWllLAhDMkOKWQUr5YCCL2csBBz7VopRRe3B+KjzVcl3aGZkFK/XvPNXyZlf0G35r5YPGiE
  7zmAQYjDBc0yYldkFNcNYmxrx/kNJsdVSJIogk3OwtV4Lb2MQ9OGzc4hHTiLFNVHkc5XxSiMJSAh
  rEW2hPNBSBhWoSgUq7Qce8VoeyUicDXKMLSVQlHvClAheSupWmmBjF8f6Y2BNBdBCJzL3o0Ogc89
  p6x7yYmuG8UUc5ECIp/L0Y+ITgiFFnkERdTKKiijeiaN4v81ChzCKoRaPbUXwNCXsP8LSYz2BaQ+
  lY4io50myD2eedSOyZplI2IwqkpCUhzCkaMKRJl5uOc+0GCsFXxqzc7BFp7QGEydLAM6JY3o6zdL
  ycmRDfFmt3GMUJuZRRrGukfHmh1HphR3mG1Bzc3p8LHCkueehJ0G0sJmJw41LTwMUpajksckTiUw
  I2JRYaZj2OlVslxg694KvVAAvd7ppnQS6qUwYiNIptQ3AAzYtLYm6vrmCXAmxRqOTGHPSGhZSywk
  2Ag1YEMUiRntp3S9RdPKXUsYoSsnhzDakNprTKvFPVSBan4EIlKkyPVGgov2Ci93PRtYA0EtFUI8
  x2qkyqHa2TYFWq5SCyw96Plgmqy4Z0MBjIGFqSaU5phWkgpyQwiZDBe0rpsSdUVcLYI5IYeC2dOB
  rVypna4iC1yPJjNNF+Lzo3JPMhQvd8z0LiS+sOzMypBatpRUAQsuBB0co4MCUc1pQ47zFkdRomxC
  HUEpKwe80hprUnEteYR388jl3rd/SueE8yIJmI9KdIbyxGOGnmcZLMs6FNRVqqglIQku1DYBB957
  Q3LQecy8+fZmbMHYugXosJGMKlDIoUa67JCPFGq3dyJljY6lStCTckwcw1kinySIQgY07LuOJjBH
  aF8WszDGSaBDlmrPdiurVXNSmnpWiFTKt0nXomZVjA57sFqCS+VZG1+crpNK7LYTNsR1SjC1o9lo
  o11GXUbIrZmzOIMQDeu+MYpZAilkWI9WWkqtVdGmSoZk3pSzemTNIzOvhlglGZCFOGcyWJzEfz2l
  Q9+OWZhzztW4jsk5dzhkorthlyl/PMV2rlXD2HQ0XK+K2QR1TnZbo8X0Y2HcwFGmNNgguqWXZoha
  amz5QyPApBSAAf8q0iyxlarsMYOVd6NxiUskp9ZM63gSeylJKr9GYMzsDOuhCn5EK+CkCDm4tMGY
  LUqDEvS86SltOFzyu0QHllDVIiOWtz5hIJMebJFcyWbKRmkYyCN5vBJMYwzKetcxxnCGsIUXJe23
  IIN6nBhCbBroVtRxM3oIa31o2VWUknz6KnScaeS1yl1FgpOFnxJmgK7V1GTarQtNNPQ0VRBcyC82
  Y3QYejxGN2YezDV6JtjiBIIF6zUXpIlIl3frz4Patcb44lkHuVOxi723tnPIsxHj/mZEZKxDxmT0
  zuONSs3sQsZTyQiWdds38kr1uNLIGLzXSvxXnyRXFChKClJsIyUm5if7u3QN4glmJhVeIYWDveqh
  ramzWNbeXgat9/KvW49xpjMdJQ1Xa2YjCZ2s0ZKfZXPJVkqDWpfGFt1BU1pwcvixEJVwOafF89+t
  DTELbeKUqhmHol3Clv49iSg9nryx3PdJEd10jsqRGr2rJHUiI8QX4dX48jv1SbLGBkCTX5Kfaa2V
  rmKWvLaoKeSb07cULMmy9nXLbUtMJ1cqglJStCXvJ+tJHvEkbnRqUk3ITLX5I+Y3+bHy9ah9z3bM
  LJEBampE+E+Ckco4juHeqiIW5Q4o4E90MSUixid+rULEN+ruII66tc4sWArwpet2rctWWGnQymtO
  /YPOrcQ2j8naXkr8H+DmQcPYEoUgE4ogAAHu5cIi5gKO5kzUQoiW8MIa+GG9B8u3AGo9CAJUDmJT
  AOKY2S+w/YOQrcLEd+MuJGxuIank7sporbAvAsnXC2/CKup8Qc2i+sPK8yIiFKveIgVaNMDGEIxZ
  BcbKEIJM1ALC3UoWh28Kmmq8o5D0u7D4IjB88CKWvylBDIXMSwVkCUk0YOaqbKAwakEoeWLMMWDG
  PeQiOQruOCnU9AnSbsxgtWQuEYiEvgp8JwJS7sOwnkg1BVBYbSJSEYM2DnDg3NDmhaKGMLDukc5q
  /+sa+GscqfF2sazWGdCOSRDY2bCik4V218k8xcKYDWbs+gteN6RMp9E0vU4qv2nm6cnw/SnmRMrc
  +2JOpWvavQIgVoVqD2SUEI/o9qJTHZFkGc+OF6o8wySiuy98saufB2zS5zHwzDABD8oWKpDgPeVG
  SCC0JSnG6hCm9YI8tKPKv7A7BFC1HGIGveXAxknUt5G6I2xqIvAonkHetecvBUSpFUS2xSPgXI9r
  DiL1BnHhFow0OcI8QCo8mMscIsobHyss1WzDCIwi0SQ4z2JCXOxQI3CNHCnq/LBc2ED2+Uzsp8R2
  WHA4pWIfE4M6xrKrI46c2TE0LyAQl8EISQDXDYPgXM1uPobKJC3MKMIqIRDouyIs1aV6JSj1CHH7
  LrF8KMw6s6LgI8S0JEz+qU0qgkm+e+AQl6Ck7S/IzwTsnUcIM7MdFHMlE4MclEJHBOPSdipKakr4
  MyM8U4mYEIM27hEC/pDkGsjyswkcy4KSkbBzBzLw8NJw1lF+Hu1iJ+J83qxaxOhW2UbsC1N+POCk
  Qyn3Mu/UnGKvBOFrMjKuxpKuM7OVMwnQ7dCOnULygim8RgR4WuJUcIZm7cZmPTBaKXDkGM+PNQ1C
  YyKsT0RQLmKRB9CFL0LA1iheo8ueI8SoWTKOEI0Gz+V2C0107cJMTeMc4pGkxs3up8IfMrMg+VIb
  MsI6NpG3Myxim6akE5PA08Ko7g/VDc9rNKKXFgdi5WIEkdPMKMIwMQnqxqQahnLUJIPfNtLo+NF9
  LwzNPsKQSC8ulENoqBCWMgvE/LQXG49Y2FDJBgvFOkQzBOlIhnDJQjGa+eiAxqkoUrBYFLPEdmdI
  LuCUCU9g8uVQfm/vRKsxHkIsIwPBIuI9FASCqAVGPePErE1KxFAFD7RuLCmWSCzy7dE4r1K0JVOn
  OnRZKPSQ2hGaNpSPUShnG2WqTzKnPIkoI2tWJUIegCMW3LGcPeC017S2qlTKo9ROIcIyIwtuMXKx
  FAKZMtOWQAhcpGjpJ2zEm2scpOMs2TUKlCU44oEo4pTY0TTaJFV7P4xY2TBdP1SWQVKPE1E1I0Gs
  PETcK+M8OMulWaPGV8ZUUXUm1AIlVAo9TNVEHuI4LAFqOY9ZVSJSlKMyG8UczYjyoYKC5wJNRqzA
  Oaz6My39XtN7VolEJFCNU0z6bK8unwMynbWBCm6rUOKZKPE8rsODV3I2XgKeJcLkWyIoLYIwJiIo
  LRYzWcywRhW7RNY/TPXawtXHUAUhSeS1DKYiFqfOFKWOD2yo52IyvEP2T0IYV0V2k7ZylcgTGS0B
  N68zXwSw2S+c8wJNWLOSnc+5EwRMnUx5LOQFYyMMIuOVY2IoRgIpW1W9HkJvY+/xaoJ0tU0ZV5Cm
  TMPeQadM6i8PXSF6YjbaTdFKOHFAxVN6lijioVZ6VtZ4nDP8nEz+ZnSOqBQoWqiFCdG/G+xgaqak
  DmPsJGFrHlO0KC1JYraoIlazJbW2/wK5a9VEeCKRTQpxUKkkJMnafeqAXcPeJ/LpL5XYIkQALjDM
  JtYFb8Ya10BzESD23+0JbO8pUa/ZCPBPYXI1KitdaW2CXqeaSaIYFabWTcJnUqK4OYITcs3MJio9
  Je7nU/c0y4PRBqrot2xgphL9SfFiG8Y6vAIUJNfQrsI+tNIHBU2SznBVN7Dg2bJRcHVVOVMnIncN
  aZG5cY/UtMDXFgY4OYukKgIZeiOcK+yxRKOVevZBBnPNa7ZFXAwyMQIKtKpynrUCfw3KT4vRZWu/
  apGdPweWS0pQPrX+lEMzBchrDJCW2elDCPIwTPf7T/fkQWIoE4RAJOGsG8KvebS6hm6+T0Ypg1gb
  HgsxiVgdesQozDVC3RaoJOwyISHfgxMeI2p0J0JnDNC8U4teMvdlcYI/jI4knKlRaGPfGLd2xslB
  fyMcxqxnGutWM64oxSJaouJHeaF7j1j7HhOAKo46PgqEJXgZcxPMbnHkIky0IkwsT0KHTNczc2kT
  ZGIyPGvZi8PEIgXaJsS4n4hYRBHkJAK+ZUy1QA1/dO8vfeMbSdQHVVjlKhFHVReEp8lJX5cbSwy0
  bSIwbSIoFrj0VQKWuOeShUUmqkUjIEp8UiK+NrQ3lspaJAMWrqIc73inaoHeJJgytq9Ez2XmjIyW
  bXPMKaIIQ0IwXcJsMbbPJRffhnMuTtBO6bE3C3I1I1Ky6MNNgG/s1sTASqSaa2IIVPlAJNYgeOgc
  L0SyJsSyUhC+pWVEvmpXIOJMcNHbBO8gRMpwIRl7jInyS3mOV0LuE48abXHkn3JYakPm7e6OI654
  0GMlbPUZYVli0WxpWOz0Q+QWcQuROGMXceIaHOHuXFgIaQz9OKgaqlgAMtKOno+a8gPYnQSsffBO
  xQJSxcSCnQJIIYxuvJOKlS9OeknDpIK0Io4+uQ0iZnKbCK3vSZcDbPYNKOLM6tT++YI+zyGdqAXk
  6Ox+JVeaGdh+KZmA9mIpn6lmdGXhoOLyXGI9S6iOvmxgUiIYMvkE6PskZmv68yxweW0CXEnzoMhU
  XjcUOJj0wAayyQXuwUhUwLR5nevQQveDKwxreFVRVwNOIpeZHlsrsrsPiDHhj+XEtMovHhsIX1MB
  tAL0JBsinQNJqlRDKOPmQ5CiTKIhIOI8S6vrU2PgeWS6S8lki+YEeagWg6V2UmVS7TOGZ+ldHQIJ
  OpC0Ryp7Ks/YiAnlgGVItMBzuwVLUoIpFgKptQGsHOHeI+8aGNr+i7BQJFuoqlmlBVrTqToLU3TX
  CjoTkJIRGcnEcPIOKXwydII9vC1oYaaSrRpSuYIYarK/S6Pee6x8nDsgI/rSmtYbA9IbpyUiIIKb
  siv7lInFIOP8IZvoKYKwpJr5PMGNr87EMzOGJsX1sQABQwIxvyQ7ma7hBbx9jIZ8JTqOUnIQcPoK
  S+fiqEbMKpm+1vuxxUaKLuQWIIr455xypXsYjTEdQwJUvTKpwatMVOMycMKW9ivqcOVOPeVFzVgG
  PhOLr3zNU2JsBjS6Vsewr9PIL1wThKSWIgPsKpOBw6ew9MlmwIPhuwwIxwhZt2hWgZ0Xr2VQcYrQ
  ktLCIZU3RDCjj7HlrF0rzIJNzCp2MXOVj5j7h9NQ08y1nMKZSxj3HlBW2mew7Du8Xr2OXp00TBRG
  AA8h0ofqPwK+PaIhqOVbU1m8VkVRvKVd0UhUhYgrt3mKoQ7EuK2bpyMZx9wsMfh3zkovPMUnqlIE
  P1xcKprLu2/mIIF6GdHhcfPNr8HOIiG9iAX+yQewX4LuwFzI4yaCBjx5sIOqn2r+wLwghVx4XgJN
  pN2Ui8ll45qs1uqFzGcMvq6O0UJSaGNNoKziXqld1bBR0BfctNr9NRwJNRSwIw7gIJsqP00609FU
  R5yLcdkWHP4H4uVUXqeXmKVoV2NIKXqPmL2cqkZ41uwKS5qr4yfKXp6khZV68hQ3MsXthbCjcYVI
  4oX148i52OaIP0IYSzO3PNrF4LiB7oOJ38P4K+n2WOtN4B6CKvh7LCIJyLNQVuaK9OVkuBx3oJ1C
  6Pz/tT0eLz44lSxV0WSyKo0UKXopsLX4v0TMnvGYNJqqcPKa7fKKpSMzw2Z8Pfy8XkexvDxGRAy1
  cfkX4L4JiByLHh8II3j96Hr9iBLGIgQWIxBWIZuJ4702JF2z3CPf5QdJugKpt39EqlS7ywVl8zBU
  v1GdRDGZ1GZnqcSsiLCiQaIgnaSCrUSzPxx5KaI8XsYSeQhZmL+qdx1jh77sRht7eb5ySOIYIAjE
  4nH+tV6xn+a0YjIKvV6/xiQiU/xSOSE/4sUn+GBCKYpFn+ezWc4SWi0/ykSomWilF5NJ4tFwBMwA
  OZAUpY/5ZEzmazG/zGWonQY1KYvLYvPpOjDnP6U/yUQhy/znKZRUqpVjXJqoY4mIRjUyUUp+MbDE
  BSMX/AoIe0IhH/DoenFarX+hIW/29e3+zms1n/f29gb/IYHd7yIZBY5PYanEYnKpcY5+QqsQsxEK
  xY41MX/NAAUtFIabJZOlD3P6DJzHWDGOY1XpXUYTXpRVqFU8xSa1lKhmZtU7TU5tF4zUJVKLG/4H
  BGNB7jDsRDG853fgW912t1X+53O94Tb43FX/HeFZ4jnctyuJ68xutdXKjas9oDnPYTtCEMY9qdY2
  j5q6k6mp+OauDXBCQqFAT2KA5KfKdBKkKui6wuMkDdn+yyNC0nzpsMSioK4e7wO7Ei9ROd53vA4q
  PousDiNhDSJRmi7MQ43yWI0qKXCUmCbIxGjQNyoDMpaqaiKoLSjqwprYtGrbYvuhMpwNDisKMu49
  j2oEci0n8JwyiyJhSzMyxs5KHIQYxalqkLxO8wbqvA7xzp1DqIIif4ILSiCQPNGbOuWHMvpQMY1y
  Ci6ovasTRs4z6aUWoEFyJKKqQSraTqEi49pau7xDmPaSDG/Et1HTxGLxN8uS+p1QpRQsMhTPrMIn
  MdAzyiZSrrDTRmMvyCmMhD0xdYrFIuDE9CFQ6dDmuEO0Q2FNDXLlpRrWCTssytCtA1tFSBI7awHD
  ye0QoKXUKt8uVDLhOLzBFEJUicty5elLpJU0up/R8dPK8lH2OijM3sJUEmdYSMSAisXzLgSvvIHM
  fWw5Cf4ijTLJOJVSV7fdC4jbNmNgn8htwzYcv7KbKQikj75ZBN2KpKd7Xg29sxpez70RL6NPvLky
  zJiNevUyLlwtYtayDW0ZMUqdkqmCE9YWzSNMgjFCjXVSyWinE9z1W8fUQGLl2XRDQICAAA4BAAAD
  AAAAAQAsAAABAQADAAAAAQBAAAABAgADAAAABAAAGLQBAwADAAAAAQAFAAABBgADAAAAAQACAAAB
  EQAEAAAAAQAAAAgBFQADAAAAAQAEAAABFgAEAAAAAQAAALoBFwAEAAAAAQAAF/4BGgAFAAAAAQAA
  GLwBGwAFAAAAAQAAGMQBHAADAAAAAQABAAABKAADAAAAAQACAAABUgADAAAAAQABAAAAAAAAAAgA
  CAAIAAgACvyAAAAnEAAK/IAAACcQ
CATEGORIES:Personal
X-ABUID:F9DA5726-C706-11D6-ABE7-00039384D4B8\:ABPerson
END:VCARD





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.