220:
extensively modified and extended by David Dill, Alan Hu, C. Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang. Ralph Melton implemented the new version during the summer and fall of 1992. Seungjoon Park added liveness checking and fairness constraints, but because the algorithm for liveness verification conflicted with important optimizations, particularly symmetry reduction, liveness verification was omitted in subsequent releases. C. Norris Ip implemented reversible rules and repetition constructors (which are not included in release 3.1), and added symmetry and multiset reductions (which are). Ulrich Stern implemented hash compaction, improved the use of disk, and implemented
Parallel Murφ.
22:
219:
Murφ's early history is described in a paper by David Dill. The first version of Murφ was designed at
Stanford University in 1990 and 1991 by Prof. David Dill and his graduate students Andreas Drexler, Alan Hu, and Han Yang, and primarily implemented by Andreas Drexler. The specification language was
240:
uses guarded commands and an asynchronous, interleaving model of concurrency, with all synchronization and communication done through global variables. The verifier checks safety properties in the form of invariants and internal assertions that are specified in the model, and checks for deadlock. It
260:
The Murφ license is similar to the MIT license. Murφ may be used, copied, modified, sold, and redistributed for any purpose, provided the copyright notice and license are included, the name of
Stanford University is not used for advertising or publicity without permission, and modified versions are
235:
The Murφ compiler accepts a model written in the Murφ specification language and outputs C++ code that constitutes a verifier for that model. (That is, the C++ code, when executed, performs explicit-state model checking on the design described by the specification.) The
241:
does not check liveness properties, though Murφ release 2.7L did support verification of a set of common LTL liveness properties. The language and verifier support some kinds of symmetry reductions.
322:
Universal
Planner Murphi — Planning and universal planning for linear and nonlinear continuous PDDL+ models with processes and events; also timed initial literals and timed initial fluents.
485:
211:) is an explicit-state model checker developed at Stanford University, and widely used for formal verification of cache-coherence protocols.
413:
70:
44:
437:
Dill, David L.; Drexler, Andreas J.; Hu, Alan J.; Yang, C. Han (1992). "Protocol verification as a hardware design aid".
196:
343:
129:
103:
52:
48:
32:
363:
480:
439:
Proceedings of the 1992 IEEE International
Conference on Computer Design: VLSI in Computers & Processors
311:
171:
419:
306:
455:
396:
Ip, C. Norris; Dill, David L. (1993). "Efficient verification of symmetric concurrent systems".
269:
Many derivative versions of Murφ have been created, at
Stanford and elsewhere, including these:
237:
409:
401:
183:
159:
245:
317:
Eddy Murphi — Parallel and distributed, based on CMurphi, using MPI for message passing.
338:
176:
474:
423:
316:
276:
94:
David Dill's research group at the
Stanford University Computer Systems Laboratory
465:
301:
296:
291:
286:
282:
PReach (Parallel
Reachability) — Parallel model checking implemented in Erlang.
152:
281:
89:
405:
460:
398:
Proceedings of 1993 IEEE International
Conference on Computer Design ICCD'93
249:
466:
University of Utah, School of
Computing — a collection of versions of Murφ.
135:
321:
223:
The last release from Stanford was release 3.1 in November of 1993. Many
248:
protocols, but has been applied to other problems as well, including
197:
http://verify.stanford.edu/dill/murphi.html (via the Wayback Machine)
461:
Stanford Security Lab, Model Checking Methods for Security Protocols
51:
external links, and converting useful links where appropriate into
326:
164:
368:
25 Years of Model Checking: History, Achievements, Perspectives
15:
40:
192:
182:
170:
158:
148:
128:
102:
88:
312:FHP-Murphi — Finite Horizon Probabilistic Murphi.
35:may not follow Knowledge's policies or guidelines
456:Murphi Annotated Reference Manual, Release 3.1
366:(2008). Grumberg, Orna; Veith, Helmut (eds.).
227:have been created since then by other groups.
8:
83:
82:
385:. Boston, MA: Springer. pp. 333–348.
244:Murφ was originally applied to verifying
71:Learn how and when to remove this message
355:
381:Stern, Ulrich; Dill, David L. (1996).
261:not called Murphi without permission.
277:Eddy — Parallel and distributed Murφ.
7:
302:POeM — Partial-Order Enabled Murphi
297:PAM — Predicate Abstraction Murphi
250:verification of security protocols
14:
383:Formal Description Techniques IX
224:
20:
486:Free software programmed in C++
1:
344:list of model checking tools
292:Parallel Random-Walk Murphi
238:Murφ specification language
225:derivative versions of Murφ
111:; 30 years ago
109:3.1 / November 1993
502:
400:. IEEE. pp. 230–234.
188:similar to the MIT license
307:CMurphi — Caching Murphi.
124:
98:
406:10.1109/ICCD.1993.393375
207:(/ˈmɝ.fi/, also spelled
41:improve this article
85:
53:footnote references
287:Distributed Murphi
370:. pp. 77–88.
202:
201:
81:
80:
73:
493:
443:
442:
441:. IEEE: 552–525.
434:
428:
427:
393:
387:
386:
378:
372:
371:
360:
160:Operating system
144:
141:
139:
137:
119:
117:
112:
86:
76:
69:
65:
62:
56:
24:
23:
16:
501:
500:
496:
495:
494:
492:
491:
490:
471:
470:
452:
447:
446:
436:
435:
431:
416:
395:
394:
390:
380:
379:
375:
362:
361:
357:
352:
335:
267:
258:
246:cache-coherence
233:
217:
134:
120:
115:
113:
110:
77:
66:
60:
57:
38:
29:This article's
25:
21:
12:
11:
5:
499:
497:
489:
488:
483:
481:Model checking
473:
472:
469:
468:
463:
458:
451:
450:External links
448:
445:
444:
429:
414:
388:
373:
364:Dill, David L.
354:
353:
351:
348:
347:
346:
341:
339:Model checking
334:
331:
330:
329:
324:
319:
314:
309:
304:
299:
294:
289:
284:
279:
274:
266:
263:
257:
254:
232:
229:
216:
213:
200:
199:
194:
190:
189:
186:
180:
179:
177:Model Checking
174:
168:
167:
162:
156:
155:
150:
146:
145:
132:
126:
125:
122:
121:
108:
106:
104:Stable release
100:
99:
96:
95:
92:
79:
78:
33:external links
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
498:
487:
484:
482:
479:
478:
476:
467:
464:
462:
459:
457:
454:
453:
449:
440:
433:
430:
425:
421:
417:
415:0-8186-4230-0
411:
407:
403:
399:
392:
389:
384:
377:
374:
369:
365:
359:
356:
349:
345:
342:
340:
337:
336:
332:
328:
325:
323:
320:
318:
315:
313:
310:
308:
305:
303:
300:
298:
295:
293:
290:
288:
285:
283:
280:
278:
275:
273:Parallel Murφ
272:
271:
270:
264:
262:
255:
253:
251:
247:
242:
239:
230:
228:
226:
221:
214:
212:
210:
206:
198:
195:
191:
187:
185:
181:
178:
175:
173:
169:
166:
163:
161:
157:
154:
151:
147:
143:
133:
131:
127:
123:
107:
105:
101:
97:
93:
91:
87:
75:
72:
64:
61:December 2021
54:
50:
49:inappropriate
46:
42:
36:
34:
27:
18:
17:
438:
432:
397:
391:
382:
376:
367:
358:
268:
259:
243:
234:
222:
218:
208:
204:
203:
90:Developer(s)
67:
58:
43:by removing
30:
265:Derivatives
142:/Murphi2019
140:/tyler-utah
475:Categories
350:References
149:Written in
130:Repository
256:Licensing
45:excessive
424:38444364
333:See also
231:Features
153:ANSI C++
215:History
193:Website
184:License
116:1993-11
114: (
39:Please
31:use of
422:
412:
209:Murphi
136:github
420:S2CID
327:rumur
165:Linux
410:ISBN
205:Murφ
172:Type
138:.com
84:Murφ
402:doi
47:or
477::
418:.
408:.
252:.
426:.
404::
118:)
74:)
68:(
63:)
59:(
55:.
37:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.