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