A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
Maksym Bortin
Tallinn University of Technology
Abstract: The talk will give a brief overview of a framework,
embedded into simply typed higher-order logic and aimed at providing a
sound assistance in formal reasoning about models of imperative
programs with interleaved computations.