赵翔鹏的Blog Xiangpeng's Thinkpad

近期形式化方法相关学术报告/课程

ARTIST2/UNU-IIST 嵌入式系统设计2007暑期研讨班， 苏州，2007年8月1-10号。
ARTIST每年都会在国内举办一个summer school。我去听过去年在西安的课程。

Modal Logic, Invariance, and the Fine-Structure of Classical Logic
Professor Johan van Benthem from University of Amsterdam

Thursday, 2nd Aug
9:15am--11:30am Modal Logic, Invariance, and the Fine-Structure of Classical Logic 中科院软件所5号楼3层39号会议室

Friday, 3rd Aug
9:30am--11:30am Mini-Course part 2,3 中科院软件所5号楼3层39号会议室
"Modal Logic, Invariance, and the Fine-Structure of Classical Logic"

一个model checking的问题，以及MWB安装步骤

最近想用进程代数做个client/server类型的model，server端需要并行处理多个请求。

折腾了FDR之后，我发现在FDR里不能写P = a-->STOP ||| P 这样的进程；对其作deadlock检查会马上用光内存而没有任何结果。

那么，Pi演算不是号称有replication的操作符吗？于是我今天又折腾了MWB……翻了些文档才发现，原来MWB里面根本就去掉了replication。如果写agent P(x) = x.0|P，再做deadlocks P，MWB也会停止响应，只能Ctrl+C了。

总结：所有的model checker都无法实现replication（!P = P | !P)。
infinite state真的这么难吗……

p.s. 在Windows上安装Mobility Workbench的步骤如下。

1、安装SML。下载smlnj.zip，按照sml的安装说明，解压后设置环境变量SMLNJ_HOME为smlnj.zip解压后的目录，并把%SMLNJ_HOME%\bin加到path变量中。

2、下载MWB的源代码。注意，MWB没有编译好的可执行文件！必须手工编译。

3、编译MWB代码。到mwb解压后的目录下执行sml -m sources.cm saveit.sml

4、把mwb.sh改名为mwb.bat (copy mwb.sh mwb.bat)

5、执行mwb.bat

文档：在http://www.it.uu.se/profundis/mwb-dist 下面，guide-3.122.ps.gz 是一份95年写的手册，介绍了mwb的各种命令；x4.ps.gz介绍了pi演算、时态逻辑等一大堆东西，只有第16章有用，里面介绍了pi演算的符号与mwb符号的对应关系（比如发送x应写成'x)；examples.tar是例子。相比之下FDR的文档就好得多。

此外，如果要深入研究Mobility Workbench的使用和程序验证，贵州大学有一些非常好的介绍资料。

p.s. 安装FDR也是够讨厌的。申请license后，安装说明指出要给某个文件设置setuuid位（真不知它有什么保护措施需要root权限）后，才能在普通用户下正常运行；而我迄今不知道在linux下怎么给某个文件设置setuuid位，所以我只好在root下执行FDR。。。

IEEE 通俗简介~(转载)

标  题: IEEE 通俗简介~
发信站: 北大未名站 (2007年03月23日02:11:54 星期五) , 站内信件

电子类学生大都知道IEEE, 这个IEEE就像一个大的BBS论坛，而这个协会下面有很多杂志
，比如图像处理，信号处理，微波技术等。这些杂志就是论坛下的分版面。每个版面有
版主（主编），版副（副主编）等职务。

大学里的教授负责组织人力在IEEE灌水。教授灌的水被别的论坛或版面转载或引用。这
就叫坑。大牛教授挖大坑，小牛教授挖小坑。同学们就在这些大坑，小坑中灌水。

水越多的坑，坑就越牛，从而挖坑的教授（坑主）名气也越大。根据挖坑的大小，和水
量，IEEE会评选出IEEE senior member (高级坑主)，IEEE fellow (坑王)，IEEE life
fellow (终生坑王)。一般同学只要交了注册费就可以成为student member (灌水学员
), 毕业后可成为member（灌水员）。

