Page Not Found
Page not found. Your pixels are in another canvas.
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
Short Bio
About me
Page not in menu
This is a page not in th emain menu
Posts
Paper accepted at CAV 2024
Published:
Our paper «Avoiding the Shoals - A New Approach to Liveness Checking» is accepted at CAV 2024.
ATVA 2024 PC member
Published:
I was invited as a PC member at ATVA 2024.
CAV 2024 PC member
Published:
I was invited as a PC member at CAV 2024.
Paper accepted at VMCAI 2024
Published:
Our paper «Model-Guided Synthesis for LTL over Finite Traces» is accepted at VMCAI 2024.
Moshe @Beijing
Published:
My postdoc advisor Moshe Vardi, the professor at Rice University, visited Tsinghua University during Sept. 23 - 30.
IDAS 2023 @Wuhan
Published:
Attend IDAS 2023 held in Wuhan, China.
CAV 2023 @Paris
Published:
Our paper «Searching for i-good lemmas to accelerate safety model checking» was accepted and presented at CAV 2023.
portfolio
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
publications
SAT-based LTL Satisfiability Checking
Published in Journal 1, 2009
This paper is about the number 1. The number 2 is left for future work.
Recommended citation: Your Name, You. (2009). "Paper Title Number 1." Journal 1. 1(1). http://academicpages.github.io/files/paper1.pdf
Paper Title Number 2
Published in Journal 1, 2010
This paper is about the number 2. The number 3 is left for future work.
Recommended citation: Your Name, You. (2010). "Paper Title Number 2." Journal 1. 1(2). http://academicpages.github.io/files/paper2.pdf
Paper Title Number 3
Published in Journal 1, 2015
This paper is about the number 3. The number 4 is left for future work.
Recommended citation: Your Name, You. (2015). "Paper Title Number 3." Journal 1. 1(3). http://academicpages.github.io/files/paper3.pdf
talks
Talk on AAAI SSS-23
Published:
In this talk, I introduced our journey from LTLf satisfiability checking to synthesis.
Talk on HW Formal Methods Workshop @Hongkong
Published:
In this talk, I introduced the history of model checking and our recent work in this topic
teaching
Automatic Verification for Intelligent Systems
Graduate course, Software Engineering, ECNU, 2022
This is a course for graduate students in Autumn of 2022, introducing model checking techniques and their applications to the industry.
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.