Parameterized Verification of Deterministic MPI Programs

Stephen F. Siegel

REVIEW 3 major objections 5 minor 26 references

Parameterized Verification of Deterministic MPI Programs

T0 review · 3 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that deterministic MPI programs can be verified for all process counts by transforming them into sequential programs checked with standard deductive tools.

desk verdict The transformation idea is real and the artifact is strong, but the five verified C/MPI claims rest on an unproved synchronous variant that the paper waves through with 'everything goes as before.' read the letter →

arxiv 2607.18049 v1 pith:Q3EPFWBE submitted 2026-07-20 cs.PL cs.LO

Stephen F. Siegel This is my paper · ORCID

classification cs.PLcs.LO

keywords MPIparameterizedverificationdeductivemessage-passingprogramshappens-beforesequentialtransformationdeterministicconcurrencysoundnesstheorem

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Parameterized verification asks whether a message-passing program is correct for every possible number of processes, not just one fixed small count. This paper claims that for deterministic programs — those where each receive names a single sender — the question can be reduced to verifying an ordinary sequential program. The reduction uses four user-supplied functions: the number of messages from each sender to each receiver, the level of each communication event in the happens-before order, and a predicate describing the content of each message. If the resulting sequential program passes a standard deductive verifier, the paper proves the original parallel program is deadlock-free, assertion-safe, terminating, and functionally correct for any process count. The claim is realized in a prototype tool that verified five C/MPI programs, including a diffusion simulation, without any bound on process number or input size.

What carries the argument

The load-bearing object is the transformation itself, parameterized by four universal user-supplied functions: the number of messages from each sender to each receiver; the property of the j-th message from s to d; and the levels of the j-th send and receive in the happens-before order. The transformation instruments send and receive with count arrays, replaces receives with invariant-constrained nondeterministic choice, asserts the invariant on sends, and maintains a level counter that must strictly increase at every communication step. The level mechanism converts acyclicity of the happens-before graph into finitely checkable sequential assertions; Theorem 1 states that correctness of the

What would settle it

Run any of the five verified programs under a model checker that models MPI's buffered implementation with finite channel capacity and adversarial scheduling; a deadlock, buffer overflow, or assertion violation at any process count would refute the synchronous-equivalence premise. Alternatively, search for a synchronous message-passing program whose transformed sequential program is correct yet the parallel program deadlocks, which would falsify the asserted synchronous soundness.

Watch

Extended reading notes

Core claim

The central discovery is a soundness theorem: given a message-passing program P and the sequential program S produced by the transformation, if S is correct then P is correct. The transformation replaces each send with an assertion that the message satisfies a user-supplied invariant, then increments a send count; each receive becomes a nondeterministic choice of any value satisfying the invariant for that channel position, then increments a receive count. A running level is required to strictly increase at every communication step, using user-supplied level functions, and a global check enforces that each send's level is below its matching receive's level — together these rule out cycles in

Load-bearing premise

The results for actual MPI programs rest on two premises that the paper states but does not prove here: MPI standard-mode point-to-point communication is equivalent to synchronous communication for the properties verified, and the synchronous version of the transformation is sound — if either premise fails, the five verified programs may still be incorrect for some process count.

Editorial extensions

If this is right

Deductive verification of parameterized message-passing programs becomes possible with off-the-shelf sequential program verifiers; no bound on the process count is needed.
The method is modular: procedures can be verified one at a time, and a procedure body can be split into communication-closed regions, each with its own specification.
Because the output is an ordinary sequential program, any verification technology that supports nondeterministic choice, assertions, and assumptions — model checkers, symbolic executors, or static analyzers — can potentially be used.
The five case studies suggest the annotation burden, while high (1.5–3.5 times the code size), is manageable and yields under-a-minute verification times.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The five case-study guarantees inherit two premises the paper does not prove: the equivalence of MPI standard-mode semantics to synchronous semantics, and the soundness of the synchronous variant of the transformation. A rigorous proof of either is a direct way to harden the approach.
The same sequentialization could be adapted to verify quantitative properties (such as interval bounds on accumulated sums) by choosing the message invariant accordingly; the paper hints at this but does not develop it.
A natural cross-check is to run the generated sequential programs of the five case studies under a bounded model checker for increasing process counts; agreement would corroborate the sequentialization, while any discrepancy would expose a gap in the transformation or its premises.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Core point: this is a genuine advance. The user supplies per-channel message counts, a message invariant, and level functions; the tool rewrites an MPI program into a sequential program whose correctness implies correctness for all process counts. That removes the process-count bound that limits finite-state model checking, and it improves on DafnyMPI by using a local per-channel view instead of demanding tag-based global order. Theorem 1 is proved for the asynchronous MPlite model, the appendix contains the argument, and the artifact is real: shipped code, prover output, reproducible VCs. The five case studies are legitimate deductive proofs, and the annotation burden is honestly reported.

