Concurrency and transactional memory in Dafny

In course

Qui quis fugiat sit occaecat excepteur adipisicing. Magna officia mollit sunt aute eiusmod nulla eiusmod sint dolore Lorem deserunt consequat labore ea. Aliqua sint anim est pariatur velit reprehenderit dolor ea anim aute culpa. Culpa in aliqua ex cillum aliqua dolore fugiat.

Description

This lecture introduces Dafny, a compiled language designed for formal verification, ensuring correct code execution without runtime errors. It covers modeling concurrency, safety rules, liveness properties, and transactional memory concepts. The instructor presents examples and papers on concurrency and transactional memory, emphasizing formal verification and advanced algorithm creation.

Instructor

sit aliquip elit

Ex officia exercitation aliqua anim. Anim exercitation excepteur duis officia laboris fugiat enim. Eu eiusmod exercitation non et esse laboris adipisicing aliquip Lorem qui proident ullamco minim. Incididunt deserunt aute est elit laborum reprehenderit Lorem duis exercitation sit. Ipsum proident aute eu voluptate ex laborum aute eiusmod veniam velit. Do aliquip qui proident incididunt consequat. Cupidatat nostrud et consectetur pariatur ullamco.

Official source

https://mediaspace.epfl.ch/media/0_wfzxzowz

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Ontological neighbourhood

Computer engineering

High-performance computing: Distributed computing

Related lectures (33)