Wishnu Prasetya

T3i

T3i is a tool to automatically generate test suites to unit-test Java classes. T3i allows test suites to be interactively generated and manipulated. Test suites are treated as first class objects; they can be merged, queried, filtered, and transformed. Test suites can be analyzed, e.g. to mine invariants. T3i uses T3 as back-end, which is random-based, but very fast.

URL: https://git.science.uu.nl/prase101/t3/wikis/home
To cite the tool:
To cite the back-end tool T3, or its precessor T2:

FITTEST

FITTEST was a European project to develop a continous testing approach to test Internet Applications.

URL: http://crest.cs.ucl.ac.uk/fittest
To cite the project:
A more detailed overview of the project:
Vault: http://www.projects.science.uu.nl/cs-fittest/

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 simple axiomatic logic to prove temporal properties of concurrent systems.

UNITY's traditional home at Austin :) It includes the old collection of "Notes on UNITY".
My embedding of various variants of UNITY in the theorem prover HOL.