The soft spot is the bridge from Theorem 1 to those case studies. All five verified programs use MPI_Sendrecv, which the paper treats under the synchronous semantics. That variant is not proved. Section 2.3.1 says 'Everything goes through as before,' but the changes are not cosmetic: the happens-before relation becomes one over matching pairs, the two level functions collapse into one, and the minimal-level deadlock argument in Appendix B depends on the inequality slevel < rlevel. With a single level function that argument needs a different justification, and the paper does not supply it. The sendrecv transformation in Section 2.3.1 even writes MAX(..., rlevel(...)) one line after rlevel has been eliminated. The artifact has a matching inconsistency: in the VM_sendrecv macro in Appendix C.6, line 194 passes src where dest is intended when computing the expected send count. These look like fixable typos, but they are symptoms that the synchronous case is not literally 'as before.' Since every case study depends on that unproved lemma plus the cited [21] MPI-to-synchronous equivalence, the paper's headline claim of complete proofs is stronger than the current text supports. The [21] part is prior published work, so that is fine; the gap is the synchronous transformation and the Sendrecv rule.

Proportion matters: the core asynchronous result appears sound, and the approach is likely salvageable as stated. But the case-study guarantees are conditional until the synchronous variant gets a real proof or the tool output is explicitly labeled experimental. I would send this to a serious referee — the idea and the artifact earn that — and the revision should either close the synchronous gap or soften the claim.

Referee Report

3 major / 5 minor

Summary. The paper presents a method and tool for parameterized verification of a deterministic subset of MPI programs. Users annotate a C/MPI program with universal functions nummsg, msginv, slevel (and related metadata functions) and a region-sequence specification; VMFC transforms the program into a sequential C program with ACSL annotations, which Frama-C/Wp then verifies. In an idealized asynchronous language MPlite, Theorem 1 states that correctness of the transformed sequential program implies correctness of the original message-passing program, and Appendix B gives a detailed proof. Section 2.3.1 extends the transformation to synchronous semantics and to a combined sendrecv statement, but this extension is asserted informally. The paper reports complete proofs of five C/MPI programs with no bounds on process counts, backed by a Zenodo artifact.

Significance. If the gaps are closed, the contribution is significant: parameterized, unbounded verification of real C/MPI programs is currently out of reach for most tools, and the level-function/region decomposition is a clean way to make acyclic happens-before and communication-closedness checkable by a sequential verifier. The machine-checked Frama-C proofs and the shipped artifact are concrete strengths, and the Appendix B proof is a serious formalization for the asynchronous model. The main weakness is that the case-study guarantees depend on an unproved synchronous variant and on VMFC macros whose listings contain errors.

major comments (3)