IEEE每个版面一般会举行一年一度的版聚(IEEE symposium)。大家从四面八方聚在一起
交流灌水心得。一些坑王会在版聚时介绍挖坑经验(IEEE workshop)。为了鼓励灌水学
员灌好水，为成为坑主作准备，版聚设了本年度最佳灌水奖(best student paper)。
一般灌水在IEEE的发贴区(IEEE sponsored conferences)。有价值的坑或者连环坑经编
辑后会保留到精华区(IEEE Transaction).

关于进程代数CSP的随笔

最近在读Roscoe的CSP书，觉得越到后面越不好读。理论很精巧、复杂，就像一精密仪器，搞懂其运作就已不易，要想改改就更难了。

CSP小心、仔细的同时建立了相互等价的denotational，algebraic，operational三种语义。虽然语义等价是个很漂亮的结论，但我以为这样做的缺点是不得不在本来就很复杂的指称语义中又加入了一些额外的东西。所以Brookes对CSP trace语义的改进的确很好。

Tony Hoare有一篇文章“Why Ever CSP?”比较了CSP与CCS设计理念的不同。比如CCS使用很少的（甚至是最少的）operator，这样可以简化inductive proof；而CSP引入大量的operator，像顺序复合，它虽然很容易用并行和同步来模拟，但引入后可以方便用户。值得一读。

最后，我的另一篇blog的链接：进程代数的几种有用扩展

如何检查latex中的英语语法错误

咱们都不是native speaker，所以英语时态搞错，单复数用错是难免的。可惜WinEdt只有拼写检查，所以用Latex写文章时总要花大量时间检查语法。

怎么自动检查语法？我的基本思路是把latex转为word，然后用Word来检查。但从pdf直接复制粘贴到word效果比较差（当然也能凑合用），所以最好先把latex转为html，然后再用word打开，下面是步骤：

1. 下载tth http://hutchinson.belmont.ma.us/tth/tth-noncom/tth_exe.zip

2. 解压后，把要转换的文件（假设是myfile.tex）拷贝到tth目录中，执行tth -a myfile.html

3. 此时用word打开myfile.html即可。建议在“工具”-“拼写和语法”-“选项” 对话框中选中“Grammar and style”，这样可以给出更多的语法建议。（建议把被动语态检查关闭，挺烦人的）

这个方法是很简单，不过还挺实用。最后推荐一下Kile这个Latex编辑器。感觉比WinEdt好用，支持自动补全！可以少敲好多键。可惜只能在Linux下面用。

说到自动补全，如果您用WinEdt，可以试试输入\begin{XXX}}（注意最后是两个右括号），WinEdt会自动补上\end{XXX}。不过，这个功能比起Kile来还是差远了。

如何组织论文（转载）

 http://www.sce.carleton.ca/faculty/chinneck/thesis/ThesisChinese.html

如何组织论文

加拿大渥太华市卡尔顿大学

系统与计算机工程系

John W. Chinneck教授

email: chinneck @ sce . carleton . ca

最新修订：1999年9月29日

最早写于1988年，后经定期细微修改

文章的主页是：

http://www.sce.carleton.ca/faculty/chinneck/thesis.html

本文已被翻译成多种语言。

简介

本文这篇文章描述了作为研究生阶段的中心任务—书面论文的组织方法。要知道如何组织论文，首先需要了解研究生阶段的研究任务，论文是其中之一。换句话说，这篇文章对你当你刚刚开始研究生初期阶段的学习以及后期的论文写作，这篇文章对你是有帮助的。

研究生阶段的研究内容

研究生阶段的研究最重要的特点是作出对知识具有独创性的贡献。论文唯一的目的也就是证明这一点。如果你无法证明作出的贡献，那么你的论文可能无法通过将会导致失败。

简言之综上所述读完这篇文章，你的论文需要体现以下两个要点：

l       确定一个值得研究的，并且还没有获得解答的难题或问题；

l       你已经解决了该难题或回答了该问题。

你对知识的贡献主要在于对难题的解决或对问题的回答上面。

