Federal University of Santa Catarina Software/Hardware Integration Lab

Call for Participation

Date: 30 Jan 2013	Room: INE 105
Time: 14:00

 

Lightweight Modeling: Language, Tools, and Analysis

Steven Stewart

University of Waterloo

In lightweight modeling, analysis is applied incrementally while developing an abstraction, and lightweight formal methods offer an attempt to obtain the benefits of formal methods without incurring a heavy cost. Alloy is a problem description language used in the application of lightweight formal methods, and Kodkod, a relational constraint solver, is the backend of Alloy. Ultimately, these tools leverage advancements in SAT-solving technologies for the analysis of lightweight models, and a number of applications have emerged, including model finding, design space exploration, program synthesis, and discrete multi-objective optimization. Currently, we are interested in re-engineering Alloy to offer a more extensible and extendable language and compiler, offering greater flexibility to researchers wanting to customize this toolchain for their respective problem domains. Additionally, an intriguing new application of Alloy and Kodkod is being proposed that introduces bounded model checking into a runtime verification architecture.

 

Steven Stewart received his Bachelor of Arts and Bachelor of Computer Science degrees in 2008 from the University of New Brunswick, Canada. He earned his Master's of Computer Science degree in 2011, also from the University of New Brunswick, on the topic of parallel dynamic programming. Currently, Steven is a PhD student at the University of Waterloo, Canada, in the Department of Electrical and Computer Engineering, interested in software language engineering and formal methods.

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