The synchronous-semantics variant is asserted, not proved. Theorem 1 and Appendix B cover only asynchronous MPlite with separate send/recv statements. Section 2.3.1 says 'Everything goes through as before,' but the modifications are substantive: only slevel is used, and sendrecv creates two events from one process that can complete in either order, so the transformed code checks both new levels against the old level and takes MAX. Appendix B's deadlock argument depends on two level functions and the inequality slevel<rlevel in Eq. (1), so it does not automatically transfer. All five case studies are C/MPI programs verified under the synchronous interpretation, and cycsum and diffuse1d use MPI_Sendrecv; hence the reported complete proofs rest on this missing lemma. Concretely, the sendrecv transformation at line 3 of §2.3.1 writes MAX(..., rlevel(...)) although rlevel is not defined in th
Appendix C.6 lists VMFC's VM_send and VM_sendrecv macros. In VM_send (lines ~165-182), `_mcount = VM_MCOUNT(fid, rid, src, VM_pid, _sc)` uses an undeclared identifier `src`; for a send the call should be `VM_MCOUNT(fid, rid, VM_pid, dest, _sc)`. The same wrong `src` argument appears in the send half of VM_sendrecv (line ~194). In addition, line ~217 writes `_rc[src]` where `_rc` is a scalar integer; the intended argument is `_rc`. These are not merely presentation typos: for programs with non-constant mcount or msgtag, the transformed code either fails to compile or checks the wrong message specification. The five case studies use mcount=1, which is why the artifact's VCs can still succeed, but the implementation as documented does not match the method of §2.
VMFC procedures can contain multiple internal/external regions, and the tool checks region sequence and resets sc/rc/level at boundaries (VM_Region_begin/end in Appendix C.6). However, no theorem states that correctness of each region's transformed sequential program plus the region-sequence/universality checks implies correctness of the whole parallel procedure. This compositionality is load-bearing for diffuse1d.c, which has NSTEP external regions inside a loop. Please provide a composition theorem or a precise invariant for region decomposition, or state the additional conditions under which per-region soundness composes.

minor comments (5)

In the sendrecv pseudo-code, line 3 should use `slevel` instead of `rlevel`. Also clarify that sendrecv is treated as an atomic combined event, so the two new-level checks are against the pre-statement level, not against each other.
The artifact description refers to 'Figure 8' for the code-line and annotation-line statistics, but the actual table is Figure 7. Please fix the cross-reference.
The abstract and introduction say the five programs are verified to 'compute the expected results'; §3.3 states that programs 1–3 use `-wp-model real`. The guarantees are therefore for real arithmetic, not IEEE floating-point. Please qualify the claim to avoid overstating floating-point correctness.
The clause "mpi universal tset(,tset)*;" appears malformed; it should describe a comma-separated list of tsets.
The new sendrecv statement should specify behavior when dest or source is out of range, given that ordinary send/recv are no-ops in that case.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: user-provided nummsg/msginv/levels are checked obligations; Theorem 1 is self-contained; the synchronous-variant gap is a soundness risk, not an equation-to-input reduction.

full rationale

The derivation chain is not circular. Theorem 1 is proved for asynchronous MPlite in Appendix B by a simulation argument: ghost variables sc/rc/level are added to the parallel program, the channel invariant is shown preserved, and deadlock-freedom follows from the minimal-new-level contradiction using Eq. (1). The user-supplied nummsg, msginv, and slevel/rlevel are not fitted outputs; they are checked obligations. The transformed program asserts msginv on every send, asserts nummsg/level conditions at region boundaries and SpecOK, so an incorrect user guess causes the sequential verification to fail rather than being silently converted into a prediction. The receive-side `choose x|msginv(...)` is an assume-guarantee step whose soundness is exactly what Theorem 1 proves (via the channel-invariant preservation), not a renaming of the target property. The one load-bearing self-citation, [21], justifies the synchronous/MPI semantics equivalence; it is prior published work with stated assumptions and parameter-free proofs, hence independent evidence rather than a self-citation chain. The manuscript's own limitation is that the synchronous variant in Sec. 2.3.1 is asserted ('Everything goes through as before...') but not proved: Appendix B covers only asynchronous MPlite, the sendrecv pseudo-code even references an undefined rlevel, and the VM_sendrecv macro (Appendix C.6) has a related src/sender inconsistency. That is a soundness gap in the C/MPI case-study claims, not a case of an equation reducing to its input, and therefore does not constitute circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numeric free parameters are fitted to data; the user-supplied functions are specifications checked by the transformation. The axioms are the deterministic subset, FIFO semantics, the cited MPI-synchronous equivalence, the unproved synchronous variant, and the soundness of the verification backend. The synchronous variant is the most fragile.

