Dr. S.W.B. (Wishnu) Prasetya

Buys Ballotgebouw
Princetonplein 5
Kamer BBL-566
3584 CC Utrecht

Dr. S.W.B. (Wishnu) Prasetya

Assistant Professor
Software Technology
+31 30 253 4090
s.w.b.prasetya@uu.nl

Lecturer and scientist. Research area: automated software testing, AI enhanced testing, program verification. Projects:

 

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.