{{Short description|Concurrent program verification method}} In computer science, '''interference freedom''' is a technique for proving partial correctness of concurrent programs with shared variables. Hoare logic had been introduced earlier to prove the correctness of sequential programs. In her PhD thesis<ref name="OwickiThesis">{{cite thesis |last= Owicki |first= Susan S. |date= August 1975 |title= Axiomatic Proof Techniques for Parallel Programs |publisher= Cornell University |hdl= 1813/6393 |type= PhD thesis |url= https://hdl.handle.net/1813/6393 |access-date=2022-07-01}}</ref> (and papers arising from it <ref name="Owicki-Gries">{{cite journal |last1=Owicki |first1=Susan |author-link1=Susan Owicki |last2=Gries |first2=David |author-link2=David Gries |title=An axiomatic proof technique for parallel programs I |journal=Acta Informatica |volume=6 |issue=4 |pages=319&ndash;340 |publisher=Springer (Germany) |location=Berlin |date=25 June 1976 |doi=10.1007/BF00268134 |s2cid=206773583 |url=https://doi.org/10.1007/BF00268134|url-access=subscription }}</ref><ref name="Owicki-Gries2">{{Cite journal |last1=Owicki |first1=Susan |authorlink1=Susan Owicki |last2=Gries |first2=David |authorlink2=David Gries |title=Verifying properties of parallel programs: an axiomatic approach |doi=10.1145/360051.360224 |journal=Communications of the ACM |volume=19 |issue=5 |pages=279&ndash;285 |date=May 1976 |s2cid=9099351 |doi-access=free }}</ref>) under advisor David Gries, Susan Owicki extended this work to apply to concurrent programs.

Concurrent programming had been in use since the mid-1960s for coding operating systems as sets of concurrent processes (see, in particular, Dijkstra.<ref name="DijkstraTHE"> {{Citation |last=Dijkstra |first=E.W. |author-link=Edsger W. Dijkstra |title=The structure of the 'THE'-multiprogramming system |journal=Communications of the ACM |volume=11 |issue=5 |pages=341–346 |year=1968 |doi=10.1145/363095.363143 |s2cid=2021311 |doi-access=free }} </ref>), but there was no formal mechanism for proving correctness. Reasoning about interleaved execution sequences of the individual processes was difficult, was error prone, and didn't scale up. Interference freedom applies to ''proofs'' instead of execution sequences; one shows that execution of one process cannot interfere with the correctness proof of another process.

A range of intricate concurrent programs have been proved correct using interference freedom, and interference freedom provides the basis for much of the ensuing work on developing concurrent programs with shared variables and proving them correct. The Owicki-Gries paper ''An axiomatic proof technique for parallel programs'' <ref name="Owicki-Gries" /> received the 1977 ACM Award for best paper in programming languages and systems.<ref>{{cite web|url=https://awards.acm.org/award_winners/owicki_1219047 |publisher=Awards.acm.org |title=Susan S Owicki |date= |accessdate=2022-07-01}}</ref><ref>{{cite web|url=https://awards.acm.org/award-winners/GRIES_1028422 |publisher=Awards.acm.org |title=David Gries |date= |accessdate=2022-07-01}}</ref>

'''Note.''' Lamport <ref name="LamportFreedom">{{Cite journal |last1=Lamport |first1=Leslie |authorlink1=Leslie Lamport |title=Proving the correctness of multiprocess programs |journal=IEEE Transactions on Software Engineering |volume=SE-3 |issue=2 |pages=125–143 |date=March 1977 |doi=10.1109/TSE.1977.229904 |bibcode=1977ITSEn...3..125L |s2cid=9985552 }}</ref> presents a similar idea. He writes, "After writing the initial version of this paper, we learned of the recent work of Owicki.<ref name="OwickiThesis" /><ref name="Owicki-Gries" />" His paper has not received as much attention as Owicki-Gries, perhaps because it used flow charts instead of the text of programming constructs like the '''if''' statement and '''while''' loop. Lamport was generalizing Floyd's method, <ref name="FloydAssigningMeaning">{{cite book |last=Floyd |first=Robert W. |author-link=Robert W. Floyd |year=1967 |chapter=Assigning Meanings to Programs |chapter-url=//people.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf |editor-first=J.T. |editor-last=Schwartz |title=Mathematical Aspects of Computer Science |publisher=American Mathematical Society |isbn=0821867288 |pages=19–32 |url=https://books.google.com/books?id=ynigSICJflYC |series=Proceedings of Symposium on Applied Mathematics |volume=19 }}</ref> while Owicki-Gries was generalizing Hoare's method.<ref name="HoareAxiomaticBasis">{{Cite journal |last1=Hoare |first1=C. A. R. |authorlink1=C.A.R. Hoare |title=An axiomatic basis for computer programming |doi=10.1145/363235.363259 |journal=Communications of the ACM |volume=12 |issue=10 |pages=576–580 |date=October 1969 |s2cid=207726175 |doi-access=free }}</ref> Essentially, all later work in this area uses text and not flow charts. Another difference is mentioned below in the section on Auxiliary variables.

==Dijkstra's Principle of non-interference== Edsger W. Dijkstra introduced the ''principle of non-interference'' in EWD 117, "Programming Considered as a Human Activity", written about 1965.<ref>{{cite web |website=E. W. Dijkstra Archive |publisher=University of Texas |url=https://www.cs.utexas.edu/~EWD/ewd01xx/EWD117.PDF |title=Programming Considered as a Human Activity}}</ref> This principle states that: The correctness of the whole can be established by taking into account only the exterior specifications (abbreviated ''specs'' throughout) of the parts, and not their interior construction. Dijkstra outlined the general steps in using this principle:

# Give a complete spec of each individual part. # Check that the total problem is solved when program parts meeting their specs are available. # Construct the individual parts to satisfy their specs, but independent of one another and the context in which they will be used.

He gave several examples of this principle outside of programming. But its use in programming is a main concern. For example, a programmer using a method (subroutine, function, etc.) should rely only on its spec to determine what it does and how to call it, and ''never'' on its implementation.

Program specs are written in Hoare logic, introduced by Sir Tony Hoare,<ref name="HoareAxiomaticBasis" /> as exemplified in the specs of processes {{math|S1}} and {{math|S2}}:

{{spaces|2|em}}{{math|{pre-S1}}}{{spaces|5.5|em}}{{math|{pre-S2}}}<br />{{spaces|2|em}}{{math|S1}}{{spaces|15|em}}{{math|S2}}<br /> {{spaces|2|em}}{{math|{post-S1}}}{{spaces|3.6|em}}{{math|{pre-S2}}}

Meaning: If execution of {{math|Si}} in a state in which precondition {{math|pre-Si}} is true terminates, then upon termination, postcondition {{math|post-Si}} is true.

Now consider concurrent programming with shared variables. The specs of two (or more) processes {{math|S1}} and {{math|S2}} are given in terms of their pre- and post-conditions, and we assume that implementations of {{math|S1}} and {{math|S2}} are given that satisfy their specs. But when executing their implementations in parallel, since they share variables, a race condition can occur; one process changes a shared variable to a value that is not anticipated in the proof of the other process, so the other process does not work as intended.

Thus, Dijkstra's Principle of non-interference is violated.

In her PhD thesis of 1975 <ref name="OwickiThesis" /> in Computer Science, Cornell University, written under advisor David Gries, Susan Owicki developed the notion of ''interference freedom''. If processes {{math|S1}} and {{math|S2}} satisfy interference freedom, then their parallel execution will work as planned. Dijkstra called this work the first significant step toward applying Hoare logic to concurrent processes.<ref>{{Cite book |title = Selected Writings on Computing: A Personal Perspective |last = Dijkstra |first = Edsger W. |publisher = Springer-Verlag |year = 1982 |doi = |series = Monographs in Computer Science |isbn = 0387906525 |chapter = EWD 554: A personal summary of the Gries-Owicki Theory |pages = 188–199 }}</ref> To simplify discussions, we restrict attention to only two concurrent processes, although Owicki-Gries<ref name="Owicki-Gries" /><ref name="Owicki-Gries2" /> allows more.

==Interference freedom in terms of proof outlines== Owicki-Gries<ref name="Owicki-Gries" /><ref name="Owicki-Gries2" /> introduced the ''proof outline'' for a Hoare triple {{math|{P}S{Q}}}. It contains all details needed for a proof of correctness of{{math|{P}S{Q}}} using the axioms and inference rules of Hoare logic. (This work uses the assignment statement {{math|x:}}{{math|{{=}} e}}, {{math|if-then}} and {{math|if-then-else}} statements, and the {{math|while}} loop.) Hoare alluded to proof outlines in his early work; for interference freedom, it had to be formalized.

A proof outline for {{math|{P}S{Q}}} begins with precondition {{math|P}} and ends with postcondition {{math|Q}}. Two assertions within braces { and } appearing next to each other indicate that the first must imply the second.

Example: A proof outline for {{math|{P} S {Q}}} where {{math|S}} is:<br /> {{math|x}}{{math|:}}{{math|{{=}} a; '''if''' e '''then''' S1 '''else''' S2}}

{{spaces|2|em}}{{math|{P}}}<br /> {{spaces|2|em}}{{math|{P1[x/a]}}}<br /> {{spaces|2|em}}{{math|x}}{{math|:}}{{math|{{=}} a;}}<br /> {{spaces|2|em}}{{math|{P1}}}<br /> {{spaces|2|em}}{{math|'''if''' e '''then''' {P1 &and; e}}}<br /> {{spaces|17|em}}{{math|S1}}<br /> {{spaces|17|em}}{{math|{Q1}}}<br /> {{spaces|8|em}}{{math|'''else''' {P1 &and; ¬ e}}}<br /> {{spaces|17|em}}{{math|S2}}<br /> {{spaces|17|em}}{{math|{Q1}}}<br /> {{spaces|2|em}}{{math|{Q1}}}<br /> {{spaces|2|em}}{{math|{Q}}}

{{math|P ⇒ P1[x/a]}} must hold, where {{math|P1[x/a]}} stands for {{math|P1}} with every occurrence of {{math|x}} replaced by {{math|a}}. (In this example, {{math|S1}} and {{math|S2}} are basic statements, like an assignment statement, '''skip''', or an '''await''' statement.)

Each statement {{math|T}} in the proof outline is preceded by a precondition {{math|pre-T}} and followed by a postcondition {{math|post-T}}, and {{math|{pre-T}T{post-T}}} must be provable using some axiom or inference rule of Hoare logic. Thus, the proof outline contains all the information necessary to prove that {{math|{P}S{Q}}} is correct.

Now consider two processes {{math|S1}} and {{math|S2}} executing in parallel, and their specs:

{{spaces|2|em}}{{math|{pre-S1}}}{{spaces|5.5|em}}{{math|{pre-S2}}}<br />{{spaces|2|em}}{{math|S1}}{{spaces|15|em}}{{math|S2}}<br />{{spaces|2|em}}{{math|{post-S1}}}{{spaces|3.6|em}}{{math|{post-S2}}}

Proving that they work suitably in parallel will require restricting them as follows. Each expression {{math|E}} in {{math|S1}} or {{math|S2}} may refer to at most one variable {{math|y}} that can be changed by the other process while {{math|E}} is being evaluated, and {{math|E}} may refer to {{math|y}} at most once. A similar restriction holds for assignment statements {{math|x:}}{{math|{{=}} E}}.

With this convention, the only indivisible action need be the memory reference. For example, suppose process {{math|S1}} references variable {{math|y}} while {{math|S2}} changes {{math|y}}. The value {{math|S1}} receives for {{math|y}} must be the value before or after {{math|S2}} changes {{math|y}}, and not some spurious in-between value.

'''Definition of Interference-free'''

The important innovation of Owicki-Gries was to define what it means for a statement {{math|T}} not to interfere with the ''proof'' of {{math|{P}S{Q}}}. If execution of {{math|T}} cannot falsify any assertion given in the proof outline of {{math|{P}S{Q}}}, then that proof still holds even in the face of concurrent execution of {{math|S}} and {{math|T}}.

'''Definition'''. Statement {{math|T}} with precondition {{math|pre-T}} does not interfere with the proof of {{math|{P}S{Q}}} if two conditions hold:

(1) {{math|{Q &and; pre-T} T {Q}}}<br />(2) Let {{math|S'}} be any statement within {{math|S}} but not within an {{math|await}} statement (see later section). Then {{math|{pre-S' &and; pre-T} T {pre-S'}}}.

Read the last Hoare triple like this: If the state is such that both {{math|T}} and {{math|S'}} can be executed, then execution of {{math|T}} is not going to falsify {{math|pre-S'}}.

'''Definition'''. Proof outlines for {{math|{P1}S1{Q1}}} and {{math|{P2}S2{Q2}}} are interference-free if the following holds. Let {{math|T}} be an {{math|await}} or assignment statement (that does not appear in an {{math|await}}) of process {{math|S1}}. Then {{math|T}} does not interfere with the proof of {{math|{P2}S2{Q2}}}. Similarly for {{math|T}} of process {{math|S2}} and {{math|{P1}S1{Q1}}}.

==Statements cobegin and await== Two statements were introduced to deal with concurrency. Execution of the statement {{math|'''cobegin''' S1 // S2 '''coend'''}} executes {{math|S1}} and {{math|S2}} in parallel. It terminates when both {{math|S1}} and {{math|S2}} have terminated.

Execution of the {{math|'''await'''}} statement {{math|'''await''' B '''then''' S}} is delayed until condition {{math|B}} is true. Then, statement {{math|S}} is executed as an indivisible action—evaluation of {{math|B}} is part of that indivisible action. If two processes are waiting for the same condition {{math|B}}, when it becomes true, one of them continues waiting while the other proceeds.

The {{math|'''await'''}} statement cannot be implemented efficiently and is not proposed to be inserted into the programming language. Rather it provides a means of representing several standard primitives such as semaphores—first express the semaphore operations as {{math|'''await'''s}}, then apply the techniques described here.

Inference rules for {{math|'''await'''}} and {{math|'''cobegin'''}} are:

{{math|'''await'''}}<br />{{math|{{sfrac|{P &and; B} S {Q}|{P} '''await''' B '''then''' S {Q} }}}}<br /><br />{{math|'''cobegin'''}} <br />{{math|{{sfrac|{P1} S1 {Q1}, {P2} S2 {Q2}<br />interference-free|{P1&and;P2} '''cobegin''' S1//S2 '''coend''' {Q1&and;Q2} }}}}

==Auxiliary variables== An ''auxiliary variable'' does not occur in the program but is introduced in the proof of correctness to make reasoning simpler —or even possible. Auxiliary variables are used only in assignments to auxiliary variables, so their introduction neither alters the program for any input nor affects the values of program variables. Typically, they are used either as program counters or to record histories of a computation.

'''Definition'''. Let {{math|AV}} be a set of variables that appear in {{math|S'}} only in assignments {{math|x:}}{{math|{{=}} E}}, where {{math|x}} is in {{math|AV}}. Then {{math|AV}} is an ''auxiliary variable set'' for {{math|S'}}.

Since a set {{math|AV}} of auxiliary variables is used only in assignments to variables in {{math|AV}}, deleting all assignments to them doesn't change the program's correctness, and we have the inference rule {{math|AV}} elimination:

{{spaces|2|em}}{{math|{{sfrac|{P} S' {Q}|{P} S {Q} }}}}

{{math|AV}} is an auxiliary variable set for {{math|S'}}. The variables in {{math|AV}} do not occur in {{math|P}} or {{math|Q}}. {{math|S}} is obtained from {{math|S'}} by deleting all assignments to the variables in {{math|AV}}.

Instead of using auxiliary variables, one can introduce a program counter into the proof system, but that adds complexity to the proof system.

'''Note:''' Apt <ref name="AprRecursiveAssertions">{{Cite journal |last1=Apt |first1=Krzysztof R. |title=Recursive assertions and parallel programs |journal=Acta Informatica |volume=15 |pages=219&ndash;232 |date=June 1981 |issue=3 |url=https://doi.org/10.1007/BF00289262 |doi=10.1007/BF00289262 |s2cid=42470032 }}</ref> discusses the Owicki-Gries logic in the context of ''recursive'' assertions, that is,''effectively computable'' assertions. He proves that all the assertions in proof outlines can be recursive, but that this is no longer the case if auxiliary variables are used only as program counters and not to record histories of computation. Lamport, in his similar work,<ref name="LamportFreedom" /> uses assertions about token positions instead of auxiliary variables, where a token on an edge of a flow chart is akin to a program counter. There is no notion of a history variable. This indicates that Owicki-Gries's and Lamport's approaches are not equivalent when restricted to recursive assertions.

==Deadlock and termination== Owicki-Gries<ref name="Owicki-Gries" /><ref name="Owicki-Gries2" /> deals mainly with partial correctness: {{math|{P} S {Q}}} means: If {{math|S}} executed in a state in which {{math|P}} is true terminates, then {{math|Q}} is true of the state upon termination.However, Owicki-Gries also gives some practical techniques that use information obtained from a partial correctness proof to derive other correctness properties, including freedom from deadlock, program termination, and mutual exclusion.

A program is in deadlock if all processes that have not terminated are executing {{math|'''await'''}} statements and none can proceed because their {{math|'''await'''}} conditions are false. Owicki-Gries provides conditions under which deadlock cannot occur.

Owicki-Gries presents an inference rule for total correctness of the '''while''' loop. It uses a bound function that decreases with each iteration and is positive as long as the loop condition is true. Apt ''et al'' <ref>{{Cite book |last1=Apt |first1=Krzysztof R. |author-link= |last2=de Boer |first2=Frank S. |author-link2= |last3=Olderog |first3=Ernst-Rüdiger |author-link3=Ernst-Rüdiger Olderog |chapter=Proving termination of parallel programs |editor1-last=Gries |editor1-first=D. |editor2-last=Feijen |editor2-first=W.H.J. |editor3-last=van Gasteren |editor3-first=A.J.M. |editor4-last=Misra |editor4-first=J. |date=1990 |pages=0&ndash;6 |title=Beauty is Our Business |series=Monographs in Computer Science |publisher=Springer Verlag |url=https://link.springer.com/book/10.1007/978-1-4612-4476-9 |location=New York|doi=10.1007/978-1-4612-4476-9 |isbn=978-1-4612-8792-6 |s2cid=24379938 }}</ref> show that this new inference rule does not satisfy interference freedom. The fact that the bound function is positive as long as the loop condition is true was not included in an interference test. They show two ways to rectify this mistake.

==A simple example== Consider the statement:{{indent|7}}{{math|{x{{=}}0} }}{{indent|7}}{{math|'''cobegin''' '''await''' '''true''' '''then''' x:}}{{math|{{=}} x+1}}{{indent|18}}// {{math|'''await''' '''true''' '''then''' x:}}{{math|{{=}} x+2}}{{indent|7}}{{math|'''coend'''}}{{indent|7}}{{math|{x{{=}}3} }}

The proof outline for it:

{{math|{x{{=}}0} }}<br />{{math|S: '''cobegin'''}}<br />{{math|{x{{=}}0} }}<br />{{math|{x{{=}}0 &or; x{{=}}2} }}<br />{{math|S1: '''await''' '''true''' '''then''' }}{{math|x}}{{math|:}}{{math|{{=}}}} {{math|x+1}}<br />{{math|{Q1: x{{=}}1 &or; x{{=}}3} }}<br />//<br />{{math|{x{{=}}0} }}<br />{{math|{x{{=}}0 &or; x{{=}}1} }}<br />{{math|S2: '''await''' '''true''' '''then''' }}{{math|x}}{{math|:}}{{math|{{=}}}} {{math|x+2}}<br />{{math|{Q2: x{{=}}2 &or; x{{=}}3} }}<br />{{math|'''coend'''}}<br />{{math|{(x{{=}}1 &or; x{{=}}3) &and; (x{{=}}2 &or; x{{=}}3)} }}<br />{{math|{x{{=}}3} }}

Proving that {{math|S1}} does not interfere with the proof of {{math|S2}} requires proving two Hoare triples:

(1) {{math|{(x{{=}}0 &or; x{{=}}2) &and; (x{{=}}0 &or; x{{=}}1} S1 {x{{=}}0 &or; x{{=}}1} }} {{indent|0}}(2) {{math|{(x{{=}}0 &or; x{{=}}2) &and; (x{{=}}2 &or; x{{=}}3} S1 {x{{=}}2 &or; x{{=}}3} }}

The precondition of (1) reduces to {{math|x{{=}}0}} and the precondition of (2) reduces to {{math|x{{=}}2}}. From this, it is easy to see that these Hoare triples hold. Two similar Hoare triples are required to show that {{math|S2}} does not interfere with the proof of {{math|S1}}.

Suppose {{math|S1}} is changed from the {{math|'''await'''}} statement to the assignment {{math|x:}}{{math|{{=}} x+1}}. Then the proof outline does not satisfy the requirements, because the assignment contains two occurrences of shared variable {{math|x}}. Indeed, the value of {{math|x}} after execution of the {{math|'''cobegin'''}} statement could be 2 or 3.

Suppose {{math|S1}} is changed to the {{math|'''await'''}} statement {{math|'''await''' '''true''' '''then''' x:}}{{math|{{=}} x+2}}, so it is the same as {{math|S2}}. After execution of {{math|S}}, {{math|x}} should be 4. To prove this, because the two assignments are the same, two auxiliary variables are needed, one to indicate whether {{math|S1}} has been executed; the other, whether {{math|S2}} has been executed. We leave the change in the proof outline to the reader.

==Examples of formally proved concurrent programs== '''A. Findpos'''. Write a program that finds the first positive element of an array (if there is one). One process checks all array elements at even positions of the array and terminates when it finds a positive value or when none is found. Similarly, the other process checks array elements at odd positions of the array. Thus, this example deals with '''while''' loops. It also has no {{math|'''await'''}} statements.

This example comes from Barry K. Rosen.<ref name="RosenChurchRosser">{{cite journal |last1= Rosen |first1= Barry K |date= 1976 |title= Correctness of parallel programs: The Church-Rosser Approach. |journal= Theoretical Computer Science |volume= 2 |issue= 2 |pages= 183–207 |doi= 10.1016/0304-3975(76)90032-3|doi-access= free }}</ref> The solution in Owicki-Gries,<ref name="Owicki-Gries" /> complete with program, proof outline, and discussion of interference freedom, takes less than two pages. Interference freedom is quite easy to check, since there is only one shared variable. In contrast, Rosen's article<ref name="RosenChurchRosser" /> uses {{math|Findpos}} as the single, running example in this 24-page paper.

An outline of both processes in a general environment:

{{spaces|0|em}}{{math|'''cobegin''' producer: ...}} <br /> {{spaces|5|em}}{{math|'''await''' in-out < N '''then''' '''skip''';}}<br /> {{spaces|5|em}}{{math|add: b[in '''mod''' N]:{{=}} next value;}}<br /> {{spaces|5|em}}{{math|markin:}} {{math|in:}}{{math|{{=}}}} {{math|in+1;}}<br /> {{spaces|5|em}}{{math|...}}<br /> {{spaces|2|em}}//<br /> {{spaces|5|em}}{{math|consumer: ...}}<br /> {{spaces|5|em}}{{math|'''await''' in-out > 0 '''then''' '''skip''';}}<br /> {{spaces|5|em}}{{math|remove:}} {{math|this value:{{=}}<br /> {{spaces|7|em}} b[out '''mod''' N];}}<br /> {{spaces|5|em}}{{math|markout:}} {{math|out:}}{{math|{{=}}}} {{math|out+1;}}<br /> . {{math|'''coend'''}}<br /> {{math|...}}

'''B. Bounded buffer consumer/producer problem'''. A producer process generates values and puts them into bounded buffer {{math|b}} of size {{math|N}}; a consumer process removes them. They proceed at variable rates. The producer must wait if buffer {{math|b}} is full; the consumer must wait if buffer {{math|b}} is empty. In Owicki-Gries,<ref name="Owicki-Gries" /> a solution in a general environment is shown; it is then embedded in a program that copies an array {{math|c[1..M]}} into an array {{math|d[1..M]}}.

This example exhibits a principle to reduce interference checks to a minimum: Place as much as possible in an assertion that is invariantly true everywhere in both processes. In this case the assertion is the definition of the bounded buffer and bounds on variables that indicate how many values have been added to and removed from the buffer. Besides buffer {{math|b}} itself, two shared variables record the number {{math|in}} of values added to the buffer and the number {{math|out}} removed from the buffer.

'''C. Implementing semaphores'''.In his article on the THE multiprogramming system,<ref name="DijkstraTHE" /> Dijkstra introduces the semaphore {{math|sem}} as a synchronization primitive: {{math|sem}} is an integer variable that can be referenced in only two ways, shown below; each is an indivisible operation:

'''1. {{math|P(sem)}}''': Decrease {{math|sem}} by 1. If now {{math|sem < 0}}, suspend the process and put it on a list of suspended processes associated with {{math|sem}}.

'''2. {{math|V(sem)}}''': Increase {{math|sem}} by 1. If now {{math|sem ≤ 0}}, remove one of the processes from the list of suspended processes associated with {{math|sem}}, so its dynamic progress is again permissible.

The implementation of {{math|P}} and {{math|V}} using {{math|'''await'''}} statements is:

{{spaces|0|em}}{{math|P(sem):}}<br /> {{spaces|6|em}}{{math|'''await''' '''true''' '''then'''}}<br /> {{spaces|10|em}}{{math|'''begin''' sem:}}{{math|{{=}}}}{{math| sem-1;}}<br /> {{spaces|14|em}}{{math|'''if''' sem < 0 '''then'''}}<br /> {{spaces|16|em}}{{math|w[this process]:}}{{math|{{=}}}}{{math| '''true'''}}<br /> {{spaces|10|em}}{{math|'''end''';}}<br /> {{spaces|10|em}}{{math|'''await''' ¬w[this process]}}<br /> {{spaces|16|em}}{{math|'''then''' '''skip'''}}<br /> {{spaces|0|em}}<br /> {{spaces|0|em}}{{math|V(sem):}}<br /> {{spaces|6|em}}{{math|'''await''' '''true''' '''then'''}}<br /> {{spaces|10|em}}{{math|'''begin''' sem:}}{{math|{{=}}}}{{math| sem+1;}}<br /> {{spaces|14|em}}{{math|'''if''' sem ≤ 0 '''then'''}}<br /> {{spaces|17|em}}{{math|'''begin''' choose ''p'' such}}<br /> {{spaces|35|em}}{{math|that w[''p''];}}<br /> {{spaces|28|em}}{{math|w[''p'']:}}{{math|{{=}}}}{{math| '''false'''}}<br /> {{spaces|17|em}}{{math|'''end'''}}<br /> {{spaces|10|em}}{{math|'''end'''}}

Here, {{math|w}} is an array of processes that are waiting because they have been suspended; initially, {{math|w[p]}}{{math|{{=}}}}{{math|'''false'''}} for every process {{math|p}}. One could change the implementation to always waken the longest suspended process.

'''D. On-the-fly garbage collection'''. At the 1975 Summer School Marktoberdorf, Dijkstra discussed an on-the-fly garbage collector as an exercise in understanding parallelism. The data structure used in a conventional implementation of LISP is a directed graph in which each node has at most two outgoing edges, either of which may be missing: an outgoing left edge and an outgoing right edge. All nodes of the graph must be reachable from a known root. Changing a node may result in unreachable nodes, which can no longer be used and are called ''garbage''. An on-the-fly garbage collector has two processes: the program itself and a garbage collector, whose task is to identify garbage nodes and put them on a free list so that they can be used again.

Gries felt that interference freedom could be used to prove the on-the-fly garbage collector correct. With help from Dijkstra and Hoare, he was able to give a presentation at the end of the Summer School, which resulted in an article in CACM.<ref name="GriesGarbageCollection">{{Cite journal |last1=Gries |first1=David |authorlink1=David Gries |title=An exercise in proving parallel programs correct |doi=10.1145/359897.359903 |journal=Communications of the ACM |volume=20 |issue=12 |pages=921&ndash;930 |date=December 1977 |s2cid=3202388 |doi-access=free }}</ref>

'''E. Verification of readers/writers solution with semaphores'''. Courtois et. al.<ref name="CourtoisEtAl">{{Cite journal |last1=Courtois |first1=P.J. |last2=Heymans |first2=F. |last3=Parnas |first3=D.L. |authorlink3=David Parnas |title=Concurrent control with "readers" and "writers" |doi=10.1145/362759.362813 |journal=Communications of the ACM |volume=14 |issue=10 |pages=667&ndash;668 |date=October 1971 |s2cid=7540747 |doi-access=free }}</ref> use semaphores to give two versions of the readers/writers problem, without proof. Write operations block both reads and writes, but read operations can occur in parallel. Owicki<ref>{{cite tech report |last=Owicki |first=Susan |authorlink=Susan Owicki |title=Verifying concurrent programs with shared data classes |number=147 |publisher=Digital Systems Laboratory, Stanford University |date=August 1977 |url=http://i.stanford.edu/pub/cstr/reports/csl/tr/77/147/CSL-TR-77-147.pdf |access-date=2022-07-08}}</ref> provides a proof.

'''F. Peterson's algorithm''', a solution to the 2-process mutual exclusion problem, was published by Peterson in a 2-page article.<ref>{{Cite journal |last1=Peterson |first1=Gary L. |title=Myths about the mutual exclusion problem |journal=IPL |volume=12 |issue=3 |pages=115&ndash;116 |date=June 1981 |url=https://dx.doi.org/10.1016/0020-0190%2881%2990106-X |doi=10.1016/0020-0190(81)90106-X |url-access=subscription }}</ref> Schneider and Andrews provide a correctness proof.<ref>{{Cite conference |last1=Schneider |first1=Fred B. |authorlink1=Fred B. Schneider |last2=Andrews |first2=Gregory R. |title=Concepts for concurrent programming |pages=669&ndash;716 |date=1986 |book-title=Current Trends in Concurrency |series=Lecture Notes in Computer Science |editor1=J.W. Bakker |editor2=W.P. de Roever |editor3=G. Rozenberg |volume=224 |location=Noordwijkerhout, the Netherlands |publisher=Springer Verlag |doi=10.1007/BFb0027049 |isbn=978-3-540-16488-3 |url=https://doi.org/10.1007/BFb0027049 |url-access=subscription }}</ref>

==Dependencies on interference freedom== The image below, by Ilya Sergey, depicts the flow of ideas that have been implemented in logics that deal with concurrency. At the root is interference freedom. The file {{Citation | url = https://ilyasergey.net/assets/other/CSL-Family-Tree.pdf | title = CSL-Family-Tree | ref = none }} contains references. Below, we summarize the major advances.

center|550px|Historical graph of program logics for interference freedom

* '''Rely-Guarantee'''. 1981. Interference freedom is not compositional. Cliff Jones<ref>{{Cite thesis |last=Jones |first=C.B. |title=Development Methods for Computer Programs including a Notion of Interference |date=June 1981 |degree=DPhil |publisher=Oxford University |url=http://www.cs.ox.ac.uk/files/9025/PRG-25.pdf |doi=}}</ref><ref>{{cite conference |title= Specification and design of (parallel) programs |first1=Cliff B. |last1=Jones |author-link1= Cliff Jones (computer scientist) |year=1983 |conference=9th IFIP World Computer Congress (Information Processing 83) |editor= R.E.A. Mason |publisher=North-Holland/IFIP |pages=321–332 |isbn=0444867295 }}</ref> recovers compositionality by abstracting interference into two new predicates in a spec: a rely-condition records what interference a thread must be able to tolerate and a guarantee-condition sets an upper bound on the interference that the thread can inflict on its sibling threads. Xu ''et al'' <ref name="XudeRoeverHe">{{Cite journal |last1=Xu |first1=Qiwen |last2=de Roever |first2=Willem-Paul |last3=He |first3=Jifeng |title=The Rely-Guarantee method for verifying shared variable concurrent programs |doi=10.1007/BF01211617 |journal=Formal Aspects of Computing |volume=9 |pages=149&ndash;174 |date=1997 |issue=2 |s2cid=12148448 |doi-access=free }}</ref> observe that Rely-Guarantee is a reformulation of interference freedom; revealing the connection between these two methods, they say, offers a deep understanding about verification of shared variable programs. * '''CSL'''. 2004. Separation logic supports local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component. Concurrent separation logic (CSL) was originally proposed by Peter O'Hearn,<ref name="O'HearnCLS">{{cite conference | url = https://link.springer.com/book/10.1007/b100113 | title = Resources, Concurrency and Local Reasoning | first = Peter W. | last = O'Hearn | author-link = Peter O'Hearn | date = 2004-09-03 | conference = CONCUR 2004 | editor1 = P. Gardner | editor2 = N. Yoshida | volume = | edition = | book-title = CONCUR 2004 -- Concurrency Theory | publisher = Springer Verlag Berlin, Heidelberg | location = London, UK | pages = 49&ndash;67 | isbn = 978-3-540-28644-8 | doi = 10.1007/b100113 | access-date = 2022-07-06| url-access = subscription }}</ref><ref>{{cite journal|last1=O'Hearn|first1=Peter|title=Resources, Concurrency and Local Reasoning|journal=Theoretical Computer Science|date=2007|volume=375|issue=1–3|pages=271–307|doi=10.1016/j.tcs.2006.12.035|url=http://www.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf|doi-access=free}}</ref> We quote from:<ref name="O'HearnCLS" /> "the Owicki-Gries method<ref name="Owicki-Gries" /> involves explicit checking of non-interference between program components, while our system rules out interference in an implicit way, by the nature of the way that proofs are constructed." * '''Deriving concurrent programs'''. 2005-2007. Feijen and van Gasteren<ref name="GasterenFeijen" /> show how to use Owicki-Gries to design concurrent programs, but the lack of a theory of progress means that designs are driven only by safety requirements. Dongol, Goldson, Mooij, and Hayes have extended this work to include a "logic of progress" based on Chandy and Misra's language Unity, molded to fit a sequential programming model. Dongel and Goldson<ref>{{cite journal | url = https://doi.org/10.2168%2Flmcs-2%281%3A6%292006 | title = Extending the theory of Owicki and Gries with a logic of progress | last1 = Dongol | first1 = Brijesh | last2 = Goldson | first2 = Doug | journal = Logical Methods in Computer Science | year = 2006 | volume = 2 | article-number = 2260 | orig-date = January 12, 2005 | publisher = Centre pour la Communication Scientifique Directe (CCSD) | arxiv = cs/0512012v3 | doi = 10.2168/lmcs-2(1:6)2006 | s2cid = 302420 | access-date = | url-status =}}</ref> describe their logic of progress. Goldson and Dongol<ref>{{Cite conference |url=https://dl.acm.org/doi/pdf/10.5555/1082260.1082265 |last1=Goldson |first1=Doug |last2=Dongol |first2=Brijesh |title=Concurrent Program Design in the Extended Theory of Owicki and Gries |pages=41–50 |date=January 2005 |book-title=CATS '05: Proc 2005 Australasian Symp on Theory of Computing |editor1=Mike Atkinson |editor2=Frank Dehne |volume=41 |publisher=Australian Computer Society, Inc. |doi= |isbn= }}</ref> show how this logic is used to improve the process of designing programs, using Dekker's algorithm for two processes as an example. Dongol and Mooij<ref>{{Cite conference |url=https://link.springer.com/content/pdf/10.1007/11783596_11 |last2=Mooij |first2=Arjan J |last1=Dongol |first1=Brijesh |title=Progress in deriving concurrent programs: emphasizing the role of stable guards |pages=14–161 |date=July 2006 |book-title=MPC'06: Proc. 8th Int. Conf. on Mathematics of Program Construction |editor1=Tarmo Uustalu |volume=41 |publisher=Springer Verlag, Berlin, Heidelberg |location=Kuressaare, Estonia |doi=10.1007/11783596_11 |isbn= |url-access=subscription }}</ref> present more techniques for deriving programs, using Peterson's mutual exclusion algorithm as one example. Dongol and Mooij<ref>{{cite journal |last1=Dongol |first1=Brijesh |last2= Mooij|first2=Arjan J |date=2008 |title=Streamlining progress-based derivations of concurrent program |journal=Formal Aspects of Computing |volume=20 |issue= 2 |pages= 141–160 |doi=10.1007/s00165-007-0037-4 |s2cid=7024064 |doi-access=free }}</ref> show how to reduce the calculational overhead in formal proofs and derivations and derive Dekker's algorithm again, leading to some new and simpler variants of the algorithm. Mooij<ref>{{Cite conference |url= |last1=Mooij |first1=Arjan J. |title=Calculating and composing progress properties in terms of the leads-to relation |pages=366–386 |date=November 2007 |book-title=ICFEM'07: Proc. Formal Engineering Methods 9th Int. Conf. on Formal Methods and Software Engineering |editor1=Michael Butler |editor2=Michael G. Hinchey |editor3=María M. Larrondo-Petrie |location=Boca Raton, Florida |volume= |publisher=Springer Verlag, Berlin, Heidelberg |doi= |isbn=978-3540766483 }}</ref> studies calculational rules for Unity's ''leads-to'' relation. Finally, Dongol and Hayes<ref>{{cite tech report |last1=Dongol |first1=Brijesh |last2=Hayes |first2=Ian |date=April 2007 |url=https://core.ac.uk/download/pdf/14986002.pdf |title=Trace semantics for the Owicki-Gries theory integrated with the progress logic from UNITY |institution=University of Queensland |number=SSE-2007-02}}</ref> provide a theoretical basis for and prove soundness of the process logic. * '''OGRA'''. 2015. Lahav and Vafeiadis strengthen the interference freedom check to produce (we quote from the abstract) "OGRA, a program logic that is sound for reasoning about programs in the release-acquire fragment of the C11 memory model." They provide several examples of its use, including an implementation of the RCU synchronization primitives.<ref>{{cite conference |url=https://link.springer.com/chapter/10.1007/978-3-662-47666-6_25 |title= Owicki-Gries reasoning for weak memory models |first1=Ori |last1=Lahav |first2=Viktor |last2=Vafeiadis |year=2015 |conference=ICALP 2015 |editor1=Halldórsson, M. |editor2=Iwama, K. |editor3=Kobayashi, N. |editor4=Speckmann, B. |volume=9135 |book-title=Automata, Languages, and Programming. ICALP 2015 |series=Lecture Notes in Computer Science |publisher=Springer |location=Berlin, Heidelberg |pages=311&ndash;323 |doi=10.1007/978-3-662-47666-6_25|url-access=subscription }}</ref> *'''Quantum programming'''. 2018. Ying ''et al'' <ref>{{cite arXiv |last1=Ying |first1=Mingsheng |last2=Zhou |first2=Li |last3=Li |first3=Yangjia |title=Reasoning about Parallel Quantum Programs |date=2018 |class=cs.LO |eprint=1810.11334}}</ref> extend interference freedom to quantum programming. Difficulties they face include intertwined nondeterminism: nondeterminism involving quantum measurements and nondeterminism introduced by parallelism occurring at the same time. The authors formally verify Bravyi-Gosset-König's parallel quantum algorithm solving a linear algebra problem, giving, they say, for the first time an unconditional proof of a computational quantum advantage. *'''POG'''. 2020. Raad ''et al'' present POG (Persistent Owicki-Gries), the first program logic for reasoning about non-volatile memory technologies, specifically the Intel-x86.<ref>{{Cite conference |last1=Raad |first1=Azalea |last2=Lahav |first2=Ori |last3=Vafeiadis |first3=Viktor |title=Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86 |date=13 November 2020 |book-title=Proceedings of the ACM on Programming Languages |volume=4 |issue=OOPSLA |pages=1&ndash;28 |publisher=ACM |doi=10.1145/3428219 |doi-access=free |hdl=10044/1/97398 |hdl-access=free }}</ref>

==Texts that discuss interference freedom==

* ''On A Method of Multiprogramming'', 1999.<ref name="GasterenFeijen">{{cite book |last1= Van Gasteren |first1= A.J.M. |last2= Feijen |first2= W.H.J. |editor-last1=Gries |editor-first1=David |editor-link1= David Gries |editor-last2=Schneider |editor-first2=Fred B. |editor-link2=Fred B. Schneider |year=1999 |title=On A Method Of Multiprogramming |series=Monographs in Computer Science |publisher=Springer-Verlag New York Inc. |pages=370 |doi=10.1007/978-1-4757-3126-2 |isbn=978-1-4757-3126-2|s2cid= 13607884 }}</ref> Van Gasteren and Feijen discuss the formal development of concurrent programs entirely on the idea of interference freedom. * ''On Current Programming'', 1997.<ref>{{cite book |last1= Schneider |first1= Fred B. |author-link1= Fred B. Schneider |editor-last1=Gries |editor-first1=David |editor-link1= David Gries |editor-last2=Schneider |editor-first2=Fred B. |editor-link2=Fred B. Schneider |year=1997 |title=On Concurrent Programming |series=Graduate Texts in Computer Science |publisher=Springer-Verlag New York Inc. |doi=10.1007/978-1-4612-1830-2 |isbn=978-1-4612-1830-2|s2cid= 9980317 }}</ref> Schneider uses interference freedom as the main tool in developing and proving concurrent programs. A connection to temporal logic is given, so arbitrary safety and liveness properties can be proven. Control predicates obviate the need for auxiliary variables for reasoning about program counters. * ''Verification of Sequential and Concurrent Programs'', 1991,<ref>{{cite book |last1= Apt |first1= Krzysztof R. |author-link1= |last2= Olderog |first2= Ernst-Rüdiger |editor-last1=Gries |editor-first1=David |editor-link1= David Gries |year=1991 |title=Verification of Sequential and Concurrent Programs |series=Texts in Computer Science |publisher=Springer-Verlag Germany }}</ref> 2009.<ref name="AptThirdEdition">{{cite book |last1= Apt |first1= Krzysztof R. |author-link1= |last3= Olderog |first3= Ernst-Rüdiger |author-link3= |last2=Boer |first2=Frank S. |author-link2= |editor-last1=Gries |editor-first1=David |editor-link1= David Gries |editor-last2=Schneider |editor-first2=Fred B. |editor-link2=Fred B. Schneider |year=2009 |edition=3rd |title=Verification of Sequential and Concurrent Programs |series=Texts in Computer Science |publisher=Springer-Verlag London |pages=502 |url=http://link.springer.com/10.1007/978-1-84882-745-5 |doi=10.1007/978-1-84882-745-5 |bibcode= 2009vscp.book.....A |isbn=978-1-84882-744-8}}</ref> This first text to cover verification of structured concurrent programs, by Apt ''et al'', has gone through several editions over several decades. * ''Concurrency Verification: Introduction to Compositional and Non-Compositional Methods'', 2112.<ref>{{cite book |last1= de Roever |first1= Willem-Paul |last2= de Boer |first2= Willem-Paul |last3= Hanneman |first3= Ulrich |last4= Hooman |first4= Jozef |last5= Lakhnech |first5= Yassine |last6= Poel |first6= Mannes |last7= Zwiers |first7= Job |editor-last1=Abramsky |editor-first1=S. |year=2012 |pages=800 |title=Concurrency Verification: Introduction to Compositional and Non-Compositional Methods |series=Cambridge Tracts in Theoretical Computer Science |publisher=Cambridge University Press USA |isbn=978-0521169325}}</ref> De Roever ''et al'' provide a systematic and comprehensive introduction to compositional and non-compositional proof methods for the state-based verification of concurrent programs

==Implementations of interference freedom==

* 1999: Nipkow and Nieto present the first formalization of interference freedom and its compositional version, the rely-guarantee method, in a theorem prover: Isabelle/HOL.<ref>{{Cite thesis |last=Nieto |first=Leonor Prensa |title=Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL |date=2002-01-31 |degree=Dr. rer. nat. |publisher=Technischen Universitaet Muenchen |type= PhD thesis |url=http://tumb1.biblio.tu-muenchen.de/publ/diss/allgemein.html |pages=198 |access-date=2022-07-05 }}</ref><ref>{{Cite conference |last1=Nipkow |first1=Tobias |last2=Nieto |first2=Leonor Prensa |title=Owicki/Gries in Isabelle/HOL |volume=1577 |conference=FASE 1999 |book-title=Fundamental Approaches to Software Engineering |editor=J.P. Finance |publisher=Springer Verlag |location=Berlin Heidelberg |series=Lecture Notes in Computer Science |date=1999-03-22 |pages=188&ndash;203 |isbn=978-3-540-49020-3 |doi=10.1007/978-3-540-49020-3_13|doi-access=free }}</ref> * 2005: Ábrahám's PhD thesis provides a way to prove multithreaded Java programs correct in three steps: (1) Annotate the program to produce a proof outline, (2) Use their tool ''Verger'' to automatically create verification conditions, and (3) Use the theorem prover PVS to prove the verification conditions interactively.<ref>{{Cite thesis |last=Ábrahám |first=Erika |title=An Assertional Proof System for Multithreaded Java - Theory and Tool Support |date=2005-01-20 |degree=PhD |publisher=Universiteit Leiden |type= PhD thesis |url=https://hdl.handle.net/1887/584 |pages=220 |hdl=1887/584 |access-date=2022-07-05 |isbn=9090189084}}</ref><ref>{{cite journal |last1=Ábrahám |first1=Erika |last2=Boer |first2=Frank, S., de |last3=Roever |first3=Willem-Paul, de |last4=Martin |first4=Steffen |title=An assertion-based proof system for multithreaded Java |journal=Theoretical Computer Science |publisher=Elsevier |volume=331 |date=2005-02-25 |issue=2–3 |pages=251&ndash;290 |doi=10.1016/j.tcs.2004.09.019|doi-access=free }} </ref> * 2017: Denissen<ref>{{Cite thesis |last=Denissen |first=P.E.J.G |title=Extending Dafny to Concurrency: Owicki-Gries style program verification for the Dafny program verifier |date=November 2017 |degree=Masters |publisher=Eindhoven University of Technology |url=https://research.tue.nl/en/studentTheses/extending-dafny-to-concurrency}}</ref> reports on an implementation of Owicki-Gries in the "verification ready" programming language Dafny.<ref>{{cite web |url=https://dafny.org |title=Dafny Programming Language |access-date=2022-07-20}}</ref> Denissen remarks on the ease of use of Dafny and his extension to it, making it extremely suitable when teaching students about interference freedom. Its simplicity and intuitiveness outweighs the drawback of being non-compositional. He lists some twenty institutions that teach interference freedom. * 2017: Amani ''et al'' combine the approaches of Hoare-Parallel, a formalisation of Owicki-Gries in Isabelle/HOL for a simple while-language, and SIMPL, a generic language embedded in Isabelle/HOL, to allow formal reasoning on C programs.<ref>{{cite conference | url = http://dx.doi.org/10.1145/3018610.3018627 | title = COMPLX: A verification framework for concurrent imperative programs | first1 = S. | last1 = Amani | first2 = J. | last2 = Andronick | first3 = M. | last3 = Bortin | first4 = C. | last4 = Lewis | first5 = C. | last5 = Rizkallah | first6 = J. | last6 = Tuong | date = 16 January 2017 | conference = CPP 2017: Proc 6th ACM SIGPLAN Conference on Certified Programs and Proof | editor1 = Yves Bertot | editor2 = Viktor Vafeiadid | publisher = ACM | location = Paris, France | pages = 138&ndash;150 | isbn = 978-1-4503-4705-1 | doi = 10.1145/3018610.3018627| url-access = subscription }}</ref> * 2022: Dalvandi ''et al'' introduce the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs, building on Nipkow and Nieto's encoding of Owicki–Gries in the Isabelle theorem prover.<ref name="DalvandiEtAl">{{Cite journal |last1=Dalvandi |first1=Sadegh |last2=Dongol |first2=Brijesh |last3=Doherty |first3=Simon |last4=Wehrheim |first4=Heike |title=Integrating Owicki–Gries for C11-Style memory models into Isabelle/HOL |doi=10.1007/s10817-021-09610-2 |journal=Journal of Automated Reasoning |volume=66 |pages=141&ndash;171 |date=February 2022 |s2cid=215238874 |doi-access=free |arxiv=2004.02983 }}</ref> * 2022: This webpage <ref>{{cite web |url=https://civl-verifier.github.io |title=Civl: A verifier for concurrent programs |access-date=2022-07-22}}</ref> describes the Civl verifier for concurrent programs and gives instructions for installing it on your computer. It is built on top of Boogie, a verifier for sequential programs. Kragl et al <ref>{{Cite conference |last1=Kragl |first1=Bernhard |last2=Qadeer |first2=Shaz |last3=Henzinger |first3=Thomas A. |title=Refinement for structured concurrent programs |date=2020 |book-title=CAV 2020: Computer Aided Verification |series=Lecture Notes in Computer Science |editor1=S. Lahiri |editor2=C. Wang |volume=12224 |publisher=Springer Verlag |doi=10.1007/978-3-030-53288-8_14 |isbn=978-3-030-53288-8 |doi-access=free }}</ref> describe how interference freedom is achieved in Civl using their new specification idiom, ''yield invariants''. One can also use specs in the rely-guarantee style. Civl offers a combination of linear typing and logic that allows economical and local reasoning about disjointness (like separation logic). Civl is the first system that offers refinement reasoning on structured concurrent programs. * 2022. Esen and Rümmer developed TRICERA,<ref>{{Cite conference |last1=Esen |first1=Zafer |last2=Rümmer |first2=Philipp |title=TRICERA Verifying C Programs Using the Theory of Heaps |date=October 2022 |book-title=Proc. 22nd Conf. on Formal Methods in Computer-Aided Design – FMCAD 2022 |editor1=A. Griggio |editor2=N. Rungta |volume= |issue= |pages=360&ndash;391 |publisher=TU Wien Academic Press |doi=10.34727/2022/isbn.978-3-85448-053-2_45 |doi-access=free }}</ref> an automated open-source verification tool for C programs. It is based on the concept of constrained Horn clauses, and it handles programs operating on the heap using a theory of heaps. A web interface to try it online is available. To handle concurrency, TRICERA uses a variant of the Owicki-Gries proof rules, with explicit variables to added to represent time and clocks.

==References== {{Reflist}}

Category:Formal methods Category:Program logic Category:Logic in computer science