Friday, 16 May 2008, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: We look at a fragment of ASMs used to model protocol-like aspects of software systems. Such models are used industrially as part of documentation and oracles in modelbased testing of application-level network protocols. Correctness assumptions about the model are often expressed through state invariants. An important problem is to validate the model prior to its use as an oracle. We discuss a technique of using Satisfiability Modulo Theories or SMT to perform bounded reachability analysis of such models, outline the main challenges and propose some solutions to them.