assumptions (5)

domain assumption Every receive operation specifies a single source (no MPI_ANY_SOURCE).
Used throughout Section 2; it makes the matching relation determined by per-process FIFO order, which is essential for defining message invariants and levels.
domain assumption MPlite channels are FIFO with unbounded buffers.
Defined in Section 2.1 and used in the channel invariant in Appendix B to justify that the j-th received message is the j-th sent one.
domain assumption MPI standard-mode blocking point-to-point semantics is equivalent to synchronous semantics for correctness (deadlock, assertion violations, termination).
Section 2.3.2 cites [21] for this equivalence. It is load-bearing for the tool's applicability to actual MPI programs, but not proved in this paper.
ad hoc to paper The synchronous-semantics variant of the transformation is sound.
Section 2.3.1 asserts 'Everything goes through as before' without a proof. This is the weakest point, since all case studies use MPI_Sendrecv under the synchronous interpretation.
domain assumption Frama-C/Wp and the automated provers (Alt-Ergo, Z3, CVC5) are sound.
Needed to interpret the discharged VCs as correctness proofs for the sequential transformed programs (Section 3.1.2).

how reviews work

0 comments

Cite this review

Pith. "Pith review of Parameterized Verification of Deterministic MPI Programs." pith.science (2026). https://pith.science/paper/Q3EPFWBE

@misc{pith2026260718049,
  author       = {Pith},
  title        = {Pith review of: Parameterized Verification of Deterministic MPI Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Q3EPFWBE}},
  note         = {Machine review of arXiv:2607.18049}
}

read the original abstract

We consider the problem of verifying a message passing program in which the number of processes is a parameter NP and each process knows its unique ID. Processes communicate using send and receive commands which specify a single destination or source. To verify the program, the user provides functions specifying the number of messages sent from process i to process j, the level of each communication event in the happens-before hierarchy, and a fact that holds for the k-th message sent from i to j. These are used to transform the program to a parameterized sequential program which can be verified using any techniques appropriate for such programs. We realize this approach in an extension to Frama-C/Wp to verify C/MPI programs.

Figures

Figures reproduced from arXiv: 2607.18049 by the authors.

**Figure 1.** MPlite syntax. ID is a set of identifiers. Expr is a set of deterministic side-effect-free expressions. The reserved parameter NP evaluates to the number of processes, and the reserved read-only variable pid returns the unique ID of this process. extended ACSL specifications into a sequential C program with ordinary ACSL specifications. This sequential program is then analyzed by Frama-C/Wp, which generates verific… view at source ↗

**Figure 3.** Information used to transform cycsum. 2.2 The transformation We now show how to transform an MPlite program to a sequential program in such a way that the correctness of the sequential program implies the correctness of the original program. The sequential language is the same as the parallel one, except there are no send or recv statements, and pid and NP are not reserved. The result of this transformation on cyc… view at source ↗

**Figure 5.** Contract for procedure sum in cycsum.c. 3.2 VMFC Procedure Contracts VMFC supports new classes of ACSL annotations, all of which begin with the keyword mpi. It includes a bespoke version of the header file mpi.h, which defines a number of primitives available in annotations. These are all prefixed by VM, and include VM_NP (the number of processes) and VM_pid (the process ID). VMFC takes a C/MPI program with these an… view at source ↗

Figures from the paper (2 more)

**Figure 6.** Figure 6: The begin region annotation for the MPI region of sum in cycsum.c. The user assigns an ID number (1) to the region. A procedure 𝑓 can have multiple regions, each with an ID unique within 𝑓 . This is followed by several universal function definitions, including nummsg, …

