Loading presentation...

Present Remotely

Send the link below via email or IM


Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.


Verification of Erlang-style Concurrency

An overview of my current research: status and challenges. Joint work with Jonathan Kochems and Luke Ong.

Emanuele D'Osualdo

on 31 January 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Verification of Erlang-style Concurrency

Verification of Erlang-style Concurrency Emanuele D'Osualdo joint work with
Jonathan Kochems and Luke Ong emanuele.dosualdo@cs.ox.ac.uk University of Oxford Verification of Erlang-style Concurrency Shared Variables Message Passing No sharing of data
Asynchronous send
Blocking receive Challenges Recursion,
data, higher-order Unbounded message queues Unbounded
creation of processes Control Flow Analysis Counting Abstraction Soter Specifications Program-point reachability
Mutual exclusion
Bounds on mailboxes Analysis Petri Net Safe Unsafe Spurious trace? mjolnir.cs.ox.ac.uk/soter Compositionality Future directions Compositional analysis
Process Algebra
Behavioural Types
Analysis of FIFFO queues Emanuele D'Osualdo emanuele.dosualdo@cs.ox.ac.uk mjolnir.cs.ox.ac.uk/soter Surprisingly fast on single modules Whole program analysis
Full transcript