menu

School of Electronic Engineering and Computer Science

People menu

Dr Greta Yorsh

Greta

Lecturer

Email: g.yorsh@qmul.ac.uk
Telephone: +44 20 7882 6375
Room Number: Peter Landin, CS 430
Website: http://www.eecs.qmul.ac.uk/~gretay/

Teaching

Compilers (Undergraduate)

In this module, the students will learn how modern compilers work. A compiler is a tool for translating computer programs written in a higher-level programming language (such as Java or C) to a lower-level language or machine code. Major components of a compiler are lexical and syntactic analysis, semantic analysis, code generation and optimization. The module will provide an introduction to a range of concepts in programming language design and implementation, including runtime organization, memory management, assembler, linker, loader, static vs dynamic types and scopes, compilers vs interpreters, just-in-time compilation, bootstrapping, data-flow analysis, and link-time optimizations. The coursework includes 3-5 programming assignments, each of which builds a different component of the compiler. The students are encouraged to work in small teams. At the end of the semester, each team will have implemented a working (albeit simple) compiler from basic blocks and templates provided. Most students find it very rewarding experience.

Parallel Computing (Postgraduate)

High performance computing refers to the practice of aggregating computing power in order to deliver higher performance than would be obtained from a normal desktop machine. This module introduces concepts associated with high performance computing, such as parallel processing, hardware acceleration, GPU (Graphics Processing Unit) programming and FPGA (Field Programmable Gate Array) programming. It also explores some of the contexts in which high performance computing is often used, e.g. in scientific research and in business.

Program Specifications (Undergraduate/Postgraduate)

The module will cover: 1. Introduction to Logic for Systems and Program Verification and Analysis 2. Using Hoare Logic: The specification language - describing properties of programs; Proof rules in Hoare logic - verifying properties of programs; Basic technologies behind building automatic program verification tools based on Hoare logic; Using automatic verification tools based on Hoare logic. 3. Introduction to modelchecking and Spin: Temporal logic: modelling states and operations of a system; Modelchecking logics in particular CTL; Safety and Liveness in systems; Using Spin for checking properties and for problem solving.

Research

Publications

  • Jangda A, YORSH G (2017). Unbounded Superoptimization. Onward! 2017 Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
  • Vechev MT, Yahav E, Yorsh G (2013). Abstraction-guided synthesis of synchronization.. nameOfConference
  • Tripp O, Yorsh G, Field J et al. (2011). HAWKEYE: Effective Discovery of Dataflow Impediments to Parallelization. nameOfConference
  • Raman A, Yorsh G, Vechev M et al. (2011). Sprint: Speculative Prefetching of Remote Data. nameOfConference
  • Tripp O, Yorsh G, Field J et al. (2011). HAWKEYE: effective discovery of dataflow impediments to parallelization.. nameOfConference
  • Raman A, Yorsh G, Vechev MT et al. (2011). Sprint: speculative prefetching of remote data.. nameOfConference
  • Vechev M, Yahav E, Yorsh G (2010). Abstraction-Guided Synthesis of Synchronization. nameOfConference
  • Vechev MT, Yahav E, Yorsh G (2010). Abstraction-guided synthesis of synchronization.. Principles of Programming Languages The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
  • Vechev MT, Yahav E, Yorsh G (2010). PHALANX: parallel checking of expressive heap assertions.. nameOfConference
  • O'Hearn PW, Rinetzky N, Vechev MT et al. (2010). Verifying Linearizability with Hindsight. nameOfConference
  • Vechev MT, Yahav E, Yorsh G (2009). Experience with Model Checking Linearizability.. nameOfConference
  • Vechev MT, Yahav E, Yorsh G (2009). Inferring Synchronization under Limited Observability.. nameOfConference
  • Lev-Ami T, Immerman N, Reps TW et al. (2009). SIMULATING REACHABILITY USING FIRST-ORDER LOGIC WITH APPLICATIONS TO VERIFICATION OF LINKED DATA STRUCTURES. nameOfConference
  • Dor N, Field J, Gopan D et al. (2008). Automatic verification of strongly dynamic software systems. nameOfConference
  • Yorsh G, Yahav E, Chandra S (2008). Generating precise and concise procedure summaries.. nameOfConference
  • Yorsh G, Rabinovich AM, Sagiv M et al. (2007). A logic of reachable patterns in linked data-structures.. nameOfConference
  • Yorsh G, Reps T, Sagiv M et al. (2007). Logical characterizations of heap abstractions. nameOfConference
  • Yorsh G, Reps TW, Sagiv M et al. (2007). Logical characterizations of heap abstractions.. nameOfConference
  • Yorsh G, Rabinovich AM, Sagiv M et al. (2006). A Logic of Reachable Patterns in Linked Data-Structures.. nameOfConference
  • Yorsh G, Rabinovich A, Sagiv M et al. (2006). A logic of reachable patterns in linked data-structures. nameOfConference
  • Yorsh G, Ball T, Sagiv M (2006). Testing, abstraction, theorem proving: better together!. nameOfConference
  • Yorsh G, Musuvathi M (2005). A Combination Method for Generating Interpolants.. nameOfConference
  • Ball T, Kupferman O, Yorsh G (2005). Abstraction for Falsification.. nameOfConference
  • Yorsh G, Skidanov A, Reps TW et al. (2005). Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work.. nameOfConference
  • Lev-Ami T, Immerman N, Reps TW et al. (2005). Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures.. nameOfConference
  • Reps TW, Sagiv S, Yorsh G (2004). Symbolic Implementation of the Best Transformer.. nameOfConference
  • Yorsh G, Reps TW, Sagiv S (2004). Symbolically Computing Most-Precise Abstract Operations for Shape Analysis.. nameOfConference
  • Immerman N, Rabinovich AM, Reps TW et al. (2004). The Boundary Between Decidability and Undecidability for Transitive-Closure Logics.. nameOfConference
  • Immerman N, Rabinovich AM, Reps TW et al. (2004). Verification via Structure Simulation.. nameOfConference
Return to top