**Figure 7.** Figure 7: Statistics for proved C/MPI programs: number of [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 6 canonical work pages

[21]

Siegel and George S

Stephen F. Siegel and George S. Avrunin. 2005. Modeling wildcard-free MPI programs for verification. InProceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(Chicago, IL, USA)(PPoPP ’05). Association for Computing Machinery, New York, NY, USA, 95–106. doi:10.1145/ 1065944.1065957

arXiv 2005
[1]

Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. InTools and Algorithms for the Construction and An...

doi:10.1007/97 2022
[2]

Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, and Allan Blanchard. 2025. WP Plug-in Manual: Frama-C 32.0 (Germanium). https://frama- c.com/download/frama-c-wp-manual.pdf

2025
[3]

Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2025. ACSL: ANSI/ISO C Specifica- tion Language, Version 1.23. http://frama-c.com/download/acsl-1.23.pdf

2025
[4]

Allan Blanchard, François Bobot, Patrick Baudin, and Loïc Correnson. 2024. For- mally Verifying that a Program Does What It Should: The Wp Plug-in. InGuide to Software Verification with Frama-C: Core Components, Usages, and Applica- tions, Nikolai Kosmatov, Virgile Prevosto, and Julien Signoles (Eds.). Springer International Publishing, Cham, 187–261. doi...

work page doi:10.1007/978-3-031-55608-1_4 2024
[5]

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Sig- noles, and Boris Yakobowski. 2012. Frama-C — A Software Analysis Perspective. InSoftware Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings (LNCS, Vol. 7504), George Eleftherakis, Mike Hinchey, and Mik...

doi:10.1007/978-3-642-33826-7_16 2012
[6]

Retrieved April 8, 2026 from https://dafny.org

Dafny 2026.The Dafny Programming and Verification Language. Retrieved April 8, 2026 from https://dafny.org

2026
[7]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakr- ishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340. doi:10.1007/978-3-540-78800-3_24

doi:10.1007/978-3-540-78800-3_24 2008

Show all 26 references

[8]

Juergen Dingel. 2003. Computer-assisted assume/guarantee reasoning with VeriSoft. InProceedings of the 25th International Conference on Software Engineer- ing(Portland, Oregon)(ICSE ’03). IEEE Computer Society, Washington, DC, USA, 138–148. doi:10.1109/ICSE.2003.1201195

2003 arXiv
[9]

Aleksandr Fedchin, Antero Mejr, Hari Sundar, and Jeffrey S. Foster. 2026. DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Pro- grams.Proc. ACM Program. Lang.10, POPL, Article 63 (Jan. 2026), 27 pages. doi:10.1145/3776705

2026 doi
[10]

Dhriti Khanna, Subodh Sharma, César Rodríguez, and Rahul Purandare. 2018. Dynamic Symbolic Verification of MPI Programs. InFormal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedin...

2018 doi
[11]

2024.Guide to Software Verification with Frama-C

Nikolai Kosmatov, Virgile Prevosto, and Julien Signoles (Eds.). 2024.Guide to Software Verification with Frama-C. Springer, Cham. doi:10.1007/978-3-031- 55608-1

2024 doi
[12]

Rustan M

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, Berlin, Heidelberg, 348–370. doi:10.1007/978-3-642-17511-4_20

2010 doi
[13]

Rustan M

K. Rustan M. Leino, Peter Müller, and Jan Smans. 2010. Deadlock-Free chan- nels and locks. InProceedings of the 19th European Conference on Programming Languages and Systems (ESOP’10)(Paphos, Cyprus)(Lecture Notes in Computer Science, Vol. 6012). Springer-Verlag, Berlin, Heide...

2010 doi
[14]

López, Eduardo R

Hugo A. López, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2015. Protocol- based verification of message-passing parallel programs. InProceedings of the 2015 ACM SIGPLAN International Conference on Objec...

2015
[15]

Ziqing Luo and Stephen F. Siegel. 2024. Collective Contracts for Message-Passing Parallel Programs. InComputer Aided Verification (CA V 2024) (Lecture Notes in Computer Science, Vol. 14682), Arie Gurfinkel and Vijay Ganesh (Eds.). Springer, Cham, 44–68. doi:10.1007/978-3-031-65630-9_3

2024 doi
[16]

Message-Passing Interface Forum. 2025. MPI: A Message-Passing Interface Standard, Version 5.0. https://www.mpi-forum.org/docs/mpi-5.0/mpi50-report. pdf

2025
[17]

2026.Correctness for Scientific Computing Sys- tems ( CS2)

National Science Foundation. 2026.Correctness for Scientific Computing Sys- tems ( CS2). Retrieved January 26, 2026 from https://www.nsf.gov/funding/ opportunities/cs2-correctness-scientific-computing-systems

2026
[18]

2026.Alt-Ergo: An SMT Solver For Software Verification

OcamlPRO. 2026.Alt-Ergo: An SMT Solver For Software Verification. Retrieved January 24, 2026 from https://alt-ergo.ocamlpro.com

2026
[19]

Stephen F. Siegel. 2007. Model Checking Nonblocking MPI Programs. InVerifi- cation, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14–16, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4349), Byron Cook ...