研究生论文的内容

由于研究生论文的目的是证明对知识作出的具有独创性的或具有裨益的贡献，那么阅读论文的考官要能够在论文中找到如下问题的答案：

l       研究生研究的问题是什么；

l       该问题是不是一个好问题（是否被回答过？是否有用处？）；

l       研究生是否能够使考官相信该问题被充分地回答了；

l       研究生是否对知识作出了足够的贡献；

在证明你对知识作出独创性的贡献之前，你需要清晰地阐述问题对证明你对知识作出的独创性贡献是必要的。为了证明你的贡献的独创性和价值性，你必须详细地对论题及与论题相关的已有文献进行评论。然后你必须在文章里通过进行直接引用，通过引用必须能够证明你提出的问题还没有被解决被回答过，是值得你去研究的回答的。描述你如何对问题进行回答自己的解决方案通常是比较容易的，因为经过研究生阶段课程的研究过程，学习你已经对自己的研究成果耳熟能了解了详了（该领域的）详细内容。

如果论文不能够对上述几个为数不多的问题不能做出够充分的回答地说明，你就有可能要重写修论文主修科目了，否则你可能会在答辩中彻底失败。为此，下面给出了论文的一般框架，突出了如何以合适的段落标题和论文的组织来回答上述问题。有些教授可能喜欢不同的组织方式，但论文的必需要素是一样的。进一步的说明在框架后面进行阐述。

牢记一点：论文是正式文章，论文要素措辞必须放在恰当的位置确切，内容材料不能重复。

论文通常的框架

1.简介部分

简介部分概括地介绍论文的主要内容----不是对每个部分进行（详细）描述。简洁地概述问题，说明比如为什么该问题是值得研究的，也可以能概括一下取得的成果（在论文的后续部分再详细阐述）。这是对论文中主要问题的综合全面概括。

2.背景情况（可选部分）

简短地概括一下背景知识是必要的，尤其当你的研究涉及两个或多个领域的时候。这意味着论文读者可能对论文的部份材料不熟悉，你有必要在这一部分进行阐述。定义一个与简介部分上面给出的论文上一部分不同的标题可能会更好一些，例如：“Fammis代数学简述”。

3.技术发展水平的回顾

在这一部分，你可以回顾一下与论文相关（领域）的发展现状水平。再定义一个与前面有所不同的合适标题，例如：“Zylon算法的现状发展水平”。目的是展示目前该领域的主要观点发展水平（关键性的分析在后续部分展开），但不要包括你个人的独特见解。

可以根据不同的观点来组织这一部分，而不是根据作者或发表的论文刊物。例如：如果到目前为止已经有三个主要的关于Zylon问题已经有三个主要的算法的，如果有必要你可以把这些算法组织成三个小部分：

3.1 Zylons的迭代近似；

3.2 Zylons的统计权重；

3.3 Zylon操作的图论法；

4.研究的问题或问题陈述

工程（学科）论文偏向于使用“要解决的‘问题’”这一字眼，而别的学科则偏向使用“要回答的‘问题’”这一词语。无论使用哪个，这一部分主要有三个内容：

1. 对论文要解决问题的简洁描述；

2. 通过对在第三部分的直接引用证明你研究的问题没有被回答过的进行正面的阐述；

3. 讨论为什么该问题值得回答该问题；

上面的第二条是对在第三部分给出的信息的问题进行分析。例如：你的问题可能是“开发一个在有限时间里能处理大规模Zylon问题的算法”（你需要进一步描述该问题中“大规模”和“有限时间”的含义）。在你对（该领域）发展现状的分析过程中，需要说明目前的各种方法是如何失败的（即：只能够处理小规模的难题，或者需要花费大量的时间）。在这一部分的末尾你需要阐述为什么大规模快速的Zylon算法是有用的，即阐述它可以应用的场合。

由于这一部分是读者肯定要关注的，所以在标题中用“难题”或“问题”这些字眼。例如：“要研究的问题探究”或“问难题陈述解释”，或者也可以是更具体的，如：“大规模的Zylon算法的规模化问难题”。

