Portfolio item number 1
Short description of portfolio item number 1
Posts by Collection
portfolio
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.