M3: Model theory, Model generation & Model analysis
We are looking at high-level models that may involve reasonig with rich background universes or combinations of different theories, that arise in various practical applications. The mission is to investigate: 1) What is the appropriate model theory? 2) How can models be generated? 3) How can models be analyzed?
Publications
- Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann, Symbolic Query Exploration, no. MSR-TR-2009-65, May 2009
- Margus Veanes and Nikolaj Bjorner, Input-Output Model Programs, no. MSR-TR-2009-56, May 2009
- Margus Veanes and Nikolaj Bjorner, Symbolic Bounded Conformance Checking of Model Programs, no. MSR-TR-2009-28, 14 March 2009
- Nikolaj Bjorner, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Symbolic Bounded Model Checking of Abstract State Machines, no. MSR-TR-2009-14, February 2009
- Margus Veanes and Ando Saabas, On Bounded Reachability of Programs with Set Comprehensions, in LPAR'08, Springer Verlag, November 2008
- Margus Veanes and Ando Saabas, Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract), in ABZ'08, Springer Verlag, September 2008
- Margus Veanes, Nikolaj Bjørner, and Alexander Raschke, An SMT Approach to Bounded Reachability Analysis of Model Programs, in FORTE'08, Springer Verlag, June 2008
- Margus Veanes, Ando Saabas, and Nikolaj Bjorner, Bounded reachability of model programs, no. MSR-TR-2008-81, May 2008
- Jonathan Jacky, Margus Veanes, Colin Campbell, and Wolfram Schulte, Model-Based Software Testing and Analysis with C#, Cambridge University Press, January 2008
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to Test, in FATES 2005, Springer Verlag, July 2005
