1971:
2525:
2545:
2535:
1409:. The correspondence between the kind of property (safety vs liveness) with kind of proof (invariance vs well-foundedness) was a strong argument that the decomposition of properties into safety and liveness (as opposed to some other partitioning) was a useful one—knowing the type of property to be proved dictated the type of proof that is required.
1086:
above), whereas the weaker property that merely asserts the bound exists is a liveness property. Proving such a liveness property is likely to be easier than proving the tighter safety property because proving the liveness property doesn't require the kind of detailed accounting that is required for proving the safety property.
1670:("for outstanding papers on the principles of distributed computing whose significance and impact on the theory and/or practice of distributed computing have been evident for at least a decade"), for the formal decomposition into safety and liveness properties was crucial to future research into proving properties of programs.
1085:
Most of the time, knowing that a program eventually does some "good thing" is not satisfactory; we want to know that the program performs the "good thing" within some number of steps or before some deadline. A property that gives a specific bound to the "good thing" is a safety property (as noted
264:
Formal definitions that were ultimately proposed for safety properties and liveness properties demonstrated that this decomposition is not only intuitively appealing but is also complete: all properties of an execution are a conjunction of safety and liveness properties. Moreover, undertaking the
938:
314:
An execution of a program can be described formally by giving the infinite sequence of program states that results as execution proceeds, where the last state for a terminating program is repeated infinitely. For a program of interest, let
1271:
1077:
is being proscribed: a partial execution that reaches a state where the answer still has not been produced and the value of the clock (a state variable) violates the bound. Deadlock freedom is a safety property: the "bad thing" is a
823:
1351:. The formal definition of safety given above appears in a paper by Alpern and Schneider; the connection between the two formalizations of safety properties appears in a paper by Alpern, Demers, and Schneider.
1354:
Alpern and
Schneider gives the formal definition for liveness, accompanied by a proof that all properties can be constructed using safety properties and liveness properties. That proof was inspired by
1401:
characterization for the formal definitions of safety properties and liveness properties but used these automata formulations to show that verification of safety properties would require an
265:
decomposition can be helpful, because the formal definitions enable a proof that different methods must be used for verifying safety properties versus for verifying liveness properties.
765:
691:
664:
413:
1143:
1347:. Lamport subsequently developed a formal definition of safety for a NATO short course on distributed systems in Munich. It assumed that properties are invariant under
1730:
1395:
387:
228:
1163:
1004:
961:
738:
633:
586:
517:
473:
433:
1703:
1302:
537:
497:
453:
360:
1186:
1110:
1027:
984:
815:
792:
714:
609:
566:
261:
is discrete, since it happens at a particular place during execution. A "good thing" need not be discrete, but the liveness property of termination is discrete.
1194:
333:
251:
187:
167:
147:
123:
103:
83:
60:
1892:
933:{\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}
1438:
277:
from occurring during an execution. A safety property thus characterizes what is permitted by stating what is prohibited. The requirement that the
296:
An execution that starts in a state satisfying a given precondition terminates, but the final state does not satisfy the required postcondition;
2574:
1073:
Producing an answer within a specified real-time bound is a safety property rather than a liveness property. This is because a discrete
1970:
2147:
1759:
1546:
2246:
1622:
2407:
2261:
1920:
1589:
2569:
2497:
2460:
1979:
1930:
2435:
2354:
1079:
307:
299:
An execution of two concurrent processes, where the program counters for both processes designate statements within a
1885:
2465:
2185:
1165:
would be a "bad thing" and, thus, would be defining a safety property). That leads to defining a liveness property
2548:
2538:
2528:
2056:
1878:
2379:
2177:
2110:
306:
An execution of two concurrent processes where each process is waiting for another to change state (known as
2579:
2339:
2095:
2087:
1402:
2482:
2477:
2280:
1999:
1447:
1348:
2308:
2207:
2105:
2011:
2004:
1406:
743:
669:
642:
392:
1115:
2275:
2270:
2157:
2033:
2021:
1950:
1324:
2190:
1483:
Manna, Zohar; Pnueli, Amir (September 1974). "Axiomatic approach to total correctness of programs".
1452:
1339:
for describing how the assignment of a Petri net's "tokens" to its "places" could evolve; Petri net
1041:
for every execution or, equivalently, describes something that must happen during an execution. The
2287:
2122:
1994:
2256:
2197:
2167:
2152:
2117:
2016:
1960:
1915:
1856:
1708:
1649:
1502:
1465:
1373:
365:
195:
21:
1398:
2371:
1945:
1826:
1776:
1755:
1617:
1584:
1542:
129:
The safety property prohibits these "bad things": executions that start in a state satisfying
36:
17:
1148:
989:
946:
723:
618:
571:
502:
458:
418:
233:
The liveness property, the "good thing", is that execution that starts in a state satisfying
2318:
2217:
2142:
2051:
1901:
1846:
1838:
1796:
1788:
1639:
1631:
1598:
1494:
1485:
1457:
1397:
of infinite sequences of program states. Subsequently, Alpern and
Schneider not only gave a
300:
1681:
1287:
794:
to be a safety property. Formalizing this in predicate logic gives a formal definition for
522:
482:
438:
338:
2422:
2212:
2132:
2041:
1751:
1538:
1266:{\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}
1168:
1092:
1009:
966:
797:
774:
696:
591:
548:
2440:
2399:
2323:
2251:
2231:
2137:
2100:
2066:
1935:
1743:
1667:
1530:
1433:
1355:
1312:
318:
236:
172:
152:
132:
108:
88:
68:
45:
2563:
2127:
2061:
1925:
1792:
1602:
63:
2487:
2470:
2313:
1940:
1860:
1653:
1506:
1469:
125:. Total correctness is a conjunction of a safety property and a liveness property:
40:
1045:
need not be discrete—it might involve an infinite number of steps. Examples of a
2303:
2162:
190:
2389:
2384:
1359:
2450:
2266:
2046:
1748:
Distributed
Systems: Methods and Tools for Specification, An Advanced Course
1535:
Distributed
Systems: Methods and Tools for Specification, An Advanced Course
1461:
1363:
1328:
1059:
Guaranteed eventual entry to a critical section whenever entry is attempted;
476:
943:
This formal definition for safety properties implies that if an execution
285:
occurring during execution necessarily occurs at some identifiable point.
2349:
1367:
2344:
2202:
1842:
1635:
1498:
1851:
1801:
1750:. Lecture Notes in Computer Science. Vol. 190. Munich, Germany:
1644:
1537:. Lecture Notes in Computer Science. Vol. 190. Munich, Germany:
389:
denote the set of infinite sequences of program states. The relation
1056:
Non-termination of an execution that is started in a suitable state;
2412:
1870:
2502:
2492:
1436:(March 1977). "Proving the correctness of multiprocess programs".
16:
Properties of an execution of a computer program—particularly for
2455:
2430:
1053:
Termination of an execution that is started in a suitable state;
1874:
752:
678:
651:
2445:
1188:
to be a property that does not rule out any finite prefix.
1705:
denotes the set of finite sequences of program states and
542:
A property of a program is the set of allowed executions.
362:
denote the set of finite sequences of program states, and
1405:
and verification of liveness properties would require a
1070:
in the first example is discrete but not in the others.
1062:
Fair access to a resource in the presence of contention.
292:
that could be used to define a safety property include:
1746:; Mullery, Geoff P. (3 April 1984). "Basic concepts".
1533:; Mullery, Geoff P. (3 April 1984). "Basic concepts".
1089:
To differ from a safety property, a liveness property
767:. We take this inference about the irremediability of
1711:
1684:
1376:
1290:
1197:
1171:
1151:
1118:
1095:
1012:
992:
969:
949:
826:
800:
777:
746:
726:
699:
672:
645:
621:
594:
574:
551:
525:
505:
485:
461:
441:
421:
395:
368:
341:
321:
239:
198:
175:
155:
149:
and terminate in a final state that does not satisfy
135:
111:
91:
71:
48:
189:, this safety property is usually written using the
2421:
2398:
2370:
2363:
2332:
2296:
2239:
2230:
2176:
2086:
2079:
2032:
1987:
1978:
1908:
1578:
1724:
1697:
1576:
1574:
1572:
1570:
1568:
1566:
1564:
1562:
1560:
1558:
1389:
1296:
1265:
1180:
1157:
1137:
1104:
1021:
998:
978:
955:
932:
809:
786:
759:
732:
708:
685:
658:
627:
603:
580:
560:
545:The essential characteristic of a safety property
531:
511:
491:
467:
447:
427:
407:
381:
354:
327:
245:
222:
181:
161:
141:
117:
97:
77:
54:
615:for that safety property occurs at some point in
1815:Private communication from Plotkin to Schneider.
1732:the set of infinite sequences of program states.
1358:'s insight that safety properties correspond to
1323:in his 1977 paper on proving the correctness of
639:, if further execution results in an execution
1006:(with the last state repeated) also satisfies
85:if any execution started in a state satisfying
1779:(November 1986). "Safety without stuttering".
1886:
1428:
1426:
1424:
1422:
8:
1049:used to define a liveness property include:
217:
211:
205:
199:
1829:(1987). "Recognizing safety and liveness".
1620:(1987). "Recognizing safety and liveness".
335:denote the set of possible program states,
2544:
2534:
2367:
2236:
2083:
1984:
1893:
1879:
1871:
865:
861:
1850:
1800:
1716:
1710:
1689:
1683:
1643:
1451:
1439:IEEE Transactions on Software Engineering
1381:
1375:
1304:, which is an infinite-length execution.
1289:
1236:
1211:
1196:
1170:
1150:
1129:
1117:
1094:
1011:
991:
968:
948:
900:
840:
825:
799:
776:
751:
745:
725:
698:
677:
671:
650:
644:
620:
593:
573:
550:
524:
504:
484:
460:
440:
420:
394:
373:
367:
346:
340:
320:
238:
197:
174:
154:
134:
110:
90:
70:
47:
1418:
1362:and liveness properties correspond to
771:to be the defining characteristic for
273:A safety property proscribes discrete
24:—have long been formulated by giving
7:
1276:This definition does not restrict a
1112:cannot rule out any finite prefix
1325:multiprocess (concurrent) programs
1223:
1198:
887:
869:
827:
14:
760:{\displaystyle \sigma ^{\prime }}
686:{\displaystyle \sigma ^{\prime }}
659:{\displaystyle \sigma ^{\prime }}
408:{\displaystyle \sigma \leq \tau }
105:terminates in a state satisfying
2543:
2533:
2524:
2523:
1969:
1775:Alpern, Bowen; Demers, Alan J.;
1145:of an execution (since such an
1138:{\displaystyle \alpha \in S^{*}}
28:("bad things don't happen") and
1327:. He borrowed the terms from
1037:A liveness property prescribes
1781:Information Processing Letters
1590:Information Processing Letters
1260:
1220:
927:
924:
884:
866:
862:
1:
1587:(1985). "Defining liveness".
1331:, which was using the terms
2575:Theoretical computer science
1793:10.1016/0020-0190(86)90132-8
1603:10.1016/0020-0190(85)90056-0
963:satisfies a safety property
32:("good things do happen").
2247:Curry–Howard correspondence
1725:{\displaystyle S^{\omega }}
1519:i.e. it has finite duration
1390:{\displaystyle S^{\omega }}
635:. Notice that after such a
382:{\displaystyle S^{\omega }}
223:{\displaystyle \{P\}C\{Q\}}
2596:
2519:
1967:
1407:well-foundedness argument
817:being a safety property.
281:be discrete means that a
2096:Abstract interpretation
1666:The paper received the
1462:10.1109/TSE.1977.229904
1343:was a specific form of
1280:to being discrete—the
1158:{\displaystyle \alpha }
999:{\displaystyle \sigma }
956:{\displaystyle \sigma }
733:{\displaystyle \sigma }
628:{\displaystyle \sigma }
581:{\displaystyle \sigma }
568:is: If some execution
512:{\displaystyle \sigma }
468:{\displaystyle \sigma }
428:{\displaystyle \sigma }
288:Examples of a discrete
1726:
1699:
1391:
1298:
1267:
1182:
1159:
1139:
1106:
1023:
1000:
980:
957:
934:
811:
788:
761:
734:
710:
693:also does not satisfy
687:
660:
629:
605:
582:
562:
533:
513:
493:
469:
449:
429:
409:
383:
356:
329:
247:
224:
183:
163:
143:
119:
99:
79:
56:
2005:Categorical semantics
1831:Distributed Computing
1727:
1700:
1698:{\displaystyle S^{*}}
1623:Distributed Computing
1392:
1299:
1297:{\displaystyle \tau }
1268:
1183:
1160:
1140:
1107:
1082:(which is discrete).
1024:
1001:
986:then every prefix of
981:
958:
935:
812:
789:
762:
735:
711:
688:
661:
630:
606:
583:
563:
534:
532:{\displaystyle \tau }
514:
494:
492:{\displaystyle \tau }
470:
450:
448:{\displaystyle \tau }
430:
410:
384:
357:
355:{\displaystyle S^{*}}
330:
248:
225:
184:
164:
144:
120:
100:
80:
57:
2570:Concurrent computing
1951:Runtime verification
1709:
1682:
1374:
1288:
1195:
1169:
1149:
1116:
1093:
1010:
990:
967:
947:
824:
798:
775:
744:
724:
697:
670:
643:
619:
592:
572:
549:
523:
503:
483:
459:
439:
419:
415:holds for sequences
393:
366:
339:
319:
237:
196:
173:
153:
133:
109:
89:
69:
46:
2208:Invariant inference
1956:Safety and liveness
1668:2018 Dijkstra Prize
1284:can involve all of
30:liveness properties
22:distributed systems
2372:Constraint solvers
2198:Concolic execution
2153:Symbolic execution
1961:Undefined behavior
1916:Control-flow graph
1843:10.1007/BF01782772
1827:Schneider, Fred B.
1777:Schneider, Fred B.
1722:
1695:
1636:10.1007/BF01782772
1618:Schneider, Fred B.
1585:Schneider, Fred B.
1499:10.1007/BF00288637
1387:
1294:
1263:
1181:{\displaystyle LP}
1178:
1155:
1135:
1105:{\displaystyle LP}
1102:
1022:{\displaystyle SP}
1019:
996:
979:{\displaystyle SP}
976:
953:
930:
810:{\displaystyle SP}
807:
787:{\displaystyle SP}
784:
757:
730:
709:{\displaystyle SP}
706:
683:
656:
625:
611:then the defining
604:{\displaystyle SP}
601:
578:
561:{\displaystyle SP}
558:
529:
509:
489:
465:
445:
425:
405:
379:
352:
325:
243:
220:
179:
159:
139:
115:
95:
75:
52:
39:with respect to a
2557:
2556:
2515:
2514:
2511:
2510:
2226:
2225:
2075:
2074:
1754:. pp. 7–43.
1742:Alford, Mack W.;
1541:. pp. 7–43.
1529:Alford, Mack W.;
1321:liveness property
588:does not satisfy
328:{\displaystyle S}
246:{\displaystyle P}
182:{\displaystyle C}
162:{\displaystyle Q}
142:{\displaystyle P}
118:{\displaystyle Q}
98:{\displaystyle P}
78:{\displaystyle Q}
55:{\displaystyle P}
26:safety properties
2587:
2547:
2546:
2537:
2536:
2527:
2526:
2423:Proof assistants
2368:
2237:
2084:
2057:Rewriting system
2052:Process calculus
1985:
1973:
1902:Program analysis
1895:
1888:
1881:
1872:
1865:
1864:
1854:
1822:
1816:
1813:
1807:
1806:
1804:
1772:
1766:
1765:
1739:
1733:
1731:
1729:
1728:
1723:
1721:
1720:
1704:
1702:
1701:
1696:
1694:
1693:
1677:
1671:
1664:
1658:
1657:
1647:
1613:
1607:
1606:
1580:
1553:
1552:
1526:
1520:
1517:
1511:
1510:
1486:Acta Informatica
1480:
1474:
1473:
1455:
1430:
1396:
1394:
1393:
1388:
1386:
1385:
1329:Petri net theory
1303:
1301:
1300:
1295:
1272:
1270:
1269:
1264:
1241:
1240:
1216:
1215:
1187:
1185:
1184:
1179:
1164:
1162:
1161:
1156:
1144:
1142:
1141:
1136:
1134:
1133:
1111:
1109:
1108:
1103:
1028:
1026:
1025:
1020:
1005:
1003:
1002:
997:
985:
983:
982:
977:
962:
960:
959:
954:
939:
937:
936:
931:
905:
904:
845:
844:
816:
814:
813:
808:
793:
791:
790:
785:
766:
764:
763:
758:
756:
755:
739:
737:
736:
731:
715:
713:
712:
707:
692:
690:
689:
684:
682:
681:
665:
663:
662:
657:
655:
654:
634:
632:
631:
626:
610:
608:
607:
602:
587:
585:
584:
579:
567:
565:
564:
559:
538:
536:
535:
530:
518:
516:
515:
510:
498:
496:
495:
490:
474:
472:
471:
466:
454:
452:
451:
446:
434:
432:
431:
426:
414:
412:
411:
406:
388:
386:
385:
380:
378:
377:
361:
359:
358:
353:
351:
350:
334:
332:
331:
326:
301:critical section
252:
250:
249:
244:
229:
227:
226:
221:
188:
186:
185:
180:
169:. For a program
168:
166:
165:
160:
148:
146:
145:
140:
124:
122:
121:
116:
104:
102:
101:
96:
84:
82:
81:
76:
61:
59:
58:
53:
2595:
2594:
2590:
2589:
2588:
2586:
2585:
2584:
2560:
2559:
2558:
2553:
2507:
2417:
2394:
2359:
2333:Data structures
2328:
2292:
2222:
2213:Program slicing
2172:
2071:
2042:Lambda calculus
2028:
1974:
1965:
1926:Hyperproperties
1904:
1899:
1869:
1868:
1825:Alpern, Bowen;
1824:
1823:
1819:
1814:
1810:
1774:
1773:
1769:
1762:
1752:Springer Verlag
1744:Lamport, Leslie
1741:
1740:
1736:
1712:
1707:
1706:
1685:
1680:
1679:
1678:
1674:
1665:
1661:
1616:Alpern, Bowen;
1615:
1614:
1610:
1583:Alpern, Bowen;
1582:
1581:
1556:
1549:
1539:Springer Verlag
1531:Lamport, Leslie
1528:
1527:
1523:
1518:
1514:
1482:
1481:
1477:
1453:10.1.1.137.9454
1434:Lamport, Leslie
1432:
1431:
1420:
1415:
1399:BĂĽchi automaton
1377:
1372:
1371:
1317:safety property
1315:used the terms
1310:
1286:
1285:
1232:
1207:
1193:
1192:
1167:
1166:
1147:
1146:
1125:
1114:
1113:
1091:
1090:
1035:
1008:
1007:
988:
987:
965:
964:
945:
944:
896:
836:
822:
821:
796:
795:
773:
772:
747:
742:
741:
740:also occurs in
722:
721:
695:
694:
673:
668:
667:
646:
641:
640:
617:
616:
590:
589:
570:
569:
547:
546:
521:
520:
501:
500:
481:
480:
457:
456:
437:
436:
417:
416:
391:
390:
369:
364:
363:
342:
337:
336:
317:
316:
271:
235:
234:
194:
193:
171:
170:
151:
150:
131:
130:
107:
106:
87:
86:
67:
66:
44:
43:
37:totally correct
12:
11:
5:
2593:
2591:
2583:
2582:
2580:Model checking
2577:
2572:
2562:
2561:
2555:
2554:
2552:
2551:
2541:
2531:
2520:
2517:
2516:
2513:
2512:
2509:
2508:
2506:
2505:
2500:
2495:
2490:
2485:
2480:
2475:
2474:
2473:
2463:
2458:
2453:
2448:
2443:
2438:
2433:
2427:
2425:
2419:
2418:
2416:
2415:
2410:
2404:
2402:
2396:
2395:
2393:
2392:
2387:
2382:
2376:
2374:
2365:
2361:
2360:
2358:
2357:
2352:
2347:
2342:
2336:
2334:
2330:
2329:
2327:
2326:
2321:
2316:
2311:
2306:
2300:
2298:
2294:
2293:
2291:
2290:
2285:
2284:
2283:
2273:
2264:
2259:
2254:
2252:Loop invariant
2249:
2243:
2241:
2234:
2232:Formal methods
2228:
2227:
2224:
2223:
2221:
2220:
2215:
2210:
2205:
2200:
2195:
2194:
2193:
2191:Taint tracking
2182:
2180:
2174:
2173:
2171:
2170:
2165:
2160:
2155:
2150:
2145:
2140:
2138:Model checking
2135:
2130:
2125:
2120:
2115:
2114:
2113:
2103:
2098:
2092:
2090:
2081:
2077:
2076:
2073:
2072:
2070:
2069:
2067:Turing machine
2064:
2059:
2054:
2049:
2044:
2038:
2036:
2030:
2029:
2027:
2026:
2025:
2024:
2019:
2009:
2008:
2007:
1997:
1991:
1989:
1982:
1976:
1975:
1968:
1966:
1964:
1963:
1958:
1953:
1948:
1946:Rice's theorem
1943:
1938:
1936:Path explosion
1933:
1928:
1923:
1918:
1912:
1910:
1906:
1905:
1900:
1898:
1897:
1890:
1883:
1875:
1867:
1866:
1837:(3): 117–126.
1817:
1808:
1787:(4): 177–180.
1767:
1760:
1734:
1719:
1715:
1692:
1688:
1672:
1659:
1630:(3): 117–126.
1608:
1597:(4): 181–185.
1554:
1547:
1521:
1512:
1493:(3): 243–263.
1475:
1446:(2): 125–143.
1417:
1416:
1414:
1411:
1384:
1380:
1356:Gordon Plotkin
1309:
1306:
1293:
1274:
1273:
1262:
1259:
1256:
1253:
1250:
1247:
1244:
1239:
1235:
1231:
1228:
1225:
1222:
1219:
1214:
1210:
1206:
1203:
1200:
1177:
1174:
1154:
1132:
1128:
1124:
1121:
1101:
1098:
1064:
1063:
1060:
1057:
1054:
1034:
1031:
1018:
1015:
995:
975:
972:
952:
941:
940:
929:
926:
923:
920:
917:
914:
911:
908:
903:
899:
895:
892:
889:
886:
883:
880:
877:
874:
871:
868:
864:
860:
857:
854:
851:
848:
843:
839:
835:
832:
829:
806:
803:
783:
780:
754:
750:
729:
705:
702:
680:
676:
653:
649:
624:
600:
597:
577:
557:
554:
528:
508:
488:
464:
444:
424:
404:
401:
398:
376:
372:
349:
345:
324:
312:
311:
304:
297:
270:
267:
255:
254:
242:
231:
219:
216:
213:
210:
207:
204:
201:
178:
158:
138:
114:
94:
74:
51:
13:
10:
9:
6:
4:
3:
2:
2592:
2581:
2578:
2576:
2573:
2571:
2568:
2567:
2565:
2550:
2542:
2540:
2532:
2530:
2522:
2521:
2518:
2504:
2501:
2499:
2496:
2494:
2491:
2489:
2486:
2484:
2481:
2479:
2476:
2472:
2469:
2468:
2467:
2464:
2462:
2459:
2457:
2454:
2452:
2449:
2447:
2444:
2442:
2439:
2437:
2434:
2432:
2429:
2428:
2426:
2424:
2420:
2414:
2411:
2409:
2406:
2405:
2403:
2401:
2397:
2391:
2388:
2386:
2383:
2381:
2378:
2377:
2375:
2373:
2369:
2366:
2362:
2356:
2353:
2351:
2348:
2346:
2343:
2341:
2338:
2337:
2335:
2331:
2325:
2322:
2320:
2317:
2315:
2312:
2310:
2309:Incorrectness
2307:
2305:
2302:
2301:
2299:
2295:
2289:
2286:
2282:
2279:
2278:
2277:
2276:Specification
2274:
2272:
2268:
2265:
2263:
2260:
2258:
2255:
2253:
2250:
2248:
2245:
2244:
2242:
2238:
2235:
2233:
2229:
2219:
2216:
2214:
2211:
2209:
2206:
2204:
2201:
2199:
2196:
2192:
2189:
2188:
2187:
2184:
2183:
2181:
2179:
2175:
2169:
2166:
2164:
2161:
2159:
2156:
2154:
2151:
2149:
2146:
2144:
2141:
2139:
2136:
2134:
2131:
2129:
2128:Effect system
2126:
2124:
2121:
2119:
2116:
2112:
2109:
2108:
2107:
2104:
2102:
2099:
2097:
2094:
2093:
2091:
2089:
2085:
2082:
2078:
2068:
2065:
2063:
2062:State machine
2060:
2058:
2055:
2053:
2050:
2048:
2045:
2043:
2040:
2039:
2037:
2035:
2031:
2023:
2020:
2018:
2015:
2014:
2013:
2010:
2006:
2003:
2002:
2001:
1998:
1996:
1993:
1992:
1990:
1986:
1983:
1981:
1977:
1972:
1962:
1959:
1957:
1954:
1952:
1949:
1947:
1944:
1942:
1939:
1937:
1934:
1932:
1929:
1927:
1924:
1922:
1919:
1917:
1914:
1913:
1911:
1907:
1903:
1896:
1891:
1889:
1884:
1882:
1877:
1876:
1873:
1862:
1858:
1853:
1848:
1844:
1840:
1836:
1832:
1828:
1821:
1818:
1812:
1809:
1803:
1798:
1794:
1790:
1786:
1782:
1778:
1771:
1768:
1763:
1761:3-540-15216-4
1757:
1753:
1749:
1745:
1738:
1735:
1717:
1713:
1690:
1686:
1676:
1673:
1669:
1663:
1660:
1655:
1651:
1646:
1641:
1637:
1633:
1629:
1625:
1624:
1619:
1612:
1609:
1604:
1600:
1596:
1592:
1591:
1586:
1579:
1577:
1575:
1573:
1571:
1569:
1567:
1565:
1563:
1561:
1559:
1555:
1550:
1548:3-540-15216-4
1544:
1540:
1536:
1532:
1525:
1522:
1516:
1513:
1508:
1504:
1500:
1496:
1492:
1488:
1487:
1479:
1476:
1471:
1467:
1463:
1459:
1454:
1449:
1445:
1441:
1440:
1435:
1429:
1427:
1425:
1423:
1419:
1412:
1410:
1408:
1404:
1400:
1382:
1378:
1369:
1366:in a natural
1365:
1361:
1357:
1352:
1350:
1346:
1342:
1338:
1334:
1330:
1326:
1322:
1318:
1314:
1307:
1305:
1291:
1283:
1279:
1257:
1254:
1251:
1248:
1245:
1242:
1237:
1233:
1229:
1226:
1217:
1212:
1208:
1204:
1201:
1191:
1190:
1189:
1175:
1172:
1152:
1130:
1126:
1122:
1119:
1099:
1096:
1087:
1083:
1081:
1076:
1071:
1069:
1061:
1058:
1055:
1052:
1051:
1050:
1048:
1044:
1040:
1032:
1030:
1016:
1013:
993:
973:
970:
950:
921:
918:
915:
912:
909:
906:
901:
897:
893:
890:
881:
878:
875:
872:
858:
855:
852:
849:
846:
841:
837:
833:
830:
820:
819:
818:
804:
801:
781:
778:
770:
748:
727:
719:
703:
700:
674:
647:
638:
622:
614:
598:
595:
575:
555:
552:
543:
540:
526:
506:
486:
478:
462:
442:
422:
402:
399:
396:
374:
370:
347:
343:
322:
309:
305:
302:
298:
295:
294:
293:
291:
286:
284:
280:
276:
268:
266:
262:
260:
240:
232:
214:
208:
202:
192:
176:
156:
136:
128:
127:
126:
112:
92:
72:
65:
64:postcondition
49:
42:
38:
35:A program is
33:
31:
27:
23:
19:
2471:Isabelle/HOL
2288:Verification
2271:completeness
2163:Type systems
2106:Control flow
2000:Denotational
1955:
1941:Polyvariance
1909:Key concepts
1834:
1830:
1820:
1811:
1784:
1780:
1770:
1747:
1737:
1675:
1662:
1627:
1621:
1611:
1594:
1588:
1534:
1524:
1515:
1490:
1484:
1478:
1443:
1437:
1353:
1344:
1340:
1336:
1332:
1320:
1316:
1311:
1281:
1277:
1275:
1088:
1084:
1074:
1072:
1067:
1065:
1046:
1042:
1038:
1036:
942:
768:
717:
716:, since the
636:
612:
544:
541:
313:
289:
287:
282:
278:
274:
272:
263:
258:
257:Note that a
256:
191:Hoare triple
41:precondition
34:
29:
25:
15:
2400:Lightweight
2262:Side effect
2158:Termination
2012:Operational
1921:Correctness
1370:on the set
1360:closed sets
1345:boundedness
1337:boundedness
1039:good things
253:terminates.
2564:Categories
2355:Union-find
2319:Separation
2257:Refinement
2123:Dependence
2022:Small-step
1931:Invariants
1413:References
1364:dense sets
1349:stuttering
1282:good thing
1278:good thing
1068:good thing
1047:good thing
1043:good thing
769:bad things
275:bad things
18:concurrent
2451:HOL Light
2281:Languages
2267:Soundness
2186:Data-flow
2168:Typestate
2118:Data-flow
2047:Petri net
1995:Axiomatic
1980:Semantics
1852:1813/6567
1802:1813/6548
1718:ω
1691:∗
1645:1813/6567
1448:CiteSeerX
1403:invariant
1383:ω
1292:τ
1252:∈
1249:τ
1246:α
1238:ω
1230:∈
1227:τ
1224:∃
1213:∗
1205:∈
1202:α
1199:∀
1153:α
1131:∗
1123:∈
1120:α
1075:bad thing
994:σ
951:σ
916:∉
913:τ
910:β
902:ω
894:∈
891:τ
888:∀
879:σ
876:≤
873:β
870:∃
863:⟹
853:∉
850:σ
842:ω
834:∈
831:σ
828:∀
753:′
749:σ
728:σ
718:bad thing
679:′
675:σ
652:′
648:σ
637:bad thing
623:σ
613:bad thing
576:σ
527:τ
507:σ
487:τ
463:σ
443:τ
423:σ
403:τ
400:≤
397:σ
375:ω
348:∗
290:bad thing
283:bad thing
279:bad thing
259:bad thing
2549:Glossary
2529:Category
2466:Isabelle
2350:Hashcons
2324:Temporal
2240:Concepts
2080:Analyses
2017:Big-step
1368:topology
1333:liveness
1080:deadlock
1033:Liveness
308:deadlock
2539:Outline
2345:E-graph
2218:Testing
2203:Fuzzing
2178:Dynamic
2143:Pointer
1861:9717112
1654:9717112
1507:2988073
1470:9985552
1313:Lamport
1308:History
666:, then
519:equals
2314:Linear
2297:Logics
2133:Escape
2088:Static
2034:Models
1859:
1758:
1652:
1545:
1505:
1468:
1450:
1341:safety
477:prefix
269:Safety
2503:Twelf
2493:NuPRL
2488:Mizar
2461:Idris
2408:Alloy
2364:Tools
2304:Hoare
2148:Shape
2101:Alias
1988:Types
1857:S2CID
1650:S2CID
1503:S2CID
1466:S2CID
475:is a
2483:LEGO
2478:Lean
2456:HOL4
2436:Agda
2431:ACL2
2413:TLA+
2269:and
2111:kCFA
1756:ISBN
1543:ISBN
1444:SE-3
1335:and
1319:and
1066:The
455:iff
435:and
62:and
20:and
2498:PVS
2441:Coq
2390:SMT
2385:SAT
2380:CHC
2340:BDD
1847:hdl
1839:doi
1797:hdl
1789:doi
1640:hdl
1632:doi
1599:doi
1495:doi
1458:doi
720:in
499:or
479:of
2566::
2446:F*
1855:.
1845:.
1833:.
1795:.
1785:23
1783:.
1648:.
1638:.
1626:.
1595:21
1593:.
1557:^
1501:.
1489:.
1464:.
1456:.
1442:.
1421:^
1029:.
539:.
310:).
1894:e
1887:t
1880:v
1863:.
1849::
1841::
1835:2
1805:.
1799::
1791::
1764:.
1714:S
1687:S
1656:.
1642::
1634::
1628:2
1605:.
1601::
1551:.
1509:.
1497::
1491:3
1472:.
1460::
1379:S
1261:)
1258:P
1255:L
1243::
1234:S
1221:(
1218::
1209:S
1176:P
1173:L
1127:S
1100:P
1097:L
1017:P
1014:S
974:P
971:S
928:)
925:)
922:P
919:S
907::
898:S
885:(
882::
867:(
859:P
856:S
847::
838:S
805:P
802:S
782:P
779:S
704:P
701:S
599:P
596:S
556:P
553:S
371:S
344:S
323:S
303:;
241:P
230:.
218:}
215:Q
212:{
209:C
206:}
203:P
200:{
177:C
157:Q
137:P
113:Q
93:P
73:Q
50:P
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.