5.描述你是如何解决难题或回答问题的

论文的这一部分结构更为自由。可以有一个或几个部分和子部分。但目的只有一个：是使考官相信你已经回答了或解决了你在第四部分提出的问题。只解释给出你是如何与解决难题或回答你所设定的问题相关的内容。不要包含可能把你所犯的错误或走过的引入死胡同的内容，除非这些内容是与回答问题确实相关的论证。

6.结论

在结论部分你一般可以包含三点，每一点可以用一段内容进行单独阐述：

1. 结论

2. 贡献概要

3. 需要进一步研究的部分

结论不是对论文进行随便地总结：结论是你所作出推论的简短短而精的描述。，它有助于把这一部分组织成简短的几个段落，按重要性高低进行排列有助于组织好结论部分。所有的结论应该与第四部分研究的问题直接相关。例如：

1. 第五部分阐述的解决方案成功地解决了第四部分设定的阐述的问题。已经被解决了，从哪一部分到哪一部分这是一种适合于在有限的合适的时间内处理大规模的Zylon难题的新算法开发出来了；

2. 在改善的Zylon算法中主要的机理是Grooty原理；

3. ……

考官对于贡献的总结看得更为仔细。这部分你要列出对新知识的几点贡献，当然，论文本身必须能够证实这些贡献。结论贡献经常和论文其它部分重复结论交织在一起，但没有关系。列出按重要性排列的若干段落也是比较好的办法。例如：

1. 开发了一个解决大规模Zylon难题的更快的算法；

2. 论证了第一次使用Grooty原理进行Zylon计算；

3. ……

这部分也应包含论文进一步的研究的内容，以便将来研究该问题的人能够从你当初解决问题时的想法中获益。通常最好用简短的段落描述一下。

7.参考书目

参考书目要跟第三部分描述的技术发展现状密切相关。大多数考官主要看其中是否包含相应领域的重要巨作，所以这些文献一定要列出来并在第三部分进行引用。当然，如果考官发表了与你论文研究领域相关的文章作品的话，他们也会看看自己的文章是否也在里面，所以最好列出来。而且，考官可能会问你类似的问题，阅读考官的作品通常会使你有一些线索。

所有列出的引用参考书目必须在论文主体中进行实际引用。要注意参考书目区别于引用书目在对于它包含那些可能没有直接在论文中引用的书目，要注意它们的区别。根据作者的姓氏组织参考书目的先后顺序（推荐），或者根据其在论文中引用的先后排列。

8.附录

附录中该写些什么呢？可以写一些在论文进展过程中遇到的有一定难度困难，但是却能够帮助确认证明你的结论果的内容。通常是过于详细而不必置于论文主体中的内容详细的本质内容，写出来让考官能够细读并充分地相信你的结论。例如可以包含程序清单、大量的数据表格、冗长的数学据证明或推导等等。

几点关于论文框架的参考意见评价

再次重申，论文是向考官证明两大主要问题的正式文章。第三、四两个部分介绍你选择了一个值得研究的问题，第五部分介绍你的解决方法，第一、二两个部分引导读者进入问题，第六部分突出整个论文的重要结论。

要注意仔细区分哪那些是别人做的，哪那些是你做的。使考官知道这一点是很重要的。对问题进行描述的第四部分是明显的分界线，这也是把它放在文章中间的主要原因。

着手开始

着手准备论文最好的方法就是列出一个可扩展的大纲。列出预计在论文中包含的每个章节形成目录。每一章每一节写简短的几点描述其内容，整个大纲可能只有两到五三页。然后应该和导师仔细地评价一下大纲：是否存在不必要的内容（即跟阐述的问题不直接相关），如果有就删除它；是否少了一些材料，如果是就加上。在拟定提纲阶段要早作决定，这总比等到你写了一大堆又不得不丢掉更省时间。

需要花多长时间写论文？

这要比你想象的长很多，即使研究工作已经做完了，模型建立起来了，计算也完成了，留上一个学期来写论文是明智的。不是因为打字要花这么长时间，而是因为论文的写作是对论证和结论的完整组织。是在从最初的结果形成到最后的经得起完美地组织起来，使之能够经受专家级考官详细审查的完美论文过程中，你会不断地发现缺陷，改正这些缺陷是比较耗时的。

也可能是先前你和导师只有非正式的交流未正式核准的，你的论文是你的在导师第一次正式看到你的完整思路发现标准概念后。，这也是最容易发现你的就应该去察看先前存在错误误解或缺陷的时候。你需要时间去改正错误或弥补缺陷。母语非英语的学生把观点阐述清楚可能有一些困难，所以就需要多次的修改。当然，导师有时并不会不立即审阅并返回你的论文草稿。

底线是留给自己充足的时间。草草了事在答辩时不会有好结果的。

提示

牢记论文读者的背景。谁是论文的读者观众？在他们阅读你的论文之前，你应合理地预测他们对该主题知道多少。通常他们对一般问题是相当的了解，但他们并未像你一样对近若干年该领域的发展进行密切关注：这就要求你把新概念说明清楚。有时在心里描绘一个具有相当知识背景的人，并想象你在给他直接解释，是很有帮助的。

不要给让读者制造麻烦难办，这是相当重要的。你该明白考官感兴趣的问题没有几个，要在明显的章节里面给他们答案。如果他们需要化费时间找到把你要解决的阐述的问题、答辩的问题、你的解决方案对问题的回答、你以及论文的结论和主要贡献。找出这些来越困难困难，他们的心情就会越差。，最后很可能你的论文就需要退回重修改了。

以上意思就是：论文要尽可能地清楚！把问题仔细的解释明白，用合适的标题等方法突出重要的内容。论文包含的信息量是巨大的，要保证能够把读者（的注意力）引导到重要的问题上。

记住论文不是小说，通常不是按照年代顺序叙述问题，而是一篇对重要问题的解答进行阐述的正式文章。

避免使用诸如“显然，这是……”或“很明显，由于……”这样的字句，因为这些语句暗示着：如果读者没有看懂，会被认为是愚蠢的。他们可能是由于论文解释得太差而没有领会。

避免用一些使人反感的语句，提出一些仅仅是你个人的观点（诸如：软件是计算机系统最重要的促成部分），而没有在你引用的文章或解决方案里得到实证。考官喜欢挑这样的语句来问：你能不能论证一下（为什么）软件是计算机系统最重要的组成部分？

关于计算机程序及模型的注意事项

论文的目的是要给出你对知识所作出的贡献。可能你开发了计算机程序、建立了模型或是用别的工具来证明你的观点，但要记住：论文是阐述你对知识的贡献，不是这些工具。当然类似计算机程序的工具是好的而且是有用的，但仅仅是这些工具你还不能够取得高层次的学位。你必须能够通过工具的使用或者工具所能加强包含的观点来证实你对知识的贡献和你的创意。

硕士论文和博士论文

对硕士论文和博士论文的要求是不同的。区别不是在于论文的格式，而是在于问题的重要性、对要解决问题的探索层次以及贡献。博士论文当然要求解决更难的问题、作出更具原创实质性的贡献。

硕士论文对知识的贡献可以是类似于，达到对某一知识领域的改进提高，或者是已有技术在新领域中的应用这样的性质即可。博士论文必须作出对知识作出具有实质性和、有创新性的贡献。

Translated from English to Chinese by Qian Hong (qianhong@icss.com.cn)

形式语义学的相关材料（转载）

原文链接是http://www.w3china.org/dispbbs.asp?boardID=64&ID=38540
这么多经典书籍，我只认真学过2，大致翻过4…… 听到“范畴论”还是会头大~

---

形式语义学的相关材料 by accueil

UPPAAL 4.05已推出

Uppaal是我用的第一个model checker，也是我用过的所有model checker中界面最漂亮的。(功能也很强的:P)

2月12号Uppaal出了新版本4.05，下面是从官方网站抄来的new features。如果你只用过3.4，那可一定要好好看看了，因为4.0除了速度提升，还增加了不少有用的新功能，比如用户自定义函数，非确定性选择，量词等等。

---

UPPAAL 4.0 is the result of over 2 years of development. It is more user friendly, has more features and is faster than UPPAAL 3.4. The following is a summary of the most important improvements.

Performance

Runtime and memory consumption has been reduced. For some models, a drastic reduction is obtained, whereas for other models runtime is comparable to UPPAAL 3.4.

* New and improved abstractions provide dramatic performance improvements for some models.
* Memory management has been improved, giving a typical reduction of a factor of 3 to 5 in memory consumption. This does come at a minor cost in performance.
* The generalised sweep-line method has been implemented in UPPAAL. To use this feature, you need to define one or more progress measures.
* Symmetry reduction.

Language

The modelling language has been extended with new data types and user defined functions. At the same time a number of inconsistencies have been eliminated in the language. As a consequence most UPPAAL 3.4 models need minor adjustments in order to work with UPPAAL 4.0.

The GUI can convert most UPPAAL 3.4 models to the new syntax automatically. Both the command line utility and the GUI recognize the UPPAAL_OLD_SYNTAX environment variable. Defining this variable switches UPPAAL 4.0 into a compatibility mode, in which the 3.4 syntax is recognized. This option may also be of use with third party tools that generate UPPAAL models and execute UPPAAL as a backend.

The following is a summary of the language changes.

* New types:
o Record types.
o Type declarations.
o Meta variables.
o Scalars.
* Partial instantiation of process templates.
* Comparison and assignment between arrays.
* User defined functions.
* Forall and exist quantifiers.
* Non-deterministic choice on edges.
* Minor adjustments to more closely follow the syntax of C/C++/Java, including:
o Declaration of constants.
o Assignment operator changed from := to =.
o Explicit declaration of whether parameters use call by value and call by reference semantics.

Graphical User Interface

A number of long standing issues in the graphical user interface have been fixed. Although we feel that the improvements greatly enhance the user experience, most of the changes are minor.

* The editor now has unlimited undo and redo.
* Syntax and bracket highlighting.
* Rectangular selection.
* Restructured menu layout.
* Better recovery from fatal server errors.
* Improved Mac OS X support.
* Custom colors on locations and edges.
* Comments can be added to locations and edges.
* More model checking options are available in the GUI.
* A search component for the help system was added.
* Most labels of an automaton can be hidden.
* Tooltips are used in the declaration editor and automaton editor to show syntax errors. Tooltips also show useful information about locations and edges.

Command Line Interface

The command line interface of verifyta has been updated.

* More freedom in choice of extrapolation.
* Can generate pre-stable traces.
* Can generate fastest concrete traces and concrete traces to deadlocks.
* Can show statistics about the state space.
* Can compile a UPPAAL model to a stack-machine program. This is useful as a preprocessor for alternative verification backends.

如果你对formal methods感兴趣，请看形式化方法研究专栏的更多文章~

在软件所讨论grand challenge

Tony Hoare提出Grand challenge之后，国外有不少人响应，但国内基本上还没有具体动作。昨天在软件所有一个关于grand challenge的“学术报告”，去了之后才发现其实是一个panel，国内不少牛人都参加了，北京的，南京的，长沙的等等。

虽然大家还是觉得grand challenge这东西比较虚，甚至“不能拿来申项目”:P，但至少ppt中还是提到了几个比较有趣的问题，比如如何对程序语言中的reflection建立runtime的类型系统；如何对annotation建模；如何验证byte code。

其实我印象最深的一句话是zj问"我们中国做formal methods的到底要做什么"，"是否只是发发paper而已"……而L院士说”我们就是吃这口饭的"……看来"迷茫"是本研究领域的普遍现象啊。wj说“凡是漂亮的理论，多半在实际应用中不太灵光”。研究了多年的理论总是无法结合到实际应用，的确让人比较郁闷。

虽然还是看不出什么大方向，但至少在小的地方我们的研究还是有一点贡献，我觉得这就达到了研究的目的。就像老板所说，fm首先是帮助人看清问题，看清了之后就容易提出一些idea、改进的意见。这后半句才是关键，否则fm就只是rewriting，没有什么意思了。

CiteULike: 学术专用的Web 2.0收藏夹

CiteULike是个非常好用的在线论文收藏工具，是学术版的del.icio.us。先抄一段官方的FAQ：

什么是CiteULike？

CiteULike是一个免费的网络工具，它可以帮助学术工作者分享，储存和组织他们正在浏览的文献。当你在网上查阅到一篇你感兴趣的文献时，有了 CiteULike，你只需轻点鼠标，就可将其轻易收录到你的个人文献库中。这当中，CiteULike可以自动抽取这些文献的详细信息如作者、期刊名、 文章卷期、页码、出版商和摘要等信息，而不必你自己花时间键入。所有的这些工作均在浏览器中完成，当然你也不需要安装什么特别的插件。

由于你的个人文献库中所有的资料都是存放在网络上的，因此，你可以在任何一台有网络连接的电脑上随时查看。 你在与他人分享你的个人文献库的同时，也可以了解谁正在和你看同样的文献。作为回报，这将有助于你找到与你研究领域有关的文献，而这些文献可能是你原先所 不知道的。

当你写文章引用文献时，你可以将个人图书馆中的文献导入到BibTeX或Endnote的文献管理系统中，组织你自己的参考文献。

CiteULike是一个动态的文件系统，因此，如果你需要，你可以找到你在数个月前存入的文献。

这些文献只是以链接的形式存储，它们的储存方式与CiteSeer或PubMeb没什么两样。现在CiteULike上的数据库主要是关于生物与医学方面 的，但是将来还会有更多专业的数据库加入进来。目CiteULike支持的数据库系统有： AIP Scitation, Amazon, American Chem. Soc. Publications, American Geophysical Union, American Meteorological Society, Anthrosource, Association for Computing Machinery (ACM) portal, BMJ, BioMed Central, Blackwell Synergy, CSIRO Publishing, CiteSeer, HighWire, IEEE Xplore, Ingenta, IngentaConnect, IoP Electronic Journals, JSTOR, MathSciNet, MetaPress, NASA Astrophysics Data System, Nature, PLoS, PLoS Biology, Physical Review Online Archive, Project MUSE, PubMed, PubMed Central, Science, ScienceDirect, SpringerLink, Usenix, Wiley InterScience, arXiv.org e-Print archive, 尽管如此，你也可以录入其它CiteULike目前不支持的文献数据库系统——当然这需要你自己手动输入相关的信息。

CiteULike的服务是免费，并且将继续下去。你随时都可以管理你的个人文献库并免费浏览其他人的个人图书馆。CiteULike的核心数据库每15分钟备份一次，因此，你的个人文献库里的相关信息会被安全、妥当的保存而不会发生遗失。

---

Web 2.0的优点在这个网站上得到了全部体现。以前想搜索某个方面的文章，只能用关键字查询，很难保证搜出来的东西都是有用的；而使用tag技术，相当于专业编辑帮我们做一份专门的索引，因此搜到的都是相关的内容，并且可以从打分系统看出某个文章的好坏。或者直接从一篇文章入手，看看收藏这篇文章的人还收藏了哪些文章，也可以达到类似的效果。

更不用说它还有超强的bibtex导入功能，对浏览器作了一个扩展(其实就是一个javascript bookmark)，直接分析HTML来提取bibtex信息。以前特别喜欢ACM和Citeseer，因为这两个网站的文章都带bibtex，而IEEE, Springer则没有。有了CiteULike，所有的这些流行网站就都支持一键导出bibtex了。

缺点就是现在用户还太少，文章也不太多，打分的人就更少了。不过当我看到竟然有人收藏了我的一篇文章之后，还是小小的惊讶了一下。