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 and Nikolaj Bjorner, Alternating simulation and IOCO, in International Journal on Software Tools for Technology Transfer (STTT) , Springer, November 2011
- Margus Veanes and Nikolaj Bjorner, Alternating Simulation and IOCO, in ICTSS'10, Springer Verlag, November 2010
- Margus Veanes and Jonathan Jacky, Composing Model Programs for Analysis, in The Journal of Logic and Algebraic Programming, vol. 79, no. 7, pp. 467-482, Elsevier , October 2010
- Margus Veanes, Nikolai Tillmann, and Jonathan de Halleux, Qex: Symbolic SQL Query Explorer, no. MSR-TR-2009-2015, October 2009
- Margus Veanes, Nikolaj Bjorner, Yuri Gurevich, and Wolfram Schulte, Symbolic Bounded Model Checking of Abstract State Machines, in Int J Software Informatics, vol. 3, no. (2-3), pp. 149-170, June 2009
- Margus Veanes and Nikolaj Bjorner, Input-Output Model Programs, no. MSR-TR-2009-56, May 2009
- 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, Symbolic Bounded Conformance Checking of Model Programs, no. MSR-TR-2009-28, 14 March 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
