Seminars

See all upcoming seminars in LäsIT and seminar web pages at the homepage for the PhD studentseminars, TDB, Vi2, Theory and Applications Seminars (TAS) @ UpMARC., Department of Mathematics and The Stockholm Logic Seminar.

Disputation | PhD defense
Friday 23 Apr
Gustav Björdal: From Declarative Models to Local Search
, Time: 13:15

Join via Zoom: Click here for Zoom link


If you wish to attend on site, please contact phone 0734697031


Gustav Björdal will present and defend his PhD thesis From Declarative Models to Local Search.

Opponent: Prof. Laurent Michel
Supervisor:Pierre Flener

DiVA includes an abstract and the full text of the thesis.

Disputation | PhD defense
Monday 26 Apr
Arve Gengelbach: Conservative Definitions for Higher-order Logic with Ad-hoc Overloading
, Time: 9:15

Join via Zoom: Click here for Zoom link


If you wish to attend on site, please contact phone 070-4250239



Arve Gengelbach will present and defend his PhD thesis Conservative Definitions for Higher-order Logic with Ad-hoc Overloading.

Opponent: Senior lecturer Andrei Popescu
Supervisor:Tjark Weber

DiVA includes an abstract and the full text of the thesis.

Disputation | PhD defense
12 May
Leslie Solorzano: Image Processing, Machine Learning and Visualization for Tissue Analysis
Location: Sal IX, Universitetshuset, Time: 13:00

Leslie Solorzano will present and defend her PhD thesis Image Processing, Machine Learning and Visualization for Tissue Analysis.

Opponent: Professor Alexandru Telea
Supervisor:Carolina Wählby

More information will be published soon.

DoCS/CSD Seminar
21 May
Parosh Abdulla: Consistency and Persistency: Challenges and Opportunities in Program Verification
, Time: 14:15-15:15

Join via Zoom: Click here for Zoom link


Parosh Abdulla will present at the DoCS/CSD Seminar on verifying concurrent programs on architectures with persistent memory. The talk will be aimed at non-specialists and will not require deep knowledge of architecture or of formal methods.

Abstract:
Nowadays, most application platforms offer more relaxed semantics than the classical Sequential Consistency (SC) semantics. There are two primary sources of relaxation, namely weak consistency and weak persistence. Weakly consistent platforms are present at all level of the system design: at the hardware level, e.g., multiprocessors such as x86-TSO, SPARC, IBM POWER, and ARM; at the language level, e.g., C11 or Java; and at the application level, e.g., distributed databases, and geo-replicated systems. All these platforms sacrifice SC to provide stronger efficiency guarantees.

Weak persistence means that the order in which data persist over system crashes is inconsistent with the order in which the data is generated by the application. Weakly persistent systems arise in intermittent computing, file systems, and (more recently) architectures that employ Nonvolatile memories (NVRAMs).

Concurrent programs exhibit entirely new behaviors compared to SC when running on platforms with relaxed semantics. Even textbook programs such as small mutual exclusion protocols or concurrent data structures that are provably correct under SC can now show counter-intuitive behaviors. Hence, the verification community is currently facing new exciting, complicated, and practically motivated challenges.

To make the ideas concrete, I will present the semantics of concurrent programs that run on the Persistent Intel x86 architecture (Px86), implemented in Intel's Optane memory chip. We investigate the state reachability problem and show how to prove its decidability for finite-state programs. To achieve that, we provide a new formal model that is equivalent to Px86, and that has the feature of being a well-structured system. Deriving this new model results from a deep investigation of the properties of Px86 and the interplay of its components.

Half-time seminar
2021-10-08
Tina Vrieler: Teaching and Learning Computing in a Maker Community: A Longitudinal Study
, Time: 9:00-12:00

Tina Vrieler will present her half-time seminar Teaching and Learning Computing in a Maker Community: A Longitudinal Study.

More information will be published soon.

See also the list of all upcoming seminars.

Internal seminars. Lecturers may be either internal or external.

RSS