Lecturer and scientist. Research area: automated software testing, AI enhanced testing, program verification. Projects:
- iv4XR: AI-enhanced automated testing [project's github is here] [demo video] [demo project]
- Our agent-programming testing framework: iv4XR/Aplib. Check our paper Aplib: Tactical Agents for Testing Computer Games.
- IMPRESS: Improving Engagement of Students in Software Engineering Courses through Gamification. Check our papr: Can Learning Formal Specification Be Fun? – Experience and Perspective.
- Automated testing for Java: T3i.
- FITTEST project (Internet Testing) [vault].
WLP-based verification
Some previous work I did in verification engines for imperative core-languages. E.g. the Ecore library provides Dijkstra WLP-logic for a simple sequential language. The language supports basic control structures, block, program call (with pass-by-value and pass-by-reference parameters), and "old" key-word in the specification to refer to a variable's initial value. Ecore is provided as a HOL library, thus using HOL as its back-end prover. [download]
UNITY
UNITY is a nice and simple axiomatic formal system by Chandy and Misra used to model concurrent systems and to prove temporal properties about them. See Parallel Program Design: A Foundation" by Chandy, K. Mani and Misra, Jayadev. They had a group at University of Texas at Austin; if for historical reason you are interested in the old collection of "Notes on Unity", they are kept in Misra webpage here.