UFSC Federal University of Santa Catarina
Software/Hardware Integration Lab


Call for Participation

Date: 30 Sep 2013 Room: INE 103
Time: 15:10  


The Time and the Shape 

Mateus Krepsky Ludwich

Federal University of Santa Catarina
Software/Hardware Integration Lab (LISHA)

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
E-mail: lisha@lisha.ufsc.br
Web: http://www.lisha.ufsc.br