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.
 

UFSC/CTC/LISHA PO Box 476 88040-900 Florianópolis - SC BRAZIL

Phone: +55 48 3721-9516 Fax: +55 48 3721-9516.b16 E-mail: lisha@lisha.ufsc.br Web: http://www.lisha.ufsc.br