2007 doi
[20]

Stephen F. Siegel. 2026.Artifact: Parameterized Verification of Deterministic MPI Programs. doi:10.5281/zenodo.21433793

2026 doi
[22]

Siegel and George S

Stephen F. Siegel and George S. Avrunin. 2007. Verification of Halting Properties for MPI Programs Using Nonblocking Operations. InRecent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User’s Group Meeting, Paris, France, September 30...

2007 doi
[23]

Siegel, Manchun Zheng, Ziqing Luo, Timothy K

Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, and Michael S. Rogers
[24]

Vasconcelos, Francisco Martins, Hugo-Andrés López, and Nobuko Yoshida

Vasco T. Vasconcelos, Francisco Martins, Hugo-Andrés López, and Nobuko Yoshida. 2022. A Type Discipline for Message Passing Parallel Programs.ACM Trans. Program. Lang. Syst.44, 4, Article 26 (Dec. 2022), 55 pages. doi:10.1145/ 3552519

2022
[25]

ghost state

Hengbiao Yu, Zhenbang Chen, Xianjin Fu, Ji Wang, Zhendong Su, Jun Sun, Chun Huang, and Wei Dong. 2020. Symbolic verification of message passing interface programs. InProceedings of the ACM/IEEE 42nd International Conference on Soft- ware Engineering(Seoul, South Korea)(ICSE ’2...

2020
[2015]

InSC15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis

CIVL: The Concurrency Intermediate Verification Language. InSC15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. ACM, New York. doi:10.1145/2807591.2807635 Article no. 61, pages 1–12

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.

[1] [21]

Siegel and George S

Stephen F. Siegel and George S. Avrunin. 2005. Modeling wildcard-free MPI programs for verification. InProceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(Chicago, IL, USA)(PPoPP ’05). Association for Computing Machinery, New York, NY, USA, 95–106. doi:10.1145/ 1065944.1065957

arXiv 2005

[2] [1]

Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. InTools and Algorithms for the Construction and An...

doi:10.1007/97 2022

[3] [2]

Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, and Allan Blanchard. 2025. WP Plug-in Manual: Frama-C 32.0 (Germanium). https://frama- c.com/download/frama-c-wp-manual.pdf

2025

[4] [3]

Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2025. ACSL: ANSI/ISO C Specifica- tion Language, Version 1.23. http://frama-c.com/download/acsl-1.23.pdf

2025

[5] [4]

Allan Blanchard, François Bobot, Patrick Baudin, and Loïc Correnson. 2024. For- mally Verifying that a Program Does What It Should: The Wp Plug-in. InGuide to Software Verification with Frama-C: Core Components, Usages, and Applica- tions, Nikolai Kosmatov, Virgile Prevosto, and Julien Signoles (Eds.). Springer International Publishing, Cham, 187–261. doi...

work page doi:10.1007/978-3-031-55608-1_4 2024

[6] [5]

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Sig- noles, and Boris Yakobowski. 2012. Frama-C — A Software Analysis Perspective. InSoftware Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings (LNCS, Vol. 7504), George Eleftherakis, Mike Hinchey, and Mik...

doi:10.1007/978-3-642-33826-7_16 2012

[7] [6]

Retrieved April 8, 2026 from https://dafny.org

Dafny 2026.The Dafny Programming and Verification Language. Retrieved April 8, 2026 from https://dafny.org

2026

[8] [7]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakr- ishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340. doi:10.1007/978-3-540-78800-3_24

doi:10.1007/978-3-540-78800-3_24 2008