Federal University of Santa Catarina
Software/Hardware Integration Lab
Call for Participation
|Date: 30 Sep 2013||Room: INE 103|
The Time and the Shape
This presentation first introduces a logic that combines Linear Temporal Logic (LTL), and Separation Logic (SL). Then, it presents how this combined logic can be used on the generation of Runtime Verification monitors that are used to verify whether structural, and temporal properties hold for a given system.
Mateus Krepsky Ludwich received his B.Sc. and M.Sc. from the Federal University of Santa Catarina, Brazil. Mateus is currently a Ph.D. student at the same university and works as researcher in the Software/Hardware Integration Lab (LISHA). Mateus has background experience in system software, operating systems, and programming languages. His research interests are in formal verification of embedded systems, mainly concerning how to apply verification methods to embedded operating systems components that can be deployed either on software or hardware.
PO Box 476
88040-900 Florianópolis - SC
Phone: +55 48 3721-9516
Fax: +55 48 3721-9516.b16