English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The Message Passing Interface specification (MPI) defines a portablemessage-passing API used to program parallel computers. MPI programs manifest anumber of challenges on what concerns correctness: sent and expected values incommunications may not match, resulting in incorrect computations possiblyleading to crashes; and programs may deadlock resulting in wasted resources.Existing tools are not completely satisfactory: model-checking does not scalewith the number of processes; testing techniques wastes resources and arehighly dependent on the quality of the test set.  As an alternative, we present a prototype for a type-based approach toprogramming and verifying MPI like programs against protocols. Protocols arewritten in a dependent type language designed so as to capture the most commonprimitives in MPI, incorporating, in addition, a form of primitive recursionand collective choice. Protocols are then translated into Why3, a deductivesoftware verification tool. Source code, in turn, is written in WhyML, thelanguage of the Why3 platform, and checked against the protocol. Programs thatpass verification are guaranteed to be communication safe and free fromdeadlocks.  We verified several parallel programs from textbooks using our approach, andreport on the outcome.

Deductive Verification of Parallel Programs Using Why3