4372:
3072:
found that the proof rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding the rely-guarantee technique which had been originally proposed to reason about interference; in this work the elements of the model were considered not resources, but rather "views" of the program state, and a non-standard interpretation of Hoare triples accompanies the non-standard reading of pre and postconditions. Finally, CSL-style principles have been used to compose reasoning about program histories instead of program states, in order to provide modular techniques for reasoning about fine-grained concurrent algorithms.
4926:
4946:
4936:
3293:
The distinction between interactive and in-between verifiers is not a sharp one. For example, Bedrock strives for a high degree of automation, in what it terms mostly-automatic verification, where
Verifast sometimes requires annotations that resemble the tactics (little programs) used in interactive
3075:
Versions of CSL have been included in many interactive and semi-automatic (or "in-between") verification tools as described in the next section. A particularly significant verification effort is that of the μC/OS-II kernel mentioned there. But, although steps have been made, as of yet CSL-style
2334:
Separation logic leads to simple proofs of pointer manipulation for data structures that exhibit regular sharing patterns which can be described simply using separating conjunctions; examples include singly and doubly linked lists and varieties of trees. Graphs and DAGs and other data structures with
3071:
An abstract version of separation logic was proposed that works for Hoare triples where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model. Later, by suitable choice of commutative monoid, it was surprisingly
3063:
A model for concurrent separation logic was first provided by
Stephen Brookes in a companion paper to O'Hearn's. The soundness of the logic had been a difficult problem, and in fact a counterexample of John Reynolds had shown the unsoundness of an earlier, unpublished version of the logic; the issue
4202:
Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "cvc5: A Versatile and
Industrial-Strength SMT
3211:
Many tools require more user intervention than program analyses, in that they expect the user to input assertions such as pre/post specs for functions or loop invariants, but after this input is given they attempt to be fully or almost fully automatic; this mode of verification goes back to classic
3067:
At first it appeared that CSL was well suited to what
Dijkstra had called loosely connected processes, but perhaps not to fine-grained concurrent algorithms with significant interference. However, gradually it was realized that the basic approach of CSL was considerably more powerful than first
3251:
is a state-of-the-art automated verification infrastructure for permission-based reasoning. It mainly consists of a programming language and two verification backends, one based on symbolic execution and another one on verification condition generation (VCG). Based on the Viper infrastructure,
3040:
to reasoning about concurrency, replacing the use of scoping constraints to ensure separation by reasoning in separation logic. In addition to extending Hoare's approach to apply in the presence of heap-allocated pointers, O'Hearn showed how reasoning in concurrent separation logic could track
3091:
Tools for reasoning about programs fall on a spectrum from fully automatic program analysis tools, which do not require any user input, to interactive tools where the human is intimately involved in the proof process. Many such tools have been developed; the following list includes a few
3223:, was in this in-between category. It required the user to input pre/post specs, loop invariants, and resource invariants for locks. It introduced a method of symbolic execution, as well as an automatic way to infer frame axioms. Smallfoot included Concurrent Separation Logic.
3031:
2161:
3322:
for separation logic with uninterpreted memory locations can also be shown to be PSPACE-complete, whereas the problem is undecidable with interpreted memory locations (e.g., integers) or further quantifier alternations
2470:
1645:
3148:
A proof of the FSCQ file system where the specification includes behaviour under crashes as well as normal operation. This work won the best paper award at the 2015 Symposium on
Operating System Principles.
762:
1707:
2845:
1757:
714:
542:
89:, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated
2022:
2522:
3268:
for C, Java, OpenCL, and OpenMP. These frontends translate the frontend programming language into Viper to then use a Viper verification backend for proving the input program's correctness.
2335:
more general sharing are more difficult for both formal and informal proof. Separation logic has, nonetheless, been applied successfully to reasoning about programs with general sharing.
3060:, O'Hearn says that explicit checking for non-interference isn't necessary because his system rules out interference in an implicit way, by the nature of the way proofs are constructed.
848:
1390:
1503:
4286:
3501:
3245:
is an advanced current tool in the in-between category. It has demonstrated proofs ranging from object-oriented patterns to highly concurrent algorithms and to systems programs.
3110:
based on separation logic and bi-abduction. As of 2015 hundreds of bugs per month were being found by Infer and fixed by developers before being shipped to
Facebook's mobile apps
1186:
2821:
2613:
2579:
1460:
1104:
930:
1790:
1423:
1232:
268:
4949:
1310:
1271:
633:
573:
2787:
1904:
1848:
4939:
2304:
351:
386:
1144:
1552:
1338:
3216:, a term which intends to evoke the way of interacting with a verifier via an assert-check loop, analogous to the interaction between a programmer and a type-checker.
2550:
2519:
2363:
1816:
805:
317:
3099:
These tools typically look for restricted classes of bugs (e.g., memory safety errors) or attempt to prove their absence, but fall short of proving full correctness.
2217:
971:
678:
599:
231:
4511:
2727:
2700:
1527:
1054:
288:
3302:
The satisfiability problem for a quantifier-free, multi-sorted fragment of separation logic parameterized over the sorts of locations and data can be shown to be
2494:, and this works for any postcondition, not only one that is laid out neatly using the separating conjunction. This idea was taken much further by Yang, who used
2747:
2673:
2653:
2633:
2492:
2324:
2277:
2257:
2237:
2191:
2008:
1988:
1968:
1944:
1924:
1031:
1011:
991:
782:
653:
510:
490:
470:
446:
426:
406:
206:
182:
158:
4709:
4608:
3145:. In comparison to the program analysis work, these tools require more in the way of human effort but prove deeper properties, up to functional correctness.
1348:) asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I.e,.
3279:
include ideas related to CSL in the type system for a programming language. The idea to include separation in a type system has earlier examples in
4591:
4071:
2370:
1571:
807:
takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I.e.,
3076:
reasoning has been included in comparatively few tools in the automatic program analysis category (and none mentioned in the next section).
4293:
723:
3041:
dynamic ownership transfer of heap portions between processes; examples in the paper include a pointer-transferring buffer, and a
3036:
which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach of
3026:{\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}
2581:
which has variously been called overlapping conjunction or sepish, and which can be used to describe overlapping data structures:
3212:
works in the 1970s such as J King's verifier, and the
Stanford Pascal Verifier. This style of verifier has recently been called
3184:
2239:
will remain true in the postcondition). The side condition enforces this by specifying that none of the variables modified by
4259:
4222:
4186:
3999:
3879:
1712:
1657:
3382:
Millennial
Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare
4035:
3978:
2156:{\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }
687:
515:
3411:
4985:
3471:
O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local
Reasoning about Programs that Alter Data Structures".
2835:
A Concurrent
Separation Logic (CSL), a version of separation logic for concurrent programs, was originally proposed by
4548:
3705:
3319:
4647:
3369:
3670:
3622:
Proceedings of the 1st Workshop on Semantics' Program Analysis' and Computing Environments for Memory Management
1990:
may access only memory locations whose existence is asserted in the precondition or that have been allocated by
4808:
4662:
4356:
4321:
3427:
3236:
3229:
is a verifier for a marriage of separation logic and the classic rely/guarantee method for concurrent programs.
1351:
4898:
4371:
3826:
3682:
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '12
2525:. Finally, one of the most recent works in this direction is that of Hobor and Villard, who employ not only
118:
41:
3114:
1950:(e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition
810:
4980:
4861:
4380:
4331:
1651:
4800:
4970:
4836:
4755:
3152:
3137:
Proofs have been done using embeddings of Separation Logic into interactive theorem provers such as the
1465:
1149:
137:
3832:
3064:
raised by Reynolds's example is described briefly in O'Hearn's paper, and more thoroughly in Brookes's.
2792:
2584:
2555:
2173:) and enables local reasoning. It says that a program that executes safely in a small state (satisfying
1071:
853:
4866:
4586:
3522:
3176:
Verification of key modules of a commercial OS kernel, the μC/OS-II kernel, the first commercial
1191:
3903:
Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013).
3068:
envisaged, if one employed non-standard models of the logical connectives and even the Hoare triples.
2365:
could be used to reason in the presence of sharing, at least in principle. For example, in the triple
1276:
1237:
604:
4929:
4457:
4279:
4142:
2752:
1865:
1821:
126:
45:
4021:
3457:
2282:
4780:
4578:
3977:
Gotsman, Alexey; Berdine, Josh; Cook, Byron; Sagiv, Mooly (2007). "Thread-Modular Shape Analysis".
3862:
3617:
3536:
3481:
1428:
133:
3846:
3781:
3636:
3213:
3170:
Verification of an OpenSSL implementation of a cryptographic authentication algorithm, utilizing
3118:
1762:
1395:
359:
240:
4740:
4496:
4488:
4239:
4156:
1109:
547:
4246:. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 462–482.
4207:. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 415–442.
4163:. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 244–261.
3730:
3276:
1532:
1318:
4975:
4883:
4878:
4681:
4400:
3857:
3531:
3476:
322:
161:
4095:
2528:
2497:
2341:
1795:
790:
293:
4506:
4412:
4405:
4055:
3618:"An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm"
3368:
Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In
3142:
3103:
2196:
935:
578:
4676:
4671:
4558:
4434:
4422:
4351:
3959:
3408:
Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
3049:
2705:
2678:
1512:
1039:
273:
90:
8:
4688:
4523:
4395:
3188:
3138:
1555:
3963:
3817:
658:
211:
4657:
4598:
4568:
4553:
4518:
4417:
4361:
4316:
4164:
4130:
4111:
4009:
3949:
3885:
3814:
3711:
3557:
3549:
3445:
3433:
3385:
3242:
2732:
2658:
2638:
2618:
2477:
2309:
2262:
2242:
2222:
2176:
1993:
1973:
1953:
1929:
1909:
1016:
996:
976:
767:
638:
495:
475:
455:
431:
411:
391:
191:
167:
143:
61:
3904:
3280:
4772:
4346:
4255:
4218:
4182:
3995:
3875:
3701:
3598:
3423:
3220:
3042:
2474:
we obtain the weakest precondition for a statement that mutates the heap at location
4083:
3938:
2338:
In their POPL'01 paper, O'Hearn and Ishtiaq explained how the magic wand connective
4618:
4543:
4452:
4302:
4247:
4208:
4174:
3987:
3919:
3889:
3867:
3796:
3745:
3715:
3693:
3685:
3651:
3588:
3561:
3541:
3437:
3415:
3403:
3343:
2836:
185:
82:
33:
29:
17:
3257:
3232:
2219:) and that its execution will not affect the additional part of the state (and so
4823:
4613:
4533:
4442:
4251:
4213:
4178:
3303:
2824:
98:
4114:. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li:. In
3991:
3939:"Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity"
4841:
4724:
4652:
4632:
4538:
4501:
4467:
4336:
3226:
3164:
3800:
3750:
3129:(from Microsoft Research, focussed on data structures found in device drivers)
3080:
4964:
4528:
4462:
4326:
3602:
3520:
O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications".
2170:
1858:
In separation logic, Hoare triples have a slightly different meaning than in
4098:. Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. In
3923:
3689:
3655:
3499:(1972). "Some techniques for proving programs which alter data structures".
48:
review article by O'Hearn charts developments in the subject to early 2019.
4888:
4871:
4714:
4341:
3697:
3496:
3377:
3347:
3284:
3156:
3122:
3053:
1563:
37:
4240:"Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic"
3419:
3235:
implements a separation logic for message passing, following the ideas in
4704:
4563:
3871:
3373:
3196:
3107:
3057:
2465:{\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ =42\ \{P\}}
2014:
1859:
1640:{\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}
25:
81:
Separation logic supports the developing field of research described by
4790:
4785:
3986:. Lecture Notes in Computer Science. Vol. 5403. pp. 266–277.
3311:
3037:
1559:
452:
over the given store and heap. Separation logic assertions (denoted as
3902:
3553:
3126:
40:. The assertion language of separation logic is a special case of the
4851:
4667:
4447:
3171:
94:
3593:
3576:
3200:
1853:
4750:
4271:
4169:
4155:
Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016).
4143:
Viper: A Verification Infrastructure for Permission-Based Reasoning
3854:
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
3545:
3406:(2001). "BI as an assertion language for mutable data structures".
3192:
1562:
operators. They can be combined using an inference rule similar to
3954:
3765:
Hoare, C.A.R. (1972). "Towards a theory of parallel programming".
3252:
several frontends for various programming languages have emerged:
270:) if their domains do not overlap (i.e., for every memory address
77:
virtual separation (modular reasoning) between concurrent modules.
4745:
4603:
4205:
Tools and Algorithms for the Construction and Analysis of Systems
3307:
3272:
3265:
3845:
Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007).
2017:, separation logic supports the following very important rule:
757:{\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }
4126:
3937:
Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015).
3348:"Separation Logic: A Logic for Shared Mutable Data Structures"
2521:
to provide localized reasoning about mutations in the classic
109:
Separation logic assertions describe "states" consisting of a
36:, Samin Ishtiaq and Hongseok Yang, drawing upon early work by
4903:
4893:
4813:
3318:. Extending this result, satisfiability for an analog of the
512:) contain the standard boolean connectives and, in addition,
71:
4112:
A Practical Verification Framework for Preemptive OS Kernels
4072:
Open-sourcing Facebook Infer: Identify bugs before you ship.
3160:
4856:
4831:
4084:
Using Crash Hoare Logic for Certifying the FSCQ File System
3315:
1926:
executes from an initial state satisfying the precondition
60:
programs that manipulate pointer data structures—including
3669:
Gardner, Philippa; Maffeis, Sergio; Smith, Hareth (2012).
3086:
4244:
Verification, Model Checking, and Abstract Interpretation
4201:
3980:
Verification, Model Checking, and Abstract Interpretation
28:, a way of reasoning about programs. It was developed by
4238:
Reynolds, Andrew; Iosif, Radu; Serban, Cristina (2017).
3261:
3253:
3248:
2823:
can be seen to be a version of the fusion connective of
1068:
parts where its two arguments hold, respectively. I.e.,
97:
checks the validity of another algorithm) and automated
4846:
4159:. In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.).
4154:
4145:, P. Müller, M. Schwerhoff, and A. J. Summers, VMCAI'16
4059:
4038:. European Association for Theoretical Computer Science
3976:
3844:
3470:
3936:
3825:. E.W. Dijkstra Archive. Center for American History,
3155:
type system and some of its standard libraries in the
1752:{\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}
1702:{\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}
104:
2848:
2795:
2755:
2735:
2708:
2681:
2661:
2641:
2621:
2587:
2558:
2531:
2500:
2480:
2373:
2344:
2312:
2285:
2265:
2245:
2225:
2199:
2179:
2025:
1996:
1976:
1956:
1932:
1912:
1868:
1824:
1798:
1765:
1715:
1660:
1574:
1535:
1515:
1468:
1431:
1398:
1354:
1321:
1279:
1240:
1194:
1152:
1112:
1074:
1042:
1019:
999:
979:
938:
856:
813:
793:
770:
726:
690:
661:
641:
607:
581:
550:
518:
498:
478:
458:
434:
414:
394:
362:
325:
296:
276:
243:
214:
194:
170:
146:
3083:
for their invention of Concurrent Separation Logic.
2193:), can also execute in any bigger state (satisfying
709:{\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }
537:{\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }
4237:
4074:
C Calcagno, D DIstefano and P O'Hearn. 11 June 2015
3668:
3121:(which has won several verification competitions),
2279:, i.e. none of them are in the 'free variable' set
4161:Automated Technology for Verification and Analysis
4157:"A Decision Procedure for Separation Logic in SMT"
3401:
3079:O'Hearn and Brookes are co-recipients of the 2016
3025:
2815:
2781:
2741:
2721:
2694:
2667:
2647:
2627:
2607:
2573:
2544:
2513:
2486:
2464:
2357:
2318:
2298:
2271:
2251:
2231:
2211:
2185:
2155:
2002:
1982:
1962:
1938:
1918:
1898:
1842:
1810:
1784:
1751:
1701:
1639:
1546:
1521:
1497:
1454:
1417:
1384:
1332:
1304:
1265:
1226:
1180:
1138:
1098:
1048:
1025:
1005:
985:
965:
924:
842:
799:
776:
756:
708:
672:
647:
627:
593:
567:
536:
504:
484:
464:
440:
420:
400:
380:
345:
311:
282:
262:
225:
200:
176:
152:
4096:Verified correctness and security of OpenSSL HMAC
3637:"The ramifications of sharing in data structures"
3125:(which mixes shape and numerical properties) and
2806:
2805:
2804:
2803:
2802:
2598:
2597:
2596:
2595:
2594:
2567:
2566:
2565:
2564:
2563:
2537:
2536:
2506:
2505:
2418:
2417:
2350:
2349:
1854:Reasoning about programs: triples and proof rules
1832:
1831:
1741:
1740:
1606:
1605:
1540:
1539:
1374:
1373:
1326:
1325:
952:
942:
911:
896:
876:
866:
616:
615:
356:The logic allows to prove judgements of the form
4962:
4203:Solver". In Fisman, Dana; Rosu, Grigore (eds.).
4242:. In Bouajjani, Ahmed; Monniaux, David (eds.).
3662:
3609:
3519:
3297:
2830:
1064:) asserts that the heap can be split into two
188:mapping memory addresses to values. Two heaps
56:Separation logic facilitates reasoning about:
4287:
3782:"A Semantics for Concurrent Separation Logic"
2749:, but which possibly have a nonempty portion
3847:"Local Action and Abstract Separation Logic"
3731:"Resources, Concurrency and Local Reasoning"
3634:
3628:
3306:. An algorithm for solving this fragment in
3017:
2991:
2965:
2939:
2934:
2921:
2908:
2895:
2891:
2878:
2865:
2852:
2459:
2453:
2429:
2374:
2094:
2082:
2070:
2058:
2053:
2047:
2035:
2029:
1893:
1887:
1875:
1869:
1792:; more precisely, the adjoint operators are
3767:Operating System Techniques. Academic Press
3728:
3574:
4945:
4935:
4294:
4280:
3819:Cooperating sequential processes (EWD-123)
3219:The very first Separation Logic verifier,
3203:(a Coq library for low-level programming).
3106:, a static analysis tool for Java, C, and
3048:Commenting on the early classical work on
4212:
4168:
3953:
3861:
3749:
3592:
3535:
3480:
2562:
1836:
1773:
1769:
1745:
1610:
1554:share some properties with the classical
1411:
1407:
1385:{\displaystyle s,h\models P-\!\!\ast \,Q}
1378:
1167:
1163:
621:
251:
247:
3495:
3397:
3395:
3367:
3342:
3338:
3336:
3197:Fine-grained Concurrent Separation Logic
3151:Verification of a large fragment of the
132:in common programming languages such as
117:, roughly corresponding to the state of
4056:Separation logic and bi-abduction, page
3779:
3758:
3635:Hobor, Aquinas; Villard, Jules (2013).
3489:
3087:Verification and program analysis tools
2013:In addition to the standard rules from
4963:
3946:24th European Symposium on Programming
2291:
2288:
2133:
2130:
2111:
2108:
2105:
843:{\displaystyle s,h\models e\mapsto e'}
4275:
3764:
3392:
3361:
3333:
4301:
3813:
3615:
3464:
3277:Asynchronous Liquid Separation Types
2523:Schorr-Waite graph marking algorithm
1970:. In essence, during its execution,
164:mapping variables to values. A heap
1498:{\displaystyle s,h\cup h'\models Q}
1181:{\displaystyle h_{1}\,\bot \,h_{2}}
105:Assertions: operators and semantics
13:
3671:"Towards a program logic for Java
3163:framework for separation logic in
3092:representatives in each category.
2816:{\displaystyle P\cup \!\!\!\!\!*Q}
2608:{\displaystyle P\cup \!\!\!\!\!*Q}
2574:{\displaystyle \cup \,\!\!\!\!\!*}
2150:
1837:
1799:
1770:
1408:
1164:
1099:{\displaystyle s,h\models P\ast Q}
925:{\displaystyle h(\!]_{s})=\!]_{s}}
248:
14:
4997:
3513:
3285:Syntactic Control of Interference
3117:(one of the first SL analyzers),
1227:{\displaystyle h=h_{1}\cup h_{2}}
4944:
4934:
4925:
4924:
4370:
3575:O'Hearn, Peter (February 2019).
1305:{\displaystyle s,h_{2}\models Q}
1266:{\displaystyle s,h_{1}\models P}
973:denotes the value of expression
750:
745:
740:
702:
697:
692:
628:{\displaystyle P{-\!\!\ast }\,Q}
530:
525:
520:
4231:
4195:
4148:
4136:
4120:
4105:
4089:
4077:
4065:
4049:
4028:
3970:
3930:
3896:
3838:
3807:
3773:
3722:
3195:embedding of Smallfoot in HOL;
2894:
2782:{\displaystyle h_{P}\cap h_{Q}}
1899:{\displaystyle \{P\}\ C\ \{Q\}}
1843:{\displaystyle Q-\!\!\ast \,\_}
784:is undefined for all addresses.
4100:24th USENIX Security Symposium
3568:
3237:Singularity (operating system)
2441:
2435:
2426:
2410:
2404:
2398:
2395:
2389:
2383:
2377:
2299:{\displaystyle {\mathsf {fv}}}
2144:
2138:
2122:
2116:
1731:
1693:
1614:
1596:
954:
949:
943:
939:
913:
908:
897:
893:
887:
878:
873:
867:
863:
860:
829:
794:
554:
340:
334:
306:
300:
1:
3827:University of Texas at Austin
3326:
3180:kernel to have been verified.
1455:{\displaystyle s,h'\models P}
70:(avoidance of semantic frame
42:logic of bunched implications
4252:10.1007/978-3-319-52234-0_25
4214:10.1007/978-3-030-99524-9_24
4179:10.1007/978-3-319-46520-3_16
3789:Theoretical Computer Science
3738:Theoretical Computer Science
1906:asserts that if the program
1785:{\displaystyle h\,\bot \,h'}
1418:{\displaystyle h'\,\bot \,h}
381:{\displaystyle s,h\models P}
263:{\displaystyle h\,\bot \,h'}
64:in the presence of pointers;
7:
4648:Curry–Howard correspondence
3992:10.1007/978-3-540-93900-9_3
3298:Decidability and complexity
3183:Other examples include the
3097:Automatic Program Analyses.
2831:Concurrent separation logic
1139:{\displaystyle h_{1},h_{2}}
568:{\displaystyle e\mapsto e'}
51:
10:
5002:
3523:Bulletin of Symbolic Logic
3273:Mezzo Programming Language
2329:
1547:{\displaystyle -\!\!\ast }
1333:{\displaystyle -\!\!\ast }
4986:Logic in computer science
4920:
4822:
4799:
4771:
4764:
4733:
4697:
4640:
4631:
4577:
4487:
4480:
4433:
4388:
4379:
4368:
4309:
4127:The Ynot Project homepage
3801:10.1016/j.tcs.2006.12.034
3780:Brookes, Stephen (2007).
3751:10.1016/j.tcs.2006.12.035
3320:Bernays–Schönfinkel class
3314:has been integrated into
716:asserts that the heap is
346:{\displaystyle h'(\ell )}
3214:auto active verification
2545:{\displaystyle {-\!\!*}}
2514:{\displaystyle {-\!\!*}}
2358:{\displaystyle {-\!\!*}}
1811:{\displaystyle \_\ast Q}
800:{\displaystyle \mapsto }
312:{\displaystyle h(\ell )}
4497:Abstract interpretation
4086:, H Chen et al, SOSP'15
3924:10.1145/2480359.2429104
3729:O'Hearn, Peter (2007).
3690:10.1145/2103656.2103663
3656:10.1145/2480359.2429131
3616:Yang, Hongseok (2001).
3165:The Coq proof assistant
3113:Other examples include
2789:in common. Abstractly,
2212:{\displaystyle P\ast R}
1033:is otherwise undefined.
966:{\displaystyle \!]_{s}}
594:{\displaystyle P\ast Q}
68:"transfer of ownership"
3027:
2817:
2783:
2743:
2723:
2696:
2669:
2649:
2629:
2609:
2575:
2552:but also a connective
2546:
2515:
2488:
2466:
2359:
2320:
2300:
2273:
2253:
2233:
2213:
2187:
2157:
2004:
1984:
1964:
1946:then the program will
1940:
1920:
1900:
1844:
1812:
1786:
1753:
1703:
1641:
1548:
1523:
1499:
1456:
1419:
1386:
1346:separating implication
1334:
1306:
1267:
1228:
1182:
1140:
1100:
1062:separating conjunction
1050:
1027:
1007:
987:
967:
926:
844:
801:
778:
758:
710:
674:
649:
629:
595:
569:
538:
506:
486:
466:
442:
422:
402:
382:
347:
313:
284:
264:
227:
202:
178:
154:
4406:Categorical semantics
3420:10.1145/360204.375719
3143:HOL (proof assistant)
3102:A current example is
3028:
2839:, using a proof rule
2818:
2784:
2744:
2724:
2722:{\displaystyle h_{Q}}
2697:
2695:{\displaystyle h_{P}}
2670:
2650:
2630:
2610:
2576:
2547:
2516:
2489:
2467:
2360:
2321:
2301:
2274:
2254:
2234:
2214:
2188:
2165:This is known as the
2158:
2005:
1985:
1965:
1941:
1921:
1901:
1845:
1813:
1787:
1754:
1704:
1642:
1549:
1524:
1522:{\displaystyle \ast }
1500:
1457:
1420:
1387:
1335:
1307:
1268:
1229:
1183:
1141:
1101:
1051:
1049:{\displaystyle \ast }
1028:
1008:
988:
968:
927:
845:
802:
779:
759:
711:
675:
650:
630:
596:
570:
539:
507:
487:
467:
443:
423:
403:
383:
348:
314:
285:
283:{\displaystyle \ell }
265:
228:
203:
179:
155:
128:dynamically-allocated
4352:Runtime verification
3872:10.1109/LICS.2007.30
3856:. pp. 366–378.
3502:Machine Intelligence
3050:interference freedom
2846:
2793:
2753:
2733:
2706:
2679:
2659:
2639:
2619:
2585:
2556:
2529:
2498:
2478:
2371:
2342:
2310:
2283:
2263:
2243:
2223:
2197:
2177:
2023:
1994:
1974:
1954:
1930:
1910:
1866:
1822:
1796:
1763:
1713:
1658:
1572:
1533:
1513:
1466:
1429:
1396:
1392:when for every heap
1352:
1319:
1315:The binary operator
1277:
1238:
1192:
1150:
1110:
1072:
1040:
1036:The binary operator
1017:
997:
977:
936:
854:
811:
791:
787:The binary operator
768:
724:
688:
659:
639:
605:
579:
548:
516:
496:
476:
456:
432:
412:
392:
360:
323:
294:
274:
241:
212:
192:
168:
144:
91:program verification
4981:Substructural logic
4609:Invariant inference
4357:Safety and liveness
3964:2014arXiv1410.0306S
3912:ACM SIGPLAN Notices
3815:Dijkstra, Edsger W.
3644:ACM SIGPLAN Notices
3189:Coq proof assistant
3139:Coq proof assistant
993:evaluated in store
24:is an extension of
4971:2002 introductions
4773:Constraint solvers
4599:Concolic execution
4554:Symbolic execution
4362:Undefined behavior
4317:Control-flow graph
4131:Harvard University
4060:Infer project site
4036:"2016 Gödel Prize"
3835:) (September 1965)
3684:. pp. 31–44.
3577:"Separation Logic"
3414:. pp. 14–26.
3135:Interactive Proof.
3023:
2813:
2779:
2739:
2719:
2692:
2675:hold for subheaps
2665:
2645:
2625:
2605:
2571:
2542:
2511:
2484:
2462:
2355:
2316:
2296:
2269:
2249:
2229:
2209:
2183:
2153:
2000:
1980:
1960:
1936:
1916:
1896:
1840:
1808:
1782:
1749:
1699:
1637:
1544:
1519:
1495:
1452:
1415:
1382:
1330:
1302:
1263:
1224:
1178:
1136:
1096:
1046:
1023:
1003:
983:
963:
922:
840:
797:
774:
754:
706:
673:{\displaystyle e'}
670:
645:
625:
591:
565:
534:
502:
482:
462:
438:
418:
398:
378:
343:
309:
290:, at least one of
280:
260:
226:{\displaystyle h'}
223:
198:
174:
150:
62:information hiding
4958:
4957:
4916:
4915:
4912:
4911:
4627:
4626:
4476:
4475:
4261:978-3-319-52234-0
4224:978-3-030-99524-9
4188:978-3-319-46520-3
4001:978-3-540-93899-6
3881:978-0-7695-2908-0
3344:Reynolds, John C.
3021:
2742:{\displaystyle h}
2668:{\displaystyle Q}
2648:{\displaystyle P}
2628:{\displaystyle h}
2487:{\displaystyle x}
2452:
2434:
2319:{\displaystyle R}
2272:{\displaystyle R}
2252:{\displaystyle C}
2232:{\displaystyle R}
2186:{\displaystyle P}
2169:(named after the
2102:
2098:
2081:
2075:
2046:
2040:
2003:{\displaystyle C}
1983:{\displaystyle C}
1963:{\displaystyle Q}
1939:{\displaystyle P}
1919:{\displaystyle C}
1886:
1880:
1650:and they form an
1635:
1106:when there exist
1026:{\displaystyle h}
1006:{\displaystyle s}
986:{\displaystyle e}
777:{\displaystyle h}
680:are expressions.
648:{\displaystyle e}
505:{\displaystyle R}
485:{\displaystyle Q}
465:{\displaystyle P}
441:{\displaystyle P}
421:{\displaystyle h}
401:{\displaystyle s}
201:{\displaystyle h}
177:{\displaystyle h}
153:{\displaystyle s}
4993:
4948:
4947:
4938:
4937:
4928:
4927:
4824:Proof assistants
4769:
4768:
4638:
4637:
4485:
4484:
4458:Rewriting system
4453:Process calculus
4386:
4385:
4374:
4303:Program analysis
4296:
4289:
4282:
4273:
4272:
4266:
4265:
4235:
4229:
4228:
4216:
4199:
4193:
4192:
4172:
4152:
4146:
4140:
4134:
4124:
4118:
4116:CAV 2016: 59-79
4109:
4103:
4093:
4087:
4081:
4075:
4069:
4063:
4053:
4047:
4046:
4044:
4043:
4032:
4026:
4025:
4019:
4015:
4013:
4005:
3985:
3974:
3968:
3967:
3957:
3943:
3934:
3928:
3927:
3909:
3900:
3894:
3893:
3865:
3851:
3842:
3836:
3830:
3824:
3811:
3805:
3804:
3795:(1–3): 227–270.
3786:
3777:
3771:
3770:
3762:
3756:
3755:
3753:
3744:(1–3): 271–307.
3735:
3726:
3720:
3719:
3679:
3666:
3660:
3659:
3641:
3632:
3626:
3625:
3613:
3607:
3606:
3596:
3572:
3566:
3565:
3539:
3517:
3511:
3510:
3493:
3487:
3486:
3484:
3468:
3462:
3461:
3455:
3451:
3449:
3441:
3402:Ishtiaq, Samin;
3399:
3390:
3389:
3365:
3359:
3358:
3352:
3340:
3187:library for the
3157:RustBelt project
3032:
3030:
3029:
3024:
3022:
3020:
3016:
3015:
3003:
3002:
2990:
2989:
2977:
2976:
2964:
2963:
2951:
2950:
2937:
2933:
2932:
2920:
2919:
2907:
2906:
2890:
2889:
2877:
2876:
2864:
2863:
2850:
2822:
2820:
2819:
2814:
2788:
2786:
2785:
2780:
2778:
2777:
2765:
2764:
2748:
2746:
2745:
2740:
2728:
2726:
2725:
2720:
2718:
2717:
2701:
2699:
2698:
2693:
2691:
2690:
2674:
2672:
2671:
2666:
2654:
2652:
2651:
2646:
2634:
2632:
2631:
2626:
2615:holds of a heap
2614:
2612:
2611:
2606:
2580:
2578:
2577:
2572:
2551:
2549:
2548:
2543:
2541:
2520:
2518:
2517:
2512:
2510:
2493:
2491:
2490:
2485:
2471:
2469:
2468:
2463:
2450:
2432:
2422:
2364:
2362:
2361:
2356:
2354:
2325:
2323:
2322:
2317:
2305:
2303:
2302:
2297:
2295:
2294:
2278:
2276:
2275:
2270:
2258:
2256:
2255:
2250:
2238:
2236:
2235:
2230:
2218:
2216:
2215:
2210:
2192:
2190:
2189:
2184:
2162:
2160:
2159:
2154:
2137:
2136:
2115:
2114:
2100:
2099:
2097:
2079:
2073:
2056:
2044:
2038:
2027:
2009:
2007:
2006:
2001:
1989:
1987:
1986:
1981:
1969:
1967:
1966:
1961:
1945:
1943:
1942:
1937:
1925:
1923:
1922:
1917:
1905:
1903:
1902:
1897:
1884:
1878:
1849:
1847:
1846:
1841:
1817:
1815:
1814:
1809:
1791:
1789:
1788:
1783:
1781:
1758:
1756:
1755:
1750:
1708:
1706:
1705:
1700:
1680:
1646:
1644:
1643:
1638:
1636:
1634:
1617:
1576:
1553:
1551:
1550:
1545:
1528:
1526:
1525:
1520:
1504:
1502:
1501:
1496:
1488:
1461:
1459:
1458:
1453:
1445:
1424:
1422:
1421:
1416:
1406:
1391:
1389:
1388:
1383:
1339:
1337:
1336:
1331:
1311:
1309:
1308:
1303:
1295:
1294:
1272:
1270:
1269:
1264:
1256:
1255:
1233:
1231:
1230:
1225:
1223:
1222:
1210:
1209:
1187:
1185:
1184:
1179:
1177:
1176:
1162:
1161:
1145:
1143:
1142:
1137:
1135:
1134:
1122:
1121:
1105:
1103:
1102:
1097:
1055:
1053:
1052:
1047:
1032:
1030:
1029:
1024:
1012:
1010:
1009:
1004:
992:
990:
989:
984:
972:
970:
969:
964:
962:
961:
931:
929:
928:
923:
921:
920:
907:
886:
885:
849:
847:
846:
841:
839:
806:
804:
803:
798:
783:
781:
780:
775:
763:
761:
760:
755:
753:
748:
743:
715:
713:
712:
707:
705:
700:
695:
679:
677:
676:
671:
669:
654:
652:
651:
646:
634:
632:
631:
626:
620:
600:
598:
597:
592:
574:
572:
571:
566:
564:
543:
541:
540:
535:
533:
528:
523:
511:
509:
508:
503:
491:
489:
488:
483:
471:
469:
468:
463:
447:
445:
444:
439:
427:
425:
424:
419:
407:
405:
404:
399:
387:
385:
384:
379:
352:
350:
349:
344:
333:
318:
316:
315:
310:
289:
287:
286:
281:
269:
267:
266:
261:
259:
232:
230:
229:
224:
222:
207:
205:
204:
199:
186:partial function
183:
181:
180:
175:
159:
157:
156:
151:
30:John C. Reynolds
22:separation logic
18:computer science
5001:
5000:
4996:
4995:
4994:
4992:
4991:
4990:
4961:
4960:
4959:
4954:
4908:
4818:
4795:
4760:
4734:Data structures
4729:
4693:
4623:
4614:Program slicing
4573:
4472:
4443:Lambda calculus
4429:
4375:
4366:
4327:Hyperproperties
4305:
4300:
4270:
4269:
4262:
4236:
4232:
4225:
4200:
4196:
4189:
4153:
4149:
4141:
4137:
4125:
4121:
4110:
4106:
4094:
4090:
4082:
4078:
4070:
4066:
4054:
4050:
4041:
4039:
4034:
4033:
4029:
4017:
4016:
4007:
4006:
4002:
3983:
3975:
3971:
3941:
3935:
3931:
3907:
3901:
3897:
3882:
3849:
3843:
3839:
3822:
3812:
3808:
3784:
3778:
3774:
3763:
3759:
3733:
3727:
3723:
3708:
3677:
3667:
3663:
3639:
3633:
3629:
3614:
3610:
3594:10.1145/3211968
3573:
3569:
3518:
3514:
3497:Burstall, R. M.
3494:
3490:
3469:
3465:
3453:
3452:
3443:
3442:
3430:
3400:
3393:
3366:
3362:
3350:
3341:
3334:
3329:
3304:PSPACE-complete
3300:
3089:
3011:
3007:
2998:
2994:
2985:
2981:
2972:
2968:
2959:
2955:
2946:
2942:
2938:
2928:
2924:
2915:
2911:
2902:
2898:
2885:
2881:
2872:
2868:
2859:
2855:
2851:
2849:
2847:
2844:
2843:
2833:
2825:relevance logic
2794:
2791:
2790:
2773:
2769:
2760:
2756:
2754:
2751:
2750:
2734:
2731:
2730:
2729:whose union is
2713:
2709:
2707:
2704:
2703:
2686:
2682:
2680:
2677:
2676:
2660:
2657:
2656:
2640:
2637:
2636:
2620:
2617:
2616:
2586:
2583:
2582:
2557:
2554:
2553:
2532:
2530:
2527:
2526:
2501:
2499:
2496:
2495:
2479:
2476:
2475:
2413:
2372:
2369:
2368:
2345:
2343:
2340:
2339:
2332:
2311:
2308:
2307:
2287:
2286:
2284:
2281:
2280:
2264:
2261:
2260:
2244:
2241:
2240:
2224:
2221:
2220:
2198:
2195:
2194:
2178:
2175:
2174:
2129:
2128:
2104:
2103:
2057:
2028:
2026:
2024:
2021:
2020:
1995:
1992:
1991:
1975:
1972:
1971:
1955:
1952:
1951:
1931:
1928:
1927:
1911:
1908:
1907:
1867:
1864:
1863:
1856:
1823:
1820:
1819:
1797:
1794:
1793:
1774:
1764:
1761:
1760:
1714:
1711:
1710:
1709:if and only if
1673:
1659:
1656:
1655:
1618:
1577:
1575:
1573:
1570:
1569:
1534:
1531:
1530:
1514:
1511:
1510:
1481:
1467:
1464:
1463:
1438:
1430:
1427:
1426:
1399:
1397:
1394:
1393:
1353:
1350:
1349:
1320:
1317:
1316:
1290:
1286:
1278:
1275:
1274:
1251:
1247:
1239:
1236:
1235:
1218:
1214:
1205:
1201:
1193:
1190:
1189:
1172:
1168:
1157:
1153:
1151:
1148:
1147:
1130:
1126:
1117:
1113:
1111:
1108:
1107:
1073:
1070:
1069:
1041:
1038:
1037:
1018:
1015:
1014:
998:
995:
994:
978:
975:
974:
957:
953:
937:
934:
933:
916:
912:
900:
881:
877:
855:
852:
851:
832:
812:
809:
808:
792:
789:
788:
769:
766:
765:
749:
744:
739:
725:
722:
721:
701:
696:
691:
689:
686:
685:
662:
660:
657:
656:
640:
637:
636:
611:
606:
603:
602:
580:
577:
576:
557:
549:
546:
545:
529:
524:
519:
517:
514:
513:
497:
494:
493:
477:
474:
473:
457:
454:
453:
433:
430:
429:
428:is a heap, and
413:
410:
409:
393:
390:
389:
361:
358:
357:
353:is undefined).
326:
324:
321:
320:
295:
292:
291:
275:
272:
271:
252:
242:
239:
238:
215:
213:
210:
209:
193:
190:
189:
169:
166:
165:
145:
142:
141:
121:stack-allocated
107:
99:parallelization
87:local reasoning
54:
12:
11:
5:
4999:
4989:
4988:
4983:
4978:
4973:
4956:
4955:
4953:
4952:
4942:
4932:
4921:
4918:
4917:
4914:
4913:
4910:
4909:
4907:
4906:
4901:
4896:
4891:
4886:
4881:
4876:
4875:
4874:
4864:
4859:
4854:
4849:
4844:
4839:
4834:
4828:
4826:
4820:
4819:
4817:
4816:
4811:
4805:
4803:
4797:
4796:
4794:
4793:
4788:
4783:
4777:
4775:
4766:
4762:
4761:
4759:
4758:
4753:
4748:
4743:
4737:
4735:
4731:
4730:
4728:
4727:
4722:
4717:
4712:
4707:
4701:
4699:
4695:
4694:
4692:
4691:
4686:
4685:
4684:
4674:
4665:
4660:
4655:
4653:Loop invariant
4650:
4644:
4642:
4635:
4633:Formal methods
4629:
4628:
4625:
4624:
4622:
4621:
4616:
4611:
4606:
4601:
4596:
4595:
4594:
4592:Taint tracking
4583:
4581:
4575:
4574:
4572:
4571:
4566:
4561:
4556:
4551:
4546:
4541:
4539:Model checking
4536:
4531:
4526:
4521:
4516:
4515:
4514:
4504:
4499:
4493:
4491:
4482:
4478:
4477:
4474:
4473:
4471:
4470:
4468:Turing machine
4465:
4460:
4455:
4450:
4445:
4439:
4437:
4431:
4430:
4428:
4427:
4426:
4425:
4420:
4410:
4409:
4408:
4398:
4392:
4390:
4383:
4377:
4376:
4369:
4367:
4365:
4364:
4359:
4354:
4349:
4347:Rice's theorem
4344:
4339:
4337:Path explosion
4334:
4329:
4324:
4319:
4313:
4311:
4307:
4306:
4299:
4298:
4291:
4284:
4276:
4268:
4267:
4260:
4230:
4223:
4194:
4187:
4147:
4135:
4119:
4104:
4088:
4076:
4064:
4048:
4027:
4018:|journal=
4000:
3969:
3929:
3895:
3880:
3863:10.1.1.66.6337
3837:
3806:
3772:
3757:
3721:
3706:
3661:
3627:
3608:
3567:
3546:10.2307/421090
3537:10.1.1.27.4742
3530:(2): 215–244.
3512:
3488:
3482:10.1.1.29.1331
3463:
3454:|journal=
3428:
3404:O'Hearn, Peter
3391:
3360:
3331:
3330:
3328:
3325:
3299:
3296:
3291:
3290:
3289:
3288:
3269:
3264:for Rust, and
3246:
3240:
3230:
3224:
3206:
3205:
3204:
3181:
3174:
3168:
3149:
3132:
3131:
3130:
3111:
3104:Facebook Infer
3088:
3085:
3043:memory manager
3034:
3033:
3019:
3014:
3010:
3006:
3001:
2997:
2993:
2988:
2984:
2980:
2975:
2971:
2967:
2962:
2958:
2954:
2949:
2945:
2941:
2936:
2931:
2927:
2923:
2918:
2914:
2910:
2905:
2901:
2897:
2893:
2888:
2884:
2880:
2875:
2871:
2867:
2862:
2858:
2854:
2832:
2829:
2812:
2809:
2801:
2798:
2776:
2772:
2768:
2763:
2759:
2738:
2716:
2712:
2689:
2685:
2664:
2644:
2624:
2604:
2601:
2593:
2590:
2570:
2561:
2540:
2535:
2509:
2504:
2483:
2461:
2458:
2455:
2449:
2446:
2443:
2440:
2437:
2431:
2428:
2425:
2421:
2416:
2412:
2409:
2406:
2403:
2400:
2397:
2394:
2391:
2388:
2385:
2382:
2379:
2376:
2353:
2348:
2331:
2328:
2315:
2293:
2290:
2268:
2259:occur free in
2248:
2228:
2208:
2205:
2202:
2182:
2152:
2149:
2146:
2143:
2140:
2135:
2132:
2127:
2124:
2121:
2118:
2113:
2110:
2107:
2096:
2093:
2090:
2087:
2084:
2078:
2072:
2069:
2066:
2063:
2060:
2055:
2052:
2049:
2043:
2037:
2034:
2031:
1999:
1979:
1959:
1935:
1915:
1895:
1892:
1889:
1883:
1877:
1874:
1871:
1855:
1852:
1839:
1835:
1830:
1827:
1807:
1804:
1801:
1780:
1777:
1772:
1768:
1748:
1744:
1739:
1736:
1733:
1730:
1727:
1724:
1721:
1718:
1698:
1695:
1692:
1689:
1686:
1683:
1679:
1676:
1672:
1669:
1666:
1663:
1648:
1647:
1633:
1630:
1627:
1624:
1621:
1616:
1613:
1609:
1604:
1601:
1598:
1595:
1592:
1589:
1586:
1583:
1580:
1543:
1538:
1518:
1509:The operators
1507:
1506:
1494:
1491:
1487:
1484:
1480:
1477:
1474:
1471:
1451:
1448:
1444:
1441:
1437:
1434:
1414:
1410:
1405:
1402:
1381:
1377:
1372:
1369:
1366:
1363:
1360:
1357:
1329:
1324:
1313:
1301:
1298:
1293:
1289:
1285:
1282:
1262:
1259:
1254:
1250:
1246:
1243:
1221:
1217:
1213:
1208:
1204:
1200:
1197:
1175:
1171:
1166:
1160:
1156:
1133:
1129:
1125:
1120:
1116:
1095:
1092:
1089:
1086:
1083:
1080:
1077:
1045:
1034:
1022:
1002:
982:
960:
956:
951:
948:
945:
941:
919:
915:
910:
906:
903:
899:
895:
892:
889:
884:
880:
875:
872:
869:
865:
862:
859:
838:
835:
831:
828:
825:
822:
819:
816:
796:
785:
773:
752:
747:
742:
738:
735:
732:
729:
704:
699:
694:
668:
665:
644:
624:
619:
614:
610:
590:
587:
584:
563:
560:
556:
553:
532:
527:
522:
501:
481:
461:
437:
417:
397:
377:
374:
371:
368:
365:
342:
339:
336:
332:
329:
308:
305:
302:
299:
279:
258:
255:
250:
246:
221:
218:
197:
173:
149:
106:
103:
85:and others as
79:
78:
75:
65:
53:
50:
9:
6:
4:
3:
2:
4998:
4987:
4984:
4982:
4979:
4977:
4976:Program logic
4974:
4972:
4969:
4968:
4966:
4951:
4943:
4941:
4933:
4931:
4923:
4922:
4919:
4905:
4902:
4900:
4897:
4895:
4892:
4890:
4887:
4885:
4882:
4880:
4877:
4873:
4870:
4869:
4868:
4865:
4863:
4860:
4858:
4855:
4853:
4850:
4848:
4845:
4843:
4840:
4838:
4835:
4833:
4830:
4829:
4827:
4825:
4821:
4815:
4812:
4810:
4807:
4806:
4804:
4802:
4798:
4792:
4789:
4787:
4784:
4782:
4779:
4778:
4776:
4774:
4770:
4767:
4763:
4757:
4754:
4752:
4749:
4747:
4744:
4742:
4739:
4738:
4736:
4732:
4726:
4723:
4721:
4718:
4716:
4713:
4711:
4710:Incorrectness
4708:
4706:
4703:
4702:
4700:
4696:
4690:
4687:
4683:
4680:
4679:
4678:
4677:Specification
4675:
4673:
4669:
4666:
4664:
4661:
4659:
4656:
4654:
4651:
4649:
4646:
4645:
4643:
4639:
4636:
4634:
4630:
4620:
4617:
4615:
4612:
4610:
4607:
4605:
4602:
4600:
4597:
4593:
4590:
4589:
4588:
4585:
4584:
4582:
4580:
4576:
4570:
4567:
4565:
4562:
4560:
4557:
4555:
4552:
4550:
4547:
4545:
4542:
4540:
4537:
4535:
4532:
4530:
4529:Effect system
4527:
4525:
4522:
4520:
4517:
4513:
4510:
4509:
4508:
4505:
4503:
4500:
4498:
4495:
4494:
4492:
4490:
4486:
4483:
4479:
4469:
4466:
4464:
4463:State machine
4461:
4459:
4456:
4454:
4451:
4449:
4446:
4444:
4441:
4440:
4438:
4436:
4432:
4424:
4421:
4419:
4416:
4415:
4414:
4411:
4407:
4404:
4403:
4402:
4399:
4397:
4394:
4393:
4391:
4387:
4384:
4382:
4378:
4373:
4363:
4360:
4358:
4355:
4353:
4350:
4348:
4345:
4343:
4340:
4338:
4335:
4333:
4330:
4328:
4325:
4323:
4320:
4318:
4315:
4314:
4312:
4308:
4304:
4297:
4292:
4290:
4285:
4283:
4278:
4277:
4274:
4263:
4257:
4253:
4249:
4245:
4241:
4234:
4226:
4220:
4215:
4210:
4206:
4198:
4190:
4184:
4180:
4176:
4171:
4166:
4162:
4158:
4151:
4144:
4139:
4132:
4128:
4123:
4117:
4113:
4108:
4102:, August 2015
4101:
4097:
4092:
4085:
4080:
4073:
4068:
4061:
4057:
4052:
4037:
4031:
4023:
4011:
4003:
3997:
3993:
3989:
3982:
3981:
3973:
3965:
3961:
3956:
3951:
3947:
3940:
3933:
3925:
3921:
3917:
3913:
3906:
3899:
3891:
3887:
3883:
3877:
3873:
3869:
3864:
3859:
3855:
3848:
3841:
3834:
3833:transcription
3828:
3821:
3820:
3816:
3810:
3802:
3798:
3794:
3790:
3783:
3776:
3768:
3761:
3752:
3747:
3743:
3739:
3732:
3725:
3717:
3713:
3709:
3707:9781450310833
3703:
3699:
3698:10044/1/33265
3695:
3691:
3687:
3683:
3676:
3674:
3665:
3657:
3653:
3649:
3645:
3638:
3631:
3623:
3619:
3612:
3604:
3600:
3595:
3590:
3586:
3582:
3578:
3571:
3563:
3559:
3555:
3551:
3547:
3543:
3538:
3533:
3529:
3525:
3524:
3516:
3508:
3504:
3503:
3498:
3492:
3483:
3478:
3474:
3467:
3459:
3447:
3439:
3435:
3431:
3425:
3421:
3417:
3413:
3409:
3405:
3398:
3396:
3387:
3383:
3379:
3378:Woodcock, Jim
3375:
3371:
3364:
3356:
3349:
3345:
3339:
3337:
3332:
3324:
3321:
3317:
3313:
3309:
3305:
3295:
3286:
3282:
3278:
3274:
3270:
3267:
3263:
3259:
3255:
3250:
3247:
3244:
3241:
3238:
3234:
3231:
3228:
3225:
3222:
3218:
3217:
3215:
3210:
3207:
3202:
3198:
3194:
3190:
3186:
3182:
3179:
3175:
3173:
3169:
3166:
3162:
3158:
3154:
3150:
3147:
3146:
3144:
3140:
3136:
3133:
3128:
3124:
3120:
3116:
3112:
3109:
3105:
3101:
3100:
3098:
3095:
3094:
3093:
3084:
3082:
3077:
3073:
3069:
3065:
3061:
3059:
3055:
3051:
3046:
3044:
3039:
3012:
3008:
3004:
2999:
2995:
2986:
2982:
2978:
2973:
2969:
2960:
2956:
2952:
2947:
2943:
2929:
2925:
2916:
2912:
2903:
2899:
2886:
2882:
2873:
2869:
2860:
2856:
2842:
2841:
2840:
2838:
2837:Peter O'Hearn
2828:
2826:
2810:
2807:
2799:
2796:
2774:
2770:
2766:
2761:
2757:
2736:
2714:
2710:
2687:
2683:
2662:
2642:
2622:
2602:
2599:
2591:
2588:
2568:
2559:
2538:
2533:
2524:
2507:
2502:
2481:
2472:
2456:
2447:
2444:
2438:
2423:
2419:
2414:
2407:
2401:
2392:
2386:
2380:
2366:
2351:
2346:
2336:
2327:
2313:
2266:
2246:
2226:
2206:
2203:
2200:
2180:
2172:
2171:frame problem
2168:
2163:
2147:
2141:
2125:
2119:
2091:
2088:
2085:
2076:
2067:
2064:
2061:
2050:
2041:
2032:
2018:
2016:
2011:
1997:
1977:
1957:
1949:
1933:
1913:
1890:
1881:
1872:
1862:. The triple
1861:
1851:
1833:
1828:
1825:
1805:
1802:
1778:
1775:
1766:
1746:
1742:
1737:
1734:
1728:
1725:
1722:
1719:
1716:
1696:
1690:
1687:
1684:
1681:
1677:
1674:
1670:
1667:
1664:
1661:
1653:
1631:
1628:
1625:
1622:
1619:
1611:
1607:
1602:
1599:
1593:
1590:
1587:
1584:
1581:
1578:
1568:
1567:
1566:
1565:
1561:
1557:
1541:
1536:
1516:
1492:
1489:
1485:
1482:
1478:
1475:
1472:
1469:
1449:
1446:
1442:
1439:
1435:
1432:
1412:
1403:
1400:
1379:
1375:
1370:
1367:
1364:
1361:
1358:
1355:
1347:
1343:
1327:
1322:
1314:
1299:
1296:
1291:
1287:
1283:
1280:
1260:
1257:
1252:
1248:
1244:
1241:
1219:
1215:
1211:
1206:
1202:
1198:
1195:
1173:
1169:
1158:
1154:
1131:
1127:
1123:
1118:
1114:
1093:
1090:
1087:
1084:
1081:
1078:
1075:
1067:
1063:
1059:
1043:
1035:
1020:
1000:
980:
958:
946:
917:
904:
901:
890:
882:
870:
857:
836:
833:
826:
823:
820:
817:
814:
786:
771:
736:
733:
730:
727:
719:
684:The constant
683:
682:
681:
666:
663:
642:
622:
617:
612:
608:
588:
585:
582:
561:
558:
551:
499:
479:
459:
451:
435:
415:
395:
375:
372:
369:
366:
363:
354:
337:
330:
327:
303:
297:
277:
256:
253:
244:
236:
219:
216:
195:
187:
171:
163:
147:
139:
135:
131:
129:
124:
122:
116:
112:
102:
101:of software.
100:
96:
92:
88:
84:
83:Peter O'Hearn
76:
73:
69:
66:
63:
59:
58:
57:
49:
47:
43:
39:
35:
34:Peter O'Hearn
31:
27:
23:
19:
4872:Isabelle/HOL
4719:
4689:Verification
4672:completeness
4564:Type systems
4507:Control flow
4401:Denotational
4342:Polyvariance
4310:Key concepts
4243:
4233:
4204:
4197:
4160:
4150:
4138:
4122:
4115:
4107:
4099:
4091:
4079:
4067:
4051:
4040:. Retrieved
4030:
3979:
3972:
3945:
3932:
3915:
3911:
3898:
3853:
3840:
3818:
3809:
3792:
3788:
3775:
3766:
3760:
3741:
3737:
3724:
3681:
3672:
3664:
3647:
3643:
3630:
3621:
3611:
3587:(2): 86–95.
3584:
3580:
3570:
3527:
3521:
3515:
3506:
3500:
3491:
3472:
3466:
3407:
3381:
3374:Roscoe, Bill
3363:
3354:
3301:
3292:
3260:for Python,
3208:
3177:
3172:verifiable C
3134:
3115:SpaceInvader
3096:
3090:
3078:
3074:
3070:
3066:
3062:
3054:Susan Owicki
3047:
3035:
2834:
2473:
2367:
2337:
2333:
2166:
2164:
2019:
2012:
1948:not go wrong
1947:
1857:
1649:
1564:modus ponens
1508:
1345:
1341:
1340:(pronounced
1065:
1061:
1057:
1056:(pronounced
717:
449:
408:is a store,
355:
234:
127:
120:
114:
110:
108:
86:
80:
67:
55:
38:Rod Burstall
21:
15:
4801:Lightweight
4663:Side effect
4559:Termination
4413:Operational
4322:Correctness
3918:: 287–300.
3650:: 523–536.
3581:Commun. ACM
3370:Davies, Jim
3312:SMT solvers
3294:verifiers.
3281:Alias Types
3227:SmallfootRG
3209:In Between.
3178:pre-emptive
3108:Objective-C
3081:Gödel Prize
3058:David Gries
2015:Hoare logic
1860:Hoare logic
1560:implication
1556:conjunction
123:) variables
26:Hoare logic
4965:Categories
4756:Union-find
4720:Separation
4658:Refinement
4524:Dependence
4423:Small-step
4332:Invariants
4170:1603.06844
4042:2022-08-29
3429:1581133367
3327:References
3159:using the
3038:Tony Hoare
2167:frame rule
1652:adjunction
1425:such that
1342:magic wand
1146:such that
140:. A store
119:local (or
93:(where an
4852:HOL Light
4682:Languages
4668:Soundness
4587:Data-flow
4569:Typestate
4519:Data-flow
4448:Petri net
4396:Axiomatic
4381:Semantics
4020:ignored (
4010:cite book
3955:1410.0306
3858:CiteSeerX
3603:0001-0782
3532:CiteSeerX
3477:CiteSeerX
3456:ignored (
3446:cite book
3221:Smallfoot
3005:∗
2979:∥
2953:∗
2808:∗
2800:∪
2767:∩
2600:∗
2592:∪
2569:∗
2560:∪
2539:∗
2534:−
2508:∗
2503:−
2420:∗
2415:−
2405:↦
2393:∗
2387:−
2384:↦
2352:∗
2347:−
2204:∗
2151:∅
2126:∩
2089:∗
2065:∗
1838:_
1834:∗
1829:−
1803:∗
1800:_
1771:⊥
1743:∗
1738:−
1732:⇒
1726:⊨
1694:⇒
1688:∗
1682:⊨
1671:∪
1629:⊨
1608:∗
1603:−
1594:∗
1588:⊨
1542:∗
1537:−
1517:∗
1490:⊨
1479:∪
1447:⊨
1409:⊥
1376:∗
1371:−
1365:⊨
1328:∗
1323:−
1297:⊨
1258:⊨
1212:∪
1165:⊥
1091:∗
1085:⊨
1044:∗
830:↦
824:⊨
795:↦
737:⊨
618:∗
613:−
586:∗
555:↦
450:assertion
373:⊨
338:ℓ
304:ℓ
278:ℓ
249:⊥
237:(denoted
95:algorithm
4950:Glossary
4930:Category
4867:Isabelle
4751:Hashcons
4725:Temporal
4641:Concepts
4481:Analyses
4418:Big-step
3386:Palgrave
3380:(eds.).
3346:(2002).
3256:for Go,
3243:VeriFast
3233:Heap Hop
3119:Predator
2010:itself.
1779:′
1678:′
1654:, i.e.,
1486:′
1443:′
1404:′
1066:disjoint
905:′
837:′
720:, i.e.,
667:′
635:, where
562:′
388:, where
331:′
257:′
235:disjoint
220:′
162:function
52:Overview
44:(BI). A
4940:Outline
4746:E-graph
4619:Testing
4604:Fuzzing
4579:Dynamic
4544:Pointer
3960:Bibcode
3905:"Views"
3890:1044254
3716:9571576
3562:2948552
3438:2652274
3310:-based
3308:DPLL(T)
3266:VerCors
3201:Bedrock
3193:Holfoot
2330:Sharing
1462:, also
932:(where
130:objects
4715:Linear
4698:Logics
4534:Escape
4489:Static
4435:Models
4258:
4221:
4185:
4133:, USA.
3998:
3888:
3878:
3860:
3714:
3704:
3673:Script
3601:
3560:
3554:421090
3552:
3534:
3479:
3436:
3426:
3262:Prusti
3258:Nagini
3199:, and
3191:; the
3127:SLAyer
3123:MemCAD
2451:
2433:
2101:
2080:
2074:
2045:
2039:
1885:
1879:
1505:holds.
1013:) and
601:, and
448:is an
113:and a
74:); and
72:axioms
4904:Twelf
4894:NuPRL
4889:Mizar
4862:Idris
4809:Alloy
4765:Tools
4705:Hoare
4549:Shape
4502:Alias
4389:Types
4165:arXiv
3984:(PDF)
3950:arXiv
3942:(PDF)
3908:(PDF)
3886:S2CID
3850:(PDF)
3823:(PDF)
3785:(PDF)
3734:(PDF)
3712:S2CID
3678:(PDF)
3640:(PDF)
3558:S2CID
3550:JSTOR
3434:S2CID
3351:(PDF)
3254:Gobra
3249:Viper
2635:when
850:when
764:when
718:empty
184:is a
160:is a
111:store
4884:LEGO
4879:Lean
4857:HOL4
4837:Agda
4832:ACL2
4814:TLA+
4670:and
4512:kCFA
4256:ISBN
4219:ISBN
4183:ISBN
4022:help
3996:ISBN
3876:ISBN
3702:ISBN
3599:ISSN
3458:help
3424:ISBN
3355:LICS
3316:cvc5
3283:and
3275:and
3271:The
3185:Ynot
3161:Iris
3153:Rust
3141:and
3056:and
2702:and
2655:and
1818:and
1759:for
1558:and
1529:and
1273:and
1234:and
1188:and
1058:star
655:and
319:and
233:are
208:and
138:Java
136:and
125:and
115:heap
46:CACM
4899:PVS
4842:Coq
4791:SMT
4786:SAT
4781:CHC
4741:BDD
4248:doi
4209:doi
4175:doi
3988:doi
3920:doi
3868:doi
3797:doi
3793:375
3746:doi
3742:375
3694:hdl
3686:doi
3652:doi
3589:doi
3542:doi
3473:CSL
3416:doi
3412:ACM
3052:by
2306:of
1344:or
1060:or
16:In
4967::
4847:F*
4254:.
4217:.
4181:.
4173:.
4129:,
4058:,
4014::
4012:}}
4008:{{
3994:.
3958:.
3948:.
3944:.
3916:48
3914:.
3910:.
3884:.
3874:.
3866:.
3852:.
3791:.
3787:.
3740:.
3736:.
3710:.
3700:.
3692:.
3680:.
3648:48
3646:.
3642:.
3620:.
3597:.
3585:62
3583:.
3579:.
3556:.
3548:.
3540:.
3526:.
3505:.
3475:.
3450::
3448:}}
3444:{{
3432:.
3422:.
3410:.
3394:^
3384:.
3376:;
3372:;
3353:.
3335:^
3045:.
2827:.
2448:42
2408:42
2326:.
1850:.
575:,
544:,
492:,
472:,
32:,
20:,
4295:e
4288:t
4281:v
4264:.
4250::
4227:.
4211::
4191:.
4177::
4167::
4062:.
4045:.
4024:)
4004:.
3990::
3966:.
3962::
3952::
3926:.
3922::
3892:.
3870::
3831:(
3829:.
3803:.
3799::
3769:.
3754:.
3748::
3718:.
3696::
3688::
3675:"
3658:.
3654::
3624:.
3605:.
3591::
3564:.
3544::
3528:5
3509:.
3507:7
3485:.
3460:)
3440:.
3418::
3388:.
3357:.
3287:.
3239:.
3167:.
3018:}
3013:2
3009:Q
3000:1
2996:Q
2992:{
2987:2
2983:C
2974:1
2970:C
2966:}
2961:2
2957:P
2948:1
2944:P
2940:{
2935:}
2930:2
2926:Q
2922:{
2917:2
2913:C
2909:}
2904:2
2900:P
2896:{
2892:}
2887:1
2883:Q
2879:{
2874:1
2870:C
2866:}
2861:1
2857:P
2853:{
2811:Q
2797:P
2775:Q
2771:h
2762:P
2758:h
2737:h
2715:Q
2711:h
2688:P
2684:h
2663:Q
2643:P
2623:h
2603:Q
2589:P
2482:x
2460:}
2457:P
2454:{
2445:=
2442:]
2439:x
2436:[
2430:}
2427:)
2424:P
2411:)
2402:x
2399:(
2396:(
2390:)
2381:x
2378:(
2375:{
2314:R
2292:v
2289:f
2267:R
2247:C
2227:R
2207:R
2201:P
2181:P
2148:=
2145:)
2142:R
2139:(
2134:v
2131:f
2123:)
2120:C
2117:(
2112:d
2109:o
2106:m
2095:}
2092:R
2086:Q
2083:{
2077:C
2071:}
2068:R
2062:P
2059:{
2054:}
2051:Q
2048:{
2042:C
2036:}
2033:P
2030:{
1998:C
1978:C
1958:Q
1934:P
1914:C
1894:}
1891:Q
1888:{
1882:C
1876:}
1873:P
1870:{
1826:Q
1806:Q
1776:h
1767:h
1747:R
1735:Q
1729:P
1723:h
1720:,
1717:s
1697:R
1691:Q
1685:P
1675:h
1668:h
1665:,
1662:s
1632:Q
1626:h
1623:,
1620:s
1615:)
1612:Q
1600:P
1597:(
1591:P
1585:h
1582:,
1579:s
1493:Q
1483:h
1476:h
1473:,
1470:s
1450:P
1440:h
1436:,
1433:s
1413:h
1401:h
1380:Q
1368:P
1362:h
1359:,
1356:s
1312:.
1300:Q
1292:2
1288:h
1284:,
1281:s
1261:P
1253:1
1249:h
1245:,
1242:s
1220:2
1216:h
1207:1
1203:h
1199:=
1196:h
1174:2
1170:h
1159:1
1155:h
1132:2
1128:h
1124:,
1119:1
1115:h
1094:Q
1088:P
1082:h
1079:,
1076:s
1021:h
1001:s
981:e
959:s
955:]
950:]
947:e
944:[
940:[
918:s
914:]
909:]
902:e
898:[
894:[
891:=
888:)
883:s
879:]
874:]
871:e
868:[
864:[
861:(
858:h
834:e
827:e
821:h
818:,
815:s
772:h
751:p
746:m
741:e
734:h
731:,
728:s
703:p
698:m
693:e
664:e
643:e
623:Q
609:P
589:Q
583:P
559:e
552:e
531:p
526:m
521:e
500:R
480:Q
460:P
436:P
416:h
396:s
376:P
370:h
367:,
364:s
341:)
335:(
328:h
307:)
301:(
298:h
254:h
245:h
217:h
196:h
172:h
148:s
134:C
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.