Skip to content
View SaharRamezani's full-sized avatar
😁
Focusing
😁
Focusing
27 followers · 27 following

Achievements

Achievement: Public SponsorAchievement: Pair ExtraordinaireAchievement: QuickdrawAchievement: YOLOAchievement: Pull Sharkx2

Achievements

Achievement: Public SponsorAchievement: Pair ExtraordinaireAchievement: QuickdrawAchievement: YOLOAchievement: Pull Sharkx2

Highlights

  • Pro

Block or report SaharRamezani

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
SaharRamezani/README.md

intro

CS master's student in Genoa, research intern at MPI-SWS. I look for races in concurrent programs, and for proofs that there are none. Sometimes both at once.

// currently

$ whoami
> sahar ramezani. cs master's @ unige, research intern @ mpi-sws
$ currently_doing
> extending DPOR with timestamps in TraceForge
$ also
> teaching Coq to admit when it does not know
$ uptime
> 3 espressos, 1 admitted lemma, 0 races on purpose

// what I work on

At MPI-SWS, the tool I'm working on is TraceForge, a Rust engine for stateless model checking of distributed systems. The phrase "stateless model checking" sounds harder to explain at parties than it actually is. Short version: run a concurrent program over enough interleavings to be confident the bug is not there, without running all of them.

// shipped, outside academia

  • Tender Offer System for the oil sector
  • Grant Request System for a Ministry of Science
  • Oracle Forms and PL/SQL modules across several internal tools
  • A project management platform that ended up being sold to a company

// the stack

languages
Rust Kotlin Java C C++ Python Solidity

verification & theory
Coq Rocq OCaml LaTeX

infra & tools
Linux Git Docker Oracle PostgreSQL GitHub Actions

// one theorem, mostly admitted

Theorem sahar_likes_concurrency : forall p, concurrent p -> exists b, found_by_DPOR b p.
Proof.
  intros p Hc.
  induction Hc.
  - (* base case: trivially fine *)
  - (* inductive case: probably fine, it is 2 a.m. *)
Admitted.

// elsewhere

  linkedin   google scholar

based in Italy. English C1, Italian B1, German A1. international students' representative at UniGe.

Pinned Loading

  1. Cyclink Cyclink Public

    Cyclink is a comprehensive mobile application designed to enhance the cycling experience through team management, activity tracking, and AI-powered assistance.

    Kotlin 4

  2. KooDoc KooDoc Public

    Your Smart Companion for Childcare

    Kotlin 2

  3. Crypto-Donation-Platform Crypto-Donation-Platform Public

    A decentralized application (dApp) for donating Sepolia ETH to charitable organizations.

    JavaScript

  4. BridgeAllMighty BridgeAllMighty Public

    A Docker-based security testing setup featuring a vulnerable web service, a filtering HTTP proxy ("bridge"), and an attacker client. Demonstrates vulnerability exploitation (e.g., SQL injection) an…

    Lua 1

  5. Discrete-Event-Simulation Discrete-Event-Simulation Public

    Simulator with event scheduling, process management, and client-server communication to model system behavior and network data exchange.

    Python

  6. Coq-Learning Coq-Learning Public

    Formal verification exercises in Coq: mechanized semantics, inductive proofs, custom automation, and verified parsers/automata

    Makefile