Nettsider med emneord «Verification»

Publisert 3. jan. 2019 13:29

The work of Bjørnar Luteberget, Koen Claessen (from Chalmers), and Christian Johansen (from PSY and ConSeRNS groups at IFI) won the Best Paper Award at the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), which was held in Texas, USA, in November 2018.

Publisert 1. des. 2014 08:23
Publisert 4. nov. 2010 14:12
Publisert 9. nov. 2010 10:47
Publisert 9. juni 2016 10:56

The work of Bjørnar Luteberget, Christian Johansen, and Martin Steffen (from PMA and ConSeRNS groups at IFI) won the Best Paper Award at the 12th International Conference on Integrated Formal Methods, which was held in Iceland in June.

Publisert 23. sep. 2016 13:45

by Lars Tveito

Real-time collaboration allows multiple users to view and edit a document simultaneously over a network. In this thesis, we develop a new protocol, called Shared Buffer, which enables real-time collaboration in existing editors. Shared Buffer leverages a client-server architecture and minimizes the implementation effort of the client-side algorithm. It achieves this without degrading the responsiveness of the editor.

The greatest challenge of a real-time collaborative system is ensuring consistency between the distributed copies of the document. We chose eventual consistency as the consistency model, which essentially states that if all users stop typing, then eventually they will look at the same document.

We apply a formal verification technique called model checking, using it as a tool to validate the protocol. The behavior of the system is formally specified in Maude, a language based on equational and rewriting logic. Linear Temporal Logic (LTL) is used to formalize the consistency model. Using the Maude LTL model checker, we have verified that the system exhibits eventual consistency for a limited number of clients and operations.

A Shared Buffer server has been implemented in Clojure, a modern functional language with strong support for concurrency. Client implementations have been developed as an extension for Emacs, a widely used text editor, and as a library for the Python programming language.

Publisert 27. sep. 2023 13:15

The task is to dependently typed programming for certification (especially in the area of security)

Publisert 4. nov. 2010 14:19
Publisert 25. aug. 2020 15:23
Publisert 25. aug. 2020 15:24
Publisert 4. nov. 2010 14:19
Publisert 22. sep. 2014 16:14
Publisert 27. sep. 2023 13:14