–吃
发表于 2025-3-23 12:34:34
PAM: A process algebra manipulator, by directly manipulating process terms. The logic that PAM implements is equational logic plus recursion, with some features tailored to the particular requirements of process algebras. Equational reasoning is implemented by rewriting, while recursion is dealt with by induction. Proofs are construc
incite
发表于 2025-3-23 17:39:09
A proof assistant for PSF, on state space exploration, we use an axiomatic approach. The axioms we use for the construction of proofs, are based on ACP. Besides these standard axioms we also consider tactics for shortening proofs. We use PSF (Process Specification Formalism), an extension of ACP with abstract data types, to
Inclement
发表于 2025-3-23 20:47:02
http://reply.papertrans.cn/24/2334/233351/233351_13.png
Guileless
发表于 2025-3-24 00:35:53
Lecture Notes in Computer Sciencehttp://image.papertrans.cn/c/image/233351.jpg
hair-bulb
发表于 2025-3-24 03:57:51
Computer Aided Verification978-3-540-46763-2Series ISSN 0302-9743 Series E-ISSN 1611-3349
left-ventricle
发表于 2025-3-24 08:36:36
Denis Cavallucci,Stelian Brad,Pavel Livotovyer-Moore theorem prover to prove the correctness of an implementation. The kernel specification had first been given in terms of a labeled transition system. It was transcribed into the Boyer-Moore logic so that an attempt could be made to mechanically check correctness proofs.
柔美流畅
发表于 2025-3-24 12:54:57
http://reply.papertrans.cn/24/2334/233351/233351_17.png
caldron
发表于 2025-3-24 18:14:48
Mechanically checked proofs of kernel specifications,yer-Moore theorem prover to prove the correctness of an implementation. The kernel specification had first been given in terms of a labeled transition system. It was transcribed into the Boyer-Moore logic so that an attempt could be made to mechanically check correctness proofs.
Expostulate
发表于 2025-3-24 20:54:10
Avoiding state explosion by composition of minimal covering graphs,cation of Petri nets properties from the point of view of reusability of partial results already obtained. We give two algorithms which allow to compute the minimal covering graph of a Petri net by composing the minimal covering graphs of each of its modules.
故意钓到白杨
发表于 2025-3-25 00:56:03
Procure Software Delivery EnvironmentWe present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we beleive, offers a very general verification method applicable to a wide range of computational systems.