并发Haskell程序：模型检查技术调试与验证

理论计算机科学电子笔记113（2005）201-216www.elsevier.com/locate/entcs并发Haskell程序沃尔克·施托尔茨亚琛工业大学，52056 Aachen，Germany弗兰克·胡赫Christian-Albrecht-University of Kiel，24118 Kiel，Germany摘要在本文中，我们使用模型检查技术来调试并发Haskell程序。指定断言或其他属性的LTL公式在运行时进行验证。如果检测到伪造公式的运行，调试器会发出警告并记录导致违规的路径。可以在运行时动态添加公式，从而提供一定程度的可扩展性，这在源代码的静态验证中不可用。 我们给出了一个全面的例子，使用新技术来检测并发Haskell程序中的锁反转，并引入了一个模板机制来定义LTL公式，范围涵盖任意一组线程或通信抽象。关键词：验证，LTL检查，Haskell1介绍今天，几乎任何大型软件应用程序都不再是顺序程序，而是由不同数量的进程组成的整个并发系统这些进程经常共享资源，必须充分保护这些资源不受并发访问的影响。 通常这是通过集中这些行动来实现的 在受信号量保护的临界区中。如果一个信号量被接受，另一个希望接受它的进程将被挂起，直到信号量被释放。组合使用两个或多个信号量很容易导致死锁。如果我们记录导致这个事件（或任何其他程序崩溃）的操作的痕迹，我们可以给开发人员1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.026202诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201关于如何调试此错误的有用建议。此外，我们不必将自己局限于在信号量上记录事件。在整个程序中使用独特的标记定期详细说明当前运行的位置和状态非常有用。虽然这种技术很像hello-debugging，但我们将展示这些跟踪是否具有附加价值：我们可以通过嵌入到系统中的运行时验证器对正在运行的程序进行运行时验证。通常，人们感兴趣的是在特定位置或整个程序执行过程中保持的条件。这些属性不能在编译时容易地确定或验证，因为不可能验证程序执行的所有可能路径。但是，这些条件的违反可以在事后分析或运行时检测到，例如在密集测试期间。特别是，我们可以从一个或多个运行中收集信息，并检测没有导致崩溃但表明在未来或后续运行中可能违反条件的行为。如果程序行为依赖于调度或外部输入，则通常会出现这种情况我们感兴趣的属性不一定是经典的模型检查属性，如活性或公平性[10]，而是开发人员已知的程序在某些时候保持的属性。通常，这些所谓的断言由雄心勃勃的程序员在源代码的适当位置放置额外的代码来验证，并且通常在交付产品之前删除，因为它们增加了程序大小和运行时间。像线性时间逻辑（Linear-Time Logic，LTL）[1]这样的时序逻辑自然地适合于描述依赖于程序随时间变化的状态的属性。在程序执行期间，公式决不能被评估为False。 我们的系统允许动态添加新的公式，这些公式在系统发展时必须保持不变。我们展示了如何使用指定公式的技术，以及在运行时验证它对测试并发Haskell有很[9]程序。此外，系统记录导致违反属性的状态的路径本文的结构如下：第2节简要介绍了Haskell以及记录跟踪并将其用于调试的技术。第3节提供了LTL的一些背景知识，并描述了LTL运行时验证器。第4节展示了锁反转问题的一个验证示例第6节总结了本文，并提出了未来的工作。诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）2012032跟踪Haskell程序首先，我们提醒读者注意纯函数式惰性编程语言Haskell [8]。尽管在调试Haskell方面有大量的工作（请参见[13]作为比较），这些主要集中在调试惰性函数式语言中表达式求值的困难：求值可能会推迟到后续计算需要的值。这会导致无法从程序源代码中轻松导出的求值顺序（例如，无法像您那样在C或Java中）。我们只限于调试Haskell程序的IO行为（由monad序列化），并可以忽略由此产生的问题Haskell我们对扩展Concurrent Haskell [9]特别感兴趣，它在Haskell 的IOmonad中集成了并发轻量级线程由于这些线程可以通信，不同的调度可能导致不同的结果。通信可以通过MVar（可变变量）进行这些MVar还起到信号量的作用，保护关键部分，特别值得分析。在IO monad中，线程可以创建MVar（newEmptyMVar），从MVar读取值（takeMVar），并将值写入MVar（putMVar）。如果一个线程试图从一个空的MVar读取或写入一个满的MVar，那么它会挂起，直到MVar被另一个线程填充或清空。MVar可以用作简单的信号量，例如确保互斥，或用于简单的线程间通信。基于MVar，构建了更高级别的通信对象，但超出了本文的范围在以前的工作[3]中，我们开发了一个用于可视化并发Haskell线程之间通信的工具，称为并发Haskell调度器，它也可以显式地操纵线程的调度这个调试器也能够重放记录，并发执行的一个错误被发现本文提出的技术作为一个简单的例子，我们考虑一个在Concurrent Haskell1中实现的小型客户端服务器应用程序：服务器ra c = do客户端ra n = doreq-takeMVar rputMVar rnputMVar a（req，c）（m，v）- takeMVar aserver r a（c+req）-- stateProp（n，m）1本例中使用的do-符号是Haskell的IO-Monad的语法糖一个不熟悉Haskell的用户应该把它看作一个动作序列和<注释以'-- '开头。stateProp（n，m）操作将用于调试目的，并在下面进行解释。204诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201客户端ra nmain =执行r<-newEmptyMVara-newEmptyMVarforkIO （ 客 户 端 ra0） forkIO（客户端r a1）服务器r a0该系统由一个服务器和两个客户端组成服务器提供一个计数器，客户端请求可以访问该计数器并使其递增。每当客户端通过MVar r发送请求时，服务器通过MVar a响应。应答包含请求（一个Int）和计数器的当前值（c）. 这两种MVar都在全球范围内用于通信和同步在服务器和所有客户端之间。在递归调用中，服务器根据请求增加其状态。通过创建两个空的MVar和派生两个客户端线程，在main中初始化系统此后，主线程本身切换到服务器。这个例子激发了我们的运行时验证方法。在第一个视图中，程序将填充以下属性：（P）如果客户端发送一个请求，那么客户端会收到一个包含服务器当前计数器状态我们想通过运行时验证来检查这个属性。在第一步中，我们将原子状态命题添加到系统中，以识别执行过程中的相关点。因此，我们在客户端定义中的takeMVar操作之后插入（取消注释）操作 在执行此操作期间，全局状态命题（n，m）有效。一（P）的必要条件是，在系统执行期间，仅出现属性（0，0）和（1，1），即，应答m属于相应的请求n。而不是开发各种算法，应检查在执行过程中，我们提供了一个通用的检查功能强大的逻辑LTL。程序员可以通过LTL的抽象数据类型指定属性，并可以将LTL断言添加到任何程序点。对于我们的示例，添加LTL断言是明智的check“P”（g（Not（StateProp（1，0））：/\： Not（StateProp（0，1）加入这个项目该公式表示在系统的每个状态（“g”，全局）中名为“P”的断言通过执行check来激活。我们将在下一节讨论并发Haskell中LTL的诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201205|运行此程序一段时间表明违反了属性。 由于竞争条件，断言的LTL属性不成立。在后台，我们记录了执行的并发操作的跟踪，可以通过我们的并发Haskell重写器重放这有助于用户理解bug的原因。跟踪是通过重载每个并发Haskell函数来产生的，该函数将跟踪输出写入文件，类似于[3]。在我们的小系统中，该错误源于调度，其中一个客户端的执行在发送请求后直接被调度程序中断。然后，服务器响应请求。在此之后，另一客户端发送其请求并读取应答MVar，但获得对另一客户端的请求的响应。可以通过为请求生成新的应答MVar并将它们与请求一起提交给服务器3模型检验LTL线性时间时态逻辑（LTL）[1]是计算树逻辑CTL的子集，并使用描述沿计算路径的事件的运算符来扩展命题逻辑。含义：• “Next” (• “Eventually” (• “Globally” (• “直 到 ” （ U ） ： 结 合 了 两 个 属 性 的 意 义 ： 必 须 保 持 直 到 最终 保 持 。LTL的语义是相对于给定Kripke结构（一个由原子命题（AP）标记状态的转换系统）中的所有路径LTL的路径语义定义如下：定义3.1（LTL的路径语义）设AP是一组原子命题。 一个无限的词在原子命题π = p0p1p2... 其中，P（AP）ω称为路径。在以下情况下，路径π满足p0π |= Pi <$P ∈ p0π |=<$i π| = ππ| = iπ |= π和π |=p0π| = Xiπ|=p0p1... |= ϕ U ψ iff ∃i ∈ N: p i p i+1... |=和j Prop a->IO（）extend respectivelyrestrict有效原子命题的集合check：：Ord a =>String-> LTL a-> IO（）在运行时将新公式添加到公式池中。最后，一个步骤消息（由任何并发操作产生）使检查线程根据当前持有的原子提议公式的计算可以有三个不同的结果，我们将其映射到数据类型EitherBool（LTLa）3中：(i) LeftTrue：公式已被证明，可以从池中删除。(ii) “假的，假的，假的。如果此条件与程序崩溃不一致，则用户可能希望继续检查剩余的公式。(iii) 右二：在这一步之后，公式简化为既不是真也不是假。必须在剩余路径上检查新公式检查线程调用的求值函数如下（由于空间不足，我们仅限于基本命题 和 until 运 算 符 ） ： checkStep ： ： Ord a => LTL a ->Seta ->EitherBool（LTLa）2'Ord a=>'是类型a的Haskell类约束。由于原子命题存储在一个集合中，因此必须定义命题的排序。Haskell类型Either可以用来联合两个任意类型。 底层类型由两个构造函数标识：data ab =Left a|右湾208诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201checkStep（StateProp p）stateProps= Left（pcheckStepu@（U phi psi）stateProps=letphiEval=checkStep phi stateProps在checkStep psi stateProps的情况下Left True-> Left TrueLeft False -> case phiEval of左假->左假左真->右使用Rightphi左假->右psiLeftTrue-> Right（psi右phi在外部表达式的最后两种情况下，我们构建了一个新的公式，必须在下一步中进行检查。从模型检查中我们知道，只有有限的一组公式可以发生。为了避免相等公式的多次检查G F），检查线程将待检查的公式存储在一个集合中。3.3并行程序只要只有一个进程生成我们用于验证的调试跟踪，那么调试跟踪的解释就很清楚。跟踪中的每个新条目对应于Kripke结构中的一个转换如果我们允许多个进程操纵全局状态，会发生什么考虑下面的例子：两个进程（P1和P2）想要设置不同的proposi。每个进程都不知道其他进程（见图1）。 虽然美国这两个过程在时间轴上是一致的，认为它们步调一致是错误的！Concurrent Haskell具有交错语义，因此如果我们将来自两个进程的命题连接起来，我们将获得图2中的模型。注意每个路径如何类似于Haskell中可能的执行顺序。左分支指示进程P1采取步骤，而右分支对应于步骤P2。如果只有一个转换离开状态，则这是这是唯一可能的步骤，因为其中一个过程已经达到了它的最终状态（最终命题加下划线）。由于这种交错，很明显，你不应该在公式中显式地使用我们在实现中通过隐藏诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201209P1：P2欧元/英镑P欧元/英镑欧QQ欧QFig. 1.分离状态空间图二. 交错状态空间“Ne3.4使用LTL检查断言在第2节中，我们已经介绍了LTL运行时检查器的一个简单应用。在这个例子中，我们只通过stateProp设置了一个原子命题。 有时候，为一个时期设定命题是有用的时间，例如，表示线程处于临界区。函数stateProp被定义为setProp、step和releaseProp的序列。检查引擎线程的步骤消息将自动生成。由并发操作的扩展版本来执行。也就是说，我们仅将系统的并发动作视为步骤，而计算不被解释为状态空间中的步骤，而与它们所花费的时间无关。这是允许的，因为只要计算结果不用于通信，计算就不会影响并发系统。执行一个包含（指定的）错误的程序，并给它足够的时间和一个此外，它打印公式被伪造的消息，并存储可由并发Haskell编译器使用的跟踪。4应用示例：锁定反转在本节中，我们将讨论如何使用LTL运行时验证器实现以下相当复杂的检查：如果在一个特定的命令中使用了两个锁（其间没有释放步骤），如果用户也以交换顺序使用这些锁（锁反转），调试器应该警告用户，因为在并发程序中，这意味着当两个进程的执行以不合适的顺序调度时，它们可能会死锁。<$P，<$QP，<$Q<$P，<$QP、QP，Q<$P，<$QP，<$Q<$P，<$Q210诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201但是，这个警告可能还不够，因为总是可以构造一个程序，它以相反的顺序接受锁，并且永远不会死锁。这可以通过在程序中添加另一个锁来实现，即所谓的门锁，它可以确保互斥并防止系统死锁。在[11]中详细描述了在存在门锁在最近的FreeBSD操作系统内核的开发阶段，这种在运行时注意到无意中的锁反转的特殊技术被称为witness[6]。在[11]中，同样的技术也被用于Java Path [15]，一个Java应用程序的模型检查器。我们考虑两个并发进程重复竞争两个锁A和B。不可能一次获取多个锁，因此必须依次获取两个锁。如果我们假设第一个进程试图以A，B的顺序获得它们，第二个进程试图以B，A的顺序获得它们，我们可以看到，系统迟早会处于这样一种状态：进程1持有锁A并等待B变得可用，而进程2持有B等待A！这种情况正是表示死锁的循环等待模式（参见。第7章[2]在小程序中，bug可能很容易被发现。对于较大的应用程序，我们可以得出结论，很难通过简单地阅读源代码来防止这种错误。即使在测试程序时，错误也可能不会在各种运行中发生。例如，可能的是，过程1和过程2从不交错执行，而是以顺序方式执行。为了调试并发Haskell程序，我们提供了一个代数数据类型，其中包含相应线程的ThreadId，以便公式可以包含每个线程的表达式。此外，我们将记录所持有的MVar我们使用这种数据类型作为预定义的原子命题。它们由并发操作自动设置和释放，如下所示：• takeMVar：setProp（ThreadProp threadId> mvarName>）• putMVar：releaseProp（ThreadProp threadId> mvarName>）此策略也可以应用于其他并发函数。通过使用这种方法，程序将生成包含上述命题的跟踪，可能按照指示错误行为的顺序。我们可以检测到这一点，并警告开发人员，他的应用程序有可能在某些条件下进入死锁在下面，我们给出了一个两个锁的LTL公式示例，如果以相反的顺序使用锁，则该公式的值为False请注意，我们必须在Haskell程序中提供固定的ThreadId在第5节中，我们将看到如何使用模板更优雅地解决这个问题，因为在动态系统中，诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201211--提前生成所有公式。如果进程i持有锁x，我们将在公式中写入holds（pi，lx），而不是使用断言中的代数数据类型。“全局”的结果对于程序的每一步，再次执行：Gholds（pj，lx）Uho lds（pj，lx）））。为了更好地理解这个公式，我们考虑以下程序：main= do takem1 m2 = docheck“lock”（g（NottakeMVar m1（phi（StateProp（ThreadProp 1“B”）takeMVar m2（StateProp（ThreadProp1“A”）.mvA-newMVar（）putMVar m1（）mvB-newMVar（）putMVar m2（）服用mvB mvA-- helper函数：phi u v=（u：/\：（Not v））：/\：（u当这个程序被执行时，首先将公式传递给验证器。这两个重载的newMVar调用触发了模型检查器的releaseProp语句，因为它们在内部使用了插装的putMVar由于当前状态还不包含属性，因此它们不起作用。当调用take函数时，这将设置相应的命题并在LTL检查器中执行转换：在当前状态下进行评估{<$holds（p1，lA），holds（p1，lB）}，并简化为在哪里，U=holds（p1，lB）U保持（p1，lA）= holds（p1，lA） （holds（p1，lB）<$X<$J）.在步进公式并取下一个MVar之后，我们可以看到新状态holds（p1，lA），holds（p1，lB）将J求值为True，这反过来又被否定并使整个公式无效。模型检查器已阻止-发现指定的属性不适用于当前路径，并相应地采取行动，例如向用户打印警告。5使用公式模板在上一节中，我们使用了一个静态公式来演示该机制。但是在动态系统中，MVars可以在时间上生成和使用，因此不可能预先生成所有公式能够212诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201为了优雅地处理这个问题，我们引入了模板。模板包含自由变量，这些变量在整个程序运行过程中使用所有属性进行实例化。这包括一旦使用新的proposition，就实例化新的公式。理想情况下，我们希望能够以下面的形式为上面用LTL重新表述holds（pi，lx）holds（pi，ly）（holds（pi，lx）Uholds（pi，ly））→G<$（holds（pj，ly）<$$>holds（pj，lx）<$（holds（pj，ly）Uholds（pj，lx））），i/=j，xy然而，在Haskell中实现这一点意味着设计一个新的语法和编写一个不同的LTL前端，因为这样的公式模板不能很容易地用代数数据类型捕获：LTL语法必须为每个新命题扩展。使用一个真正的Haskell函数要容易得多，它在每次第一次设置一个新命题时传递所有当前已知的命题，并自行决定哪些命题可以用来实例化公式。由于Haskell由于类型系统的原因，不可能像实现模板机制所必需的那样在数据结构中收集不同类型的函数，我们使用一个简单的技巧：由于所有命题都是单一类型的，模板函数只需将命题列表作为参数。模板引擎将生成所需长度的命题的所有可能排列，并将它们传递给函数。如果命题不适合模板，则函数返回Nothing4。否则显示LTL公式通过Just返回。下面的Haskell函数实现拟议模板：lockF：： Ord a=> [Prop a] ->Maybe（LTL a）lockF（p1@（ThreadProp i1 x1）：p2@（ThreadProp i2 y1）：p3@（ThreadProp j1y2）：p4@（ThreadProp j2 x2）：_）| i1 == i2 &&x1 == x2 &&j1 == j2 &&y1 == y2 &&i1/= j1 &&x1 /= y1 = Just((phip1 p2）--> g（Not（phi p3 p4）| 否则= Nothing lockF _=NothingHaskell数据类型Maybe的定义如下：数据可能a =无|只是一个诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201213我们使用模式匹配从参数列表中提取四个参数，并通过“_“占位符丢弃其余参数如果参数不是四个ThreadProps，则lockF的第二个定义通过返回Nothing告诉模板引擎这些命题不适合实例化。如果模板接收到四个ThreadProp，则必须针对附加约束测试实际内容：防护测试我们是否真的使用两个不同的线程和两个不同的锁来就像我们在上面的数学规范中所要求的那样。在模式匹配表达式中不可能多次使用同一个变量例如，在PROLOG中，所以我们必须为每个线程和每个锁使用新的变量，并在guard中显式地测试那些必须一致的变量。测试成功后，我们使用p1中保存的表达式... p4建立公式。请注意，只有在程序设置了至少四个满足必要要求的（不同的）命题此时，我们可以添加实例化的公式到已经存在的公式，并从当前状态开始检查它我们观察到，如果没有进一步的修改，例如对参数进行排序为了在设置新命题时优化置换的生成，我们仅通过维护所有已使用命题的列表来生成新置换5.1部分实例化对于某些公式，包括上面的公式，甚至有可能公式在不需要所有参数的情况下计算为True或False，或者导致最后一个所需命题的最后一个动作确实是使公式无效的命题但由于这些是时间公式，并且我们在有足够数量的参数之前不实例化模板，我们可能会错过部分实例化：对于上面的模板，我们可以在有了前两个适当的参数后立即实例化蕴涵的左侧。然后，可以对这一部分公式进行评估，并及时采取步骤。 在本例中，隐式的左侧可能会计算为False，从而使公式冗余。然而，再一次，执行部分实例化和求值的实际实现导致了更复杂的簿记：通过将此功能投影到Haskell214诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201公式否则。newtype TemplateF a= TF--模板的新数据类型（[Prop a]->Maybe（Either（TemplateF a）（LTLa）））lockF：：Ord a=> [Prop a]->Maybe（Either（TemplateFa）（LTLa））lockF（p1@（ThreadProp i1 x1）：p2@（ThreadProp i2 y1）：_）| i1 == i2 &&x1 /= y1 = (Just . 走了TF ）（\xs -> lockF 2（p1：p2：xs））--返回匿名函数| otherwise= Nothing--带部分应用程序锁F_= NothinglockF2：： Ord a => [Propa]->Maybe（Either（TemplateF a）（LTLa））lockF2（p1@（ThreadProp i1 x1）：p2@（ThreadProp i2 y1）：p3@（ThreadProp j1 y2）：p4@（ThreadProp j2 x2）：_）| x1== x2&&j1== j2&&y1== y2&&i1/= j1=(Just . 右 ）（（phi p1 p2）--> g（Not（phi p3 p4）| 否则=无锁定F2_ =无部分实例化允许我们避免测试大量的参数组合，因为只有前两个位置的一小部分参数是有效的。正是为了这些，必须生成第二组参数，为这个例子提供了巨大的好处。一般来说，最坏情况下的行为等于普通模板的先前行为该系统还提供了记录整个跟踪的能力，程序（或其可配置的尾部），并针对该轨迹检查新公式。当然，保持这种跟踪所需的内存或存储量对大多数程序来说可能是禁止的。在未来的版本中将支持步进部分实例化的模板6结论、相关工作和未来工作我们为Concurrent Haskell提供了一个调试框架，它记录程序执行中的路点，并允许开发人员通过Concurrent Haskell调试器跟踪程序的特定路径，以得出错误行为的结论。在整个程序执行过程中或在特定时间必须保持的条件可以表示为线性时间时序逻辑LTL中的公式调试跟踪提供状态转换注释，LTL模型检查引擎根据诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201215一组公式。除了特定的调试模块之外，开发人员还可以使用显式注释来向调试跟踪添加信息。调试器支持从开始证明变为False的特定公式的点开始打印跟踪的尾部。此外，我们扩展了我们以前的工作[14]，具有强大的模板机制，允许dy-当确切的命题事先不知道时，公式的动态实例化，例如：因为它们由ThreadIds或MVars参数化。还有其他一些运行时验证的方法，尤其是对于Java。Java PathData[11]是Java虚拟机的一个工具，它能够收集有关有问题的跟踪的数据，并运行传统的模型检查算法。Java PathExplorer [5]采用了运行时验证的思想，并使用Maude重写逻辑工具[12]来实现例如Future或Past timeLTL。这两种方法仍然需要几个组件，而我们的Haskell库是自包含的。Java PathExplorer还通过用户实现的算法提供所谓的错误模式分析。Compaq[7] POSIX线程应用程序的调试器允许脚本化的、基于规则的版本确认。Temporal Rover [4]检查时间相关的规范，并通过源到源转换处理嵌入在注释中的断言作为未来的工作，我们打算在图形化的并发Haskell调试器中集成LTL检查的信息，为并发Haskell提供全面的调试工具。运行时验证对性能和内存要求的影响还有待于在更大的示例中进行检查。我们希望从子公式的固有共享中获益，因为我们选择了一种懒惰的函数式编程语言。 有关LTL运行时验证库的更多信息，请访问http://www-i2.informatik.rwth-aachen.de/~stolz/Haskell/网站。引用[1] A.Pnueli.程序的时序逻辑。在Proceedings of the 18 th IEEE Symposium on Foundations ofComputer Science，第46-77页[2] A.Silberschatz和P.B.高尔文操作系统概念。Addison-Wesley，第4版，1994年。[3] T. B？tt ch erandF. 胡昌华AD ebuggerforCo n curr entH askell.2002年9月在西班牙马德里举行的第14届函数式语言实现国际研讨会上[4] D.德鲁辛斯基时空漫游者和ATG漫游者In W.Visser，K.Havelund，G.Brat，and S.Park，editors ， SPIN Model Checking and Software Verification （ 7th International SPINWorkshop ） ， volume 1885 ofLecture Notes in Computer Science ， pages 323-330 ，Stanford，CA，USA，August/September 2000. 斯普林格。[5] K. HavelundandG. Rosu. JavaPath E xp lor er-ARunt imeV er i f ic ationTool。2001年6月在加拿大蒙特利尔举行的第六届空间人工智能、机器人和自动化国际研讨会上，ISAIRAS216诉Stolz，F.Huch/Electronic Notes in Theoretical Computer Science 113（2005）201[6] J.H.Baldwin.多线程FreeBSD内核中的锁定。在Samuel J. Le Bauer，编辑，2002年BSDCon会议记录，2002年2月11日至14日，美国加利福尼亚州旧金山。USENIX，2002年。[7] J.J.Harrow.使用可视线程检查多线程应用程序。In W.Visser，K.Havelund，G.Brat，andS.Park，editors，SPIN Model Checking and Software Verification（7th International SPINWorkshop），Volume 1885 ofLecture Notes in Computer Science，Stanford，CA，USA，August/September 2000. 斯普林格。[8] S. Peyton Jones等，Haskell 98报告。技术报告，http://www.haskell.org/网站，1998年[9] S. Peyton Jones，A.Gordon和S.芬恩并行Haskell。在POPL会议记录中'96：The 23 rd A C M S y m p o s i u m o n Pr i n c i p l e s of P r o g r a m m i n g Language s，page s 295-308，S t. 1996年佛罗里达州彼得斯堡海滩[10] 小艾米·克拉克作者声明：John W. 模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[11] K.Havelund.使用可扩展性分析指导Java程序的模型检查。 In W.Visser，K.Havelund，G.Brat，and S.Park，editors，SPIN Model Checking and Software Verification（7th InternationalSPIN Workshop），Volume 1885 ofLecture Notes in Computer Science，Stanford，CA，USA，August/September 2000. 斯普林格。[12] M.Clavel ， F.J.Duran ， S.Eker ， P.Lincoln ， N.Marti-Oliet ， J.Meseguer ， and J.F. Quesada.Maude系统在Proceedings of the 10th International Conference on Rewriting Techniquesand Applications，RTA斯普林格。[13] 题名/责任者：A. Freja，Hat和Hood：三种跟踪和消除懒惰函数式程序的系统的比较评估。In M.莫宁和P. Koopman，编辑，Proceedings of the 13th International Workshop on Implementation ofFunctional Languages（IFL 2000），卷2011计算机科学讲义，2001。[14] Stolz和F.哈。Concurrent Haskell的验证（正在进行中）。第12届国际泛函与约束逻辑研讨会论文集（WFLP DSIC-II/13/03，联合国 2003年，西班牙巴伦西亚的一个体育[15] W.Visser，K.Havelund，G.Brat，and S.Park.模型检查程序。ASEIEEE CS出版社，2000年9月。