Sumários
Exercises on Separation Logic
19 dezembro 2019, 12:30 • João Fernando Ferreira
Exercises on Separation Logic: assertions and proving small programs.
Exercises on Separation Logic
19 dezembro 2019, 11:00 • João Fernando Ferreira
Exercises on Separation Logic: assertions and proving small programs.
Invited Lecture by José Fragoso
19 dezembro 2019, 09:30 • João Fernando Ferreira
The lecture on the 19th December was delivered by Prof. José Santos.
ABSTRACT: The dynamic nature of JavaScript, together with its complex semantics, makes it a difficult target for logic-based verification techniques. I will present JaVerT: a semi-automatic verification tool chain for JavaScript based on separation logic. JaVerT targets functionally correct specifications of critical JavaScript software, in particular focusing on small Node.js libraries that have high usability: for example, those describing well-known data structures, such as a priority queue. JaVerT provides a wide variety of built-in abstractions so that our specifications are straightforward, despite the underlying complexity of the JavaScript semantics.The talk will consist of a demo of JaVerT, illustrating how it can be used to specify and verify a JavaScript priority queue implementation. It will showcase the abstractions provided by JaVerT for reasoning about the JavaScript semantics, with an emphasis on objects, prototype chains, and function closures, as well as the infrastructure for supporting arbitrary user-defined recursive predicates.
Revision / Consolidation
17 dezembro 2019, 11:00 • João Fernando Ferreira
We solved a selection of exercises on program verification (Hoare Logic, Dafny, and Separation Logic).
Lab used to work on practical project
12 dezembro 2019, 12:30 • João Fernando Ferreira
Students worked (and received support) on their projects.