Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Ofer @Shanghai

less than 1 minute read

Published:

My collaborator, Professor Ofer Strichman from Technion, Israel, was invited to give a lecture titled ‘SAT/SMT - The Engines of Reasoning’ at the 20th International Summer School held at East China Normal University in Shanghai from July 9 to 12, 2024.

Paper accepted at VMCAI 2024

less than 1 minute read

Published:

Our paper «Model-Guided Synthesis for LTL over Finite Traces» is accepted at VMCAI 2024.

Moshe @Beijing

less than 1 minute read

Published:

My postdoc advisor Moshe Vardi, the professor at Rice University, visited Tsinghua University during Sept. 23 - 30.

IDAS 2023 @Wuhan

less than 1 minute read

Published:

Attend IDAS 2023 held in Wuhan, China.

CAV 2023 @Paris

less than 1 minute read

Published:

Our paper «Searching for i-good lemmas to accelerate safety model checking» was accepted and presented at CAV 2023.

portfolio

publications

talks

Talk on AAAI SSS-23

Published:

In this talk, I introduced our journey from LTLf satisfiability checking to synthesis.

teaching

Foundations of Automated Software Verification

Undergraduate course, Software Engineering, ECNU, 2023

This is a course for undergraduate students in Spring of 2023, introducing basic principles and foundations of model checking such as logics (propositional and LTL), automata theory and model checking algorithms.

tools

simplecar

Published:

simplecar is a simple implementation of CAR (Complementary Approximate Reachability), which is a novel safety model checker algorithm and was presented since 2017.

aalta/aaltaf

Published:

aalta is a SAT-based satisfiability checker for LTL over infinite traces, and aaltaf is for LTL over finite traces.