Publications and Selected Talks

2017

  • Michalis Famelis, Julia Rubin, Rick Salay, Krzisztof Czarnecki, Marsha Chechik. “Design Space Exploration for Product Families: Reasoning about Variability and Uncertainty”. MODELS 2017, 8 pages. [slides]
  • Alicia Grubb and Marsha Chechik. “Modeling and Reasoning with Changing Intentions: An Experiment”. RE 2017, 11 pages. [paper] [slides] [supplementary material]
  • Gabriele Taentzer, Rick Salay, Daniel Struber, Marsha Chechik. “Transformations of Software Product Lines: A Generalizing Framework based on Category Theory”. MODELS’ 2017, 11 pages. [slides]
  • Daniel Struber, Julie Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer, Jennifer Ploger. “Variability-Based Model Transformation: Formal Foundation and Application”. J. of Formal Aspects of Computing , 2017. Journal version of FASE’16 paper (invited). [paper]
  • Michalis Famelis, Marsha Chechik. “Managing Design-Time Uncertainty”. In J. of Systems and Software (SoSyM), 2017, 36 pages. Also presented as "Journal First" at MODELS 2017. [slides] [paper]
  • Yi Li, Chenguang Zhu, Julia Rubin, Marsha Chechik. “Semantic Slicing of Software Version Histories”. IEEE Transactions on Software Engineering (TSE), pp. 1-22, 2017. [paper]
  • Marsha Chechik. "Software Safety and Security, Assurance Cases and Model Management". SEFM, 2017. Invited talk. [slides]
  • Sahar Kokaly: "Managing assurance cases in model based software systems". Doctoral Symposium @ ICSE 2017: 453-456 [pdf] [slides]
  • Christina Chung, Amit Kadan, Yueti Yang, Asako Matsuoka, Julia Rubin, Marsha Chechik: "The impact of visual load on performance in a human-computation game". FDG 2017: 51:1-51:4
  • Davide Di Ruscio, Marsha Chechik, Bernhard Rumpe: "9th Workshop on Modelling in Software Engineering (MiSE 2017)". MiSE@ICSE 2017: 1
  • Cynthia Disenfeld, Ioanna Stavropoulou, Julia Rubin, Marsha Chechik: "FPH: efficient detection of feature interactions through non-commutativity". ICSE (Companion Volume) 2017: 225
  • Chenguang Zhu, Yi Li, Julia Rubin, Marsha Chechik: "A dataset for dynamic discovery of semantic changes in version controlled software histories". MSR 2017: 523-526 [slides]
  • Sahar Kokaly, Rick Salay, Marsha Chechik, Mark Lawford, Tom Maibaum: "Safety Case Impact Assessment in Automotive Software Systems: An Improved Model-Based Approach". SAFECOMP 2017: 69-85 [slides]
  • Daniel Strüber, Julia Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer, Jennifer Plöger: "RuleMerger: Automatic Construction of Variability-Based Model Transformation Rules". Software Engineering 2017: 135-136
  • Yi Li, Chenguang Zhu, Julia Rubin, Marsha Chechik: "FHistorian: Locating Features in Version Histories". SPLC (A) 2017: 49-58

2016

  • Michalis Famelis. Managing Design-Time Uncertainty in Software Models. Ph.D. Thesis, University of Toronto, 2016.
  • Shoham Ben-David, Marsha Chechik, Sebastián Uchitel: "Observational Refinement and Merge for Disjunctive MTSs". ATVA 2016: 287-303
  • Daniel Strüber, Julia Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer, Jennifer Plöger: "RuleMerger: Automatic Construction of Variability-Based Model Transformation Rules". FASE 2016: 122-140
  • Rick Salay, Steffen Zschaler, Marsha Chechik: Correct Reuse of Transformations is Hard to Guarantee. ICMT 2016: 107-122
  • Christina Chung, Asako Matsuoka, Yueti Yang, Julia Rubin, Marsha Chechik: "Serious games for NP-hard problems: challenges and insights". GAS@ICSE 2016: 29-32
  • Sahar Kokaly, Rick Salay, Mehrdad Sabetzadeh, Marsha Chechik, Tom Maibaum: "Model management for regulatory compliance: a position paper". MiSE@ICSE 2016: 74-80 [slides]
  • Marsha Chechik, Michalis Famelis, Rick Salay, Daniel Strüber: "Perspectives of Model Transformation Reuse". IFM 2016: 28-44 [slides]
  • Alicia M. Grubb, Gary Song, Marsha Chechik: "GrowingLeaf: Supporting Requirements Evolution over Time". iStar 2016: 31-36 [pdf] [slides]
  • Yi Li, Chenguang Zhu, Julia Rubin, Marsha Chechik: "Precise semantic history slicing through dynamic delta refinement". ASE 2016: 495-506
  • Rick Salay, Sahar Kokaly, Marsha Chechik, Tom Maibaum: "Heterogeneous Megamodel Slicing for Model Evolution". ME@MODELS 2016: 50-59 [slides]
  • Sahar Kokaly, Rick Salay, Valentin Cassano, Tom Maibaum, Marsha Chechik: "A model management approach for assurance case reuse due to system evolution". MoDELS 2016: 196-206 [slides]
  • Alicia M. Grubb, Marsha Chechik: "Looking into the Crystal Ball: Requirements Evolution over Time". RE 2016: 86-95 [slides] [supplementary material]
  • Marsha Chechik, Jean-François Raskin: Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science 9636, Springer 2016, ISBN 978-3-662-49673-2
  • Sandrine Blazy, Marsha Chechik: Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers. Lecture Notes in Computer Science 9971, 2016, ISBN 978-3-319-48868-4

2015

  • Aws Albarghouthi. Software Verification with Program-Graph Interpolation and Abstraction/ Ph.D. Thesis, University of Toronto, 2015.
  • Rick Salay, Marsha Chechik, Michalis Famelis, Jan Gorzny: "A Methodology for Verifying Refinements of Partial Models". Journal of Object Technology 14(3): 3:1-31 (2015)
  • Marsha Chechik, Geri Georg, Martin Gogolla, Jean-Marc Jézéquel, Bernhard Rumpe, Martin Schindler: "In memory of Robert B. France, Co-Founder and Editor-in-Chief of SoSyM from 1999 to 2015". Software and System Modeling 14(2): 525-532 (2015)
  • Julia Rubin, Krzysztof Czarnecki, Marsha Chechik: "Cloned product variants: from ad-hoc to managed software product lines". STTT 17(5): 627-646 (2015)
  • Rick Salay, Marsha Chechik: "A Generalized Formal Framework for Partial Modeling". FASE 2015: 133-148
  • Daniel Strüber, Julia Rubin, Marsha Chechik, Gabriele Taentzer: "A Variability-Based Approach to Reusable and Efficient Model Transformations". FASE 2015: 283-298
  • Michalis Famelis, Levi Lucio, Gehan M. K. Selim, Alessio Di Sandro, Rick Salay, Marsha Chechik, James R. Cordy, Jürgen Dingel, Hans Vangheluwe, Ramesh S: "Migrating Automotive Product Lines: A Case Study". ICMT 2015: 82-97
  • Rick Salay, Fabiano Dalpiaz, Marsha Chechik: "Integrating Crowd Intelligence into Software". CSI-SE 2015: 1-7
  • Michalis Famelis, Naama Ben-David, Alessio Di Sandro, Rick Salay, Marsha Chechik: "MU-MMINT: An IDE for Model Uncertainty". ICSE (2) 2015: 697-700
  • Jeff Gray, Marsha Chechik, Vinay Kulkarni, Richard F. Paige: "7th International Workshop on Modeling in Software Engineering (MiSE 2015)". ICSE (2) 2015: 985-986
  • Yi Li, Julia Rubin, Marsha Chechik: "Semantic Slicing of Software Version Histories". ASE 2015: 686-696
  • Marsha Chechik, Fabiano Dalpiaz, Csaba Debreceni, Jennifer Horkoff, István Ráth, Rick Salay, Dániel Varró: "Property-Based Methods for Collaborative Model Development". GEMOC+MPM@MoDELS 2015: 1-7
  • Rick Salay, Steffen Zschaler, Marsha Chechik: "Transformation Reuse: What is the Intent?" AMT@MoDELS 2015: 7-15
  • Alessio Di Sandro, Rick Salay, Michalis Famelis, Sahar Kokaly, Marsha Chechik: "MMINT: A Graphical Tool for Interactive Model Management". MODELS Tool Demo 2015: 16-19 [video]
  • Rick Salay, Sahar Kokaly, Alessio Di Sandro, Marsha Chechik: "Enriching megamodel management with collection-based operators". MoDELS 2015: 236-245 [slides]
  • Fabiano Dalpiaz, Michal Korenko, Rick Salay, Marsha Chechik: "Using the crowds to satisfy unbounded requirements". CrowdRE@RE 2015: 19-24
  • Thorsten Berger, Daniela Lettner, Julia Rubin, Paul Grünbacher, Adeline Silva, Martin Becker, Marsha Chechik, Krzysztof Czarnecki: "What is a feature?: a qualitative study of features in industrial software product lines". SPLC 2015: 16-25
  • Marsha Chechik: "Modeling and Reasoning about Software Systems Containing Uncertainty and Variability". TASE 2015: 1
  • Jeff Gray, Marsha Chechik, Vinay Kulkarni, Richard F. Paige: 7th IEEE/ACM International Workshop on Modeling in Software Engineering, MiSE 2015, Florence, Italy, May 16-17, 2015. IEEE Computer Society 2015, ISBN 978-1-4673-7055-4
  • Dimitris S. Kolovos, Marsha Chechik: Proceedings of the Doctoral Symposium at the 18th ACM/IEEE International Conference of Model-Driven Engineering Languages and Systems 2015 (MoDELS 2015), Ottawa, Canada, September 29, 2015. CEUR Workshop Proceedings 1531, CEUR-WS.org 2015

2014

  • Daniel Strüber, Julia Rubin, Gabriele Taentzer, Marsha Chechik: "Splitting Models Using Information Retrieval and Model Crawling Techniques". FASE 2014: 47-62
  • Teemu Kanstrén, Marsha Chechik: "A Comparison of Three Black-Box Optimization Approaches for Model-Based Testing". FedCSIS 2014: 1591-1598
  • Yi Li, Tian Huat Tan, Marsha Chechik: "Management of Time Requirements in Component -Based Systems". FM 2014: 399-415
  • Ahmed Shah Mashiyat, Michalis Famelis, Rick Salay, Marsha Chechik: "Using developer conversations to resolve uncertainty in software development: a position paper". RSSE@ICSE 2014: 1-5
  • Rick Salay, Michalis Famelis, Julia Rubin, Alessio Di Sandro, Marsha Chechik: "Lifting model transformations to product lines". ICSE 2014: 117-128
  • Teemu Kanstrén, Marsha Chechik: "Trace Reduction and Pattern Analysis to Assist Debugging in Model-Based Testing". ISSRE Workshops 2014: 238-243
  • Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik: "Symbolic optimization with SMT solvers". POPL 2014: 607-618
  • Jennifer Horkoff, Rick Salay, Marsha Chechik, Alessio Di Sandro: "Supporting early decision-making in the presence of uncertainty". RE 2014: 33-42
  • Ivica Crnkovic, Marsha Chechik, Paul Grünbacher: ACM/IEEE International Conference on Automated Software Engineering, ASE '14, Vasteras, Sweden - September 15 - 19, 2014. ACM 2014, ISBN 978-1-4503-3013-8

2013

  • Jocelyn Simmonds, Shoham Ben-David, Marsha Chechik: "Monitoring and recovery for web service applications". Computing 95(3): 223-267 (2013)
  • Sebastián Uchitel, Dalal Alrajeh, Shoham Ben-David, Víctor A. Braberman, Marsha Chechik, Guido de Caso, Nicolás D'Ippolito, Dario Fischbein, Diego Garbervetsky, Jeff Kramer, Alessandra Russo, German E. Sibay: "Supporting incremental behaviour model elaboration". Computer Science - R&D 28(4): 279-293 (2013)
  • Rick Salay, Marsha Chechik, Jennifer Horkoff, Alessio Di Sandro: "Managing requirements uncertainty with partial models". Requir. Eng. 18(2): 107-128 (2013)
  • Marsha Chechik, Jocelyn Simmonds, Sotirios Liaskos, Shiva Nejati, Mehrdad Sabetzadeh, Rick Salay: "PWWM: A Personal Web Workflow Methodology". The Personal WeB 2013: 11-48
  • Shoham Ben-David, Marsha Chechik, Sebastián Uchitel: "Merging Partial Behaviour Models with Different Vocabularies". CONCUR 2013: 91-105
  • Rick Salay, Jan Gorzny, Marsha Chechik: "Change Propagation due to Uncertainty Change". FASE 2013: 21-36
  • Julia Rubin, Marsha Chechik: "Quality of Merge-Refactorings for Product Lines". FASE 2013: 83-98
  • Julia Rubin, Marsha Chechik: "A framework for managing cloned product variants". ICSE 2013: 1233-1236
  • Joanne M. Atlee, Robert Baillargeon, Marsha Chechik, Robert B. France, Jeff Gray, Richard F. Paige, Bernhard Rumpe: "5th international workshop on modeling in software engineering (MiSE 2013)". ICSE 2013: 1531-1532
  • Michalis Famelis, Rick Salay, Alessio Di Sandro, Marsha Chechik: "Transformation of Models Containing Uncertainty". MoDELS 2013: 673-689
  • Soroosh Nalchigar, Rick Salay, Marsha Chechik: "Towards a Catalog of Non-Functional Requirements in Model Transformation Languages". AMT@MoDELS 2013
  • Rick Salay, Marsha Chechik: "Supporting Agility in MDE Through Modeling Language Relaxation". XM@MoDELS 2013: 20-27
  • Julia Rubin, Marsha Chechik: "N-way model merging". ESEC/SIGSOFT FSE 2013: 301-311
  • Julia Rubin, Krzysztof Czarnecki, Marsha Chechik: "Managing cloned variants: a framework and experience". SPLC 2013: 101-110
  • Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik: "UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution)". TACAS 2013: 637-640
  • Julia Rubin, Marsha Chechik: "A Survey of Feature Location Techniques". Domain Engineering, Product Lines, Languages, and Conceptual Models 2013: 29-58
  • Joanne M. Atlee, Robert Baillargeon, Marsha Chechik, Robert B. France, Jeff Gray, Richard F. Paige, Bernhard Rumpe: Proceedings of the 5th International Workshop on Modeling in Software Engineering, MiSE 2013, San Francisco, California, USA, May 18-19, 2013. IEEE Computer Society 2013, ISBN 978-1-4673-6447-8

2012

  • M. Famelis. `Uncertainty Management with Partial Models''. In Proceedings of MODELS'12 Doctoral Symposium, October 2012.
  • P. Saadatpanah, M. Famelis, J. Gorzny, N. Robinson, M. Chechik, R. Salay. ``Comparing the Effectiveness of Reasoning Formalisms for Partial Models''. In Proceedings of MODELS'12 Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVA'12), 6 pages, October 2012. [pdf]
  • A. Albarghouthi, A. Gurfinkel, M. Chechik. ``Clair Interpretation''. In Proceedings of International Static Analysis Symposium (SAS'12), 16 pages, September 2012. [pdf]
  • R. Salay, M. Chechik, J. Horkoff. ``Managing Requirements Uncertainty with Partial Models''. In Proceedings of 20th IEEE International Requirements Engineering Conference (RE'12), September 2012. Best paper award [pdf]
  • J. Rubin, M. Chechik. ``Locating Distinguishing Features using Diff Sets''. In Proceedings of International Conference on Automated Software Engineering (ASE'12), September 2012, 4 pages (short paper). [pdf]
  • J. Rubin, A. Kirshin, G. Boetterweck, M. Chechik. ``Managing Forked Product Variants''. In Proceedings of International Software Product Line Conference (SPLC'12), September 2012, 5 pages (short paper). [pdf]
  • A. Albarghouthi, Y. Li, A. Gurfinkel, M. Chechik. ``UFO: A framework for Abstraction- and Interpolation-Based Software Verification''. In Proceedings of CAV'12, pp. 672-678, July 2012. [pdf]
  • M. Famelis, R. Salay, M. Chechik. ``Partial Models: Towards Modeling and Reasoning with Uncertainty''. In Proceedings of ICSE'12, pp. 573-583, May 2012. SIGSOFT Distinguished Paper. [pdf]
  • M. Famelis, R. Salay, M. Chechik. ``The Semantics of Partial Model Transformations''. In Proceedings of ICSE'12 Workshop on Models in Software Engineering (MiSE'12), 6 pages, June 2012. [pdf]
  • R. Salay, M. Chechik, J. Gorzny. ``Towards a Methodology for Verifying Partial Model Refinements''. In Proceedings of ICST'12 (VOLT'12 Workshop), pp. 938-945, April 2012. [pdf]
  • A. Albarghouthi, A. Gurfinkel, M. Chechik. ``From Under-Approximations to Over-Approximations and Back''. In Proceedings of TACAS'12, pp. 157-172, March 2012. [pdf]
  • R. Salay, M. Famelis, M. Chechik. ``Language Independent Refinement Using Partial Modeling''. In Proceedings of FASE'12, pp. 224-239, March 2012. [pdf]
  • J. Rubin, M. Chechik. ``Combining Related Products into Product Lines''. In Proceedings of FASE'12, pp. 285-300, March 2012. [pdf]
  • A. Albarghouthi, A. Gurfinkel, M. Chechik. ``Whale: An Interpolation-Based Algorithm for Inter-Procedural Verification''. In Proceedings of VMCAI'12, pp. 39-55, January 2012. [pdf]
  • A. Gurfinkel, M. Chechik. "Robust Vacuity for Branching Temporal Logic". Journal version of the FMCAD'04 paper. ACM Transactions on Computational Logic, 13(1), pp. 1-36, 2012. [PDF]
  • D. Fischbein, N. D'Ippolito, G. Brunet, M. Chechik, S. Uchitel. ``Weak Alphabet Merging of Partial Behaviour Models''. In ACM Transactions on Software Engineering and Methodology, 21(2), pp. 9-62, 2012. [PDF]
  • M. Chechik, S. Nejati, M. Sabetzadeh. ``A Relationship-Based Approach to Model Integration''. In Journal of Innovations in Systems and Software Engineering (ISSE), 8(1), pp. 3-18, 2012. [PDF].
  • J. Simmonds, S. Ben-David, M. Chechik. "Monitoring and Recovery for Web Service Applications". In Journal of Computing, Special Issue on Models at Run Time, 2012. [pdf]
  • J. Rubin, M. Chechik. ``A Survey of Feature Location Techniques''. Invited book chapter. 28 pages. [pdf]

2011

  • M. Famelis, S. Ben-David, M. Chechik, R. Salay. ``Partial Models: A Position Paper''. In Proceedings of MODELS'11 Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVA'11), 4 pages, October 2011. [pdf]
  • M. Chechik, J. Simmonds, S. Liaskos, S. Nejati, M. Sabetzadeh, R. Salay. ``PWWM: A Pesonal Web Workflow Methodology''. Invited book chapter. Submitted August 2011. 38 pages. [pdf]
  • S. Ben-David, M. Chechik, A. Gurfinkel, S. Uchitel. ``CSSL: A Logic for Specifying Conditional Scenarios''. In Proceedings of SIGSOFT FSE'11, pp. 37-47, November 2011. [pdf]
  • O. Wei, A. Gurfinkel, M. Chechik. "On the Consistency, Expressiveness, and Precision of Partial Models". Journal version of the VMCAI'09 paper. Journal of Information and Computation, 209(1), pp. 20-47, 2011. [PDF]
  • M. Chechik, S. Uchitel, M. Sassolas. "Exploring Inconsistencies between Modal Transition Systems". J. of Software and System Modeling (SoSyM), Volume 10, Number 1, pp. 117-142, 2011. [PDF]
  • S. Nejati, M. Sabetzadeh, M. Chechik, S. Easterbrook, P. Zave. "Matching and Merging of Variant Feature Specifications". Accepted to IEEE Transactions on Software Engineering, November 2011. [pdf]

2010

  • M. Chechik and J. Simmonds and S. Ben-David and S. Nejati and M. Sabetzadeh and R. Salay. "Modeling and Analysis of Personal Web Applications: A Vision". In Proceedings of NSERC/CASCON Symposium on Personal Web, November 2010. [PDF]
  • M. Chechik and A. Gurfinkel and S. Uchitel and S. Ben-David. "Raising Level of Abstraction with Partial Models: A Vision". In Proceedings of NSF/MSR Workshop on Usable Verification, November 2010. [PDF]
  • Jocelyn Simmonds. Dynamic Analysis of Web Services. Ph.D. Thesis, University of Toronto, 2010. [PDF]
  • F. van Breugel, M. Chechik, "19th International Conference on Concurrency Theory: Selection of Best Papers". Journal of Information and Computation, 208(10), pp. 1091-1092, 2010.
  • J. Simmonds, J. Davies, A. Gurfinkel, M. Chechik. "Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC". Journal version of the FMCAD'07 paper. Springer International Journal of Software Tools for Technology Transfer (STTT), Volume 12, Number 5, pp. 319-335, January 2010. [PDF]
  • Michail Famelis. Relationship-Driven Model Management, Masters Thesis, April 2010. [PDF]
  • Aws Albarghouthi, Abstract Analysis of Symbolic Executions, Masters Thesis, January 2010. [PDF]
  • J. Simmonds, S. Ben-David, M. Chechik. "Monitoring and Recovery of Web Service Applications". Book chapter in Smart Internet Technologies, J. Cordy, M. Chignell, J. Ng, eds., April 2010. 40 pages. [PDF]
  • J. Simmonds, S. Ben-David, M. Chechik. "Guided Recovery for Web Service Applications". 15 pages. In Proceedings of Foundations of Software Engineering (FSE'10), November 2010. [PDF]
  • A. Albarghouthi, A. Gurfinkel, O. Wei, M. Chechik. "Abstract Analysis of Symbolic Executions". In Proceedings of International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Volume 6174, pages 495-510, July 2010. Springer. [PDF]
  • J. Simmonds, M. Chechik. "RUMOR: Monitoring and Recovery of BPEL Applications". In Proceedings of International Conference on Automated Software Engineering, September 2010, pages 345-346. Tools paper. [PDF]
  • J. Simmonds, S. Ben-David, M. Chechik. "Optimizing Computation of Recovery Plans for BPEL Applications". In Proceedings of ASE'10 Workshop on Testing and Verification of Web Systems, EPTCS Volume 35, pp. 3-14, September 2010. [PDF]
  • M. Sabetzadeh, S. Nejati, M. Chechik, and S. Easterbrook. "Reasoning about Consistency in Model Merging". In Proceedings of 3rd Workshop on Living With Inconsistency in Software Development, 6 pages, September 2010. [PDF]
  • J. Rubin, M. Chechik. "From Products to Product Lines Using Model Matching and Refactoring". In Proceedings of 2nd International Workshop on Model-Driven Software Product Line Engineering (MAPLE'2010), 6 pages, September 2010. [PDF]

2009

  • Ou Wei. Abstraction for Verification and Refutation in Model Checking. Ph.D. Thesis, University of Toronto, 2009. [PDF]
  • Mihaela Bobaru (Gheorghiu). Approximation and Refinement Techniques for Hard Model-Checking Problems. Ph. D. Thesis, University of Toronto, 2009. [PDF]
  • with F. Torshizi, J. Ostroff, R. Paige. "The SCOOP Concurrency Model in Java-like Languages". In Proceedings of CPA'09, November 2009, pages 7-27 [PDF]
  • Winnie Lai. Relationship-Based Change Propagation: A Case Study . M.Sc. thesis, University of Toronto, April 2009. [PDF]
  • with J. Simmonds, Y. Gan, S. Nejati, B. O'Farrell, E. Litani, J. Waterhouse. "Runtime Monitoring of Web Service Conversations". In IEEE Transactions on Service Computing, 2(3), pages 223-244, 2009. [PDF]
  • with W. Lai, S. Nejati, J. Cabot, Z. Diskin, S. Easterbrook, M. Sabetzadeh, R. Salay. "Relationship-Based Change Propagation: A Case Study". In Proceedings of ICSE'09 Workshop on Modeling in Software Engineering (MiSE'09), May 2009. [PDF]
  • with Ou Wei and Arie Gurfinkel. "Mixed Transition Systems Revisited". In Proceedings of VMCAI'09, January 2009, 13 pages. [PDF].
  • with Sebastian Uchitel and Greg Brunet. "Behavioural Model Synthesis from Properties and Scenarios". IEEE Transactions on Software Engineering, 35(3), pages 384-406, 2009. [PDF]
  • T. Hart, K. Ku, A. Gurfinkel, M. Chechik, D. Lie. "Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates".
  • M. Chechik. "How Smart are Your Services (Reasoning about Correctness of Web Services)", in Proceedings of CAS/NSERC Strategic Workshop on Smart Internet Technologies, November 2009. [PDF]
  • M. Chechik. "A relationship-based approach to model management". In Proceedings of MOMPES'09, p. 1 (invited) [PDF]

2008

  • Shiva Nejati. Behavioural Model Fusion. Ph.D. thesis, University of Toronto, September 2008. [PDF]
  • with Arie Gurfinkel and Ou Wei. "Model Checking Reachability and Non-Termination of Recursive Programs". In Proceedings of 6th International Symposium on Automated Technology for Verification (ATVA'08) October 2008. [PDF]
  • with Tom Hart and David Lie. "Security Benchmarking using Partial Verification". In Proceedings of 3rd USENIX Workshop on Hot Topics in Security (HotSec'08), July 2008. 6 pages.
  • with Tom Hart, Kelvin Ku, David Lie, Arie Gurfinkel. "Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates". In Proceedings of International Conference on Automated Software Engineering (ASE'08) (short paper), September 2008. 4 pages. [PDF]
  • with N. D'Ippolito, D. Fishbein and S. Uchitel. "MTSA: The Modal Transition System Analyzer.", 2 pages. In Proceedings of International Conference on Automated Software Engineering (ASE'08), September 2008. Tools paper. [PDF]
  • with T. Hart, K. Ku, A. Gurfinkel and D. Lie. "PTYasm: Software Model Checking with Proof Templates", 2 pages. In Proceedings of International Conference on Automated Software Engineering (ASE'08), September 2008. Tools paper. [PDF]
  • Kelvin Ku. "Software Model-Checking: Benchmarking and Techniques for Buffer Overflow Analysis". University of Toronto M.Sc. thesis, January 2008. [PDF]
  • with S. Nejati, M. Sabetzadeh, S. Uchitel and P. Zave. "Towards Compositional Synthesis of Evolving Systems". In Proceedings of FSE'08, November 2008, 11 pages. [PDF]
  • with Shiva Nejati. "Behavioural Model Fusion: Experiences from Two Telecommunication Case Studies". In Proceedings of ICSE'08 Workshop on Modeling in Software Engineering (MiSE'08), May 2008. [PDF]
  • with Julia Rubin and Steve Easterbrook. "A Declarative Approach for Model Composition". In Proceedings of ICSE'08 Workshop on Modeling in Software Engineering (MiSE'08), May 2008. [PDF]
  • with Jocelyn Simmonds and Shiva Nejati. "Property Patterns for Runtime Monitoring of Web Service Conversations", 18 pages. In Proceedings of Runtime Verification, March 2008 [PDF].
  • with M. Sabetzadeh, S. Nejati, S. Easterbrook. "Global Consistency Checking of Distributed Models with TreMer+". Formal demo. In Proceedings of ICSE'08, May 2008. 4 pages. [PDF]

2007

  • with R. Salay, S. Easterbrook, Z. Diskin, S. Nejati, M. Sabetzadeh, P. McCormick, P. Viriyakattiyaporn. "An Eclipse-Based Model Management Framework". In Proceedings of OOPSLA'07 Workshop on Eclipse Technology, November 2007. 6 pages [PDF].
  • Yuan Gan. "Runtime Monitoring of Web Service Conversations". M.Sc. thesis, University of Toronto, March 2007. [PDF]
  • with Kevin Ku, Tom Hart, David Lie. "A Buffer Overflow Benchmark For Software Model Checkers". In Proceedings of ASE'07. November 2007. [PDF]
  • with Yuan Gan, Shiva Nejati, Jon Bennett, Bill O'Farrell, Julie Waterhouse. "Runtime Monitoring of Web Service Compositions". In Proceedings of CASCON'07, November 2007. 16 pages. [PDF] Winner of Best Student Paper Award.
  • with Mehrdad Sabetzadeh, Shiva Nejati, Sotirios Liaskos and Steve Easterbrook. "Consistency Checking of Conceptual Models via Model Merging". In Proceedings of IEEE International Conference on Requirements Engineering (RE'07), October 2007, 15 pages. [PDF]
  • with Arie Gurfinkel. "A Framework for Counterexample Generation and Exploration" (journal version of FASE'05 paper). In Software Tools for Technology Transfer (STTT), Vol. 9, No. 5-6, pp. 429-445, October 2007. [postscript]
  • with Mihaela Gheorghiu and Arie Gurfinkel. "Finding State Solutions to Temporal Queries". In Proceedings of Integrated Formal Methods (IFM'07), July 2007. LNCS 4591, pp. 273-292. [PDF]
  • with Shiva Nejati, Mehrdad Sabetzadeh and Steve Easterbrook. "A Relationship-Driven Approach to Model Merging". In Proceedings of ICSE 2007 Workshop on Models in Software Engineering (MiSE'07), May 2007. [PDF]
  • with Sebastian Uchitel, Greg Brunet and Dario Fischbain. "Partial Behavioural Models for Requirements and Early Design". In Proceedings of 2006 Dagstuhl Seminar on Methods for Modelling Software Systems (MMOSS), LNCS, 2007. [PDF].
  • with Mihaela Gheorghiu and Arie Gurfinkel. "Finding Environmental Guarantees". In Proceedings of FASE'07, LNCS 4422, March-April 2007. [abstract] [PDF].
  • with Shiva Nejati, Mehrdad Sabetzadeh, Steve Easterbrook and Pamela Zave. "Matching and Merging of Statecharts Specifications". In Proceedings of ICSE'07, May 2007. [pdf] Winner of Distinguished Paper Award
  • with Sebastian Uchitel and Greg Brunet. "Behaviour Model Synthesis From Properties and Scenarios". In Proceedings of ICSE'07, May 2007. [pdf]

2006

  • with Merhrad Sabetzadeh, Shiva Nejati and Steve Easterbrook. "A Relationship-Driven Approach to View Merging", in Posters track, SIGSOFT FSE'06, 3 pages, November 2006.
  • with Mihaela Gheorghiu and Arie Gurfinkel. "VaqUoT: A Tool for Vacuity Detection", in Tools and Posters track of Formal Methods 2006, 4 pages, August 2006. [PDF]
  • with Mihaela Gheorghiu and Arie Gurfinkel. "TLQ: A Query Solver for States", in Tools and Posters track of Formal Methods 2006, 4 pages, August 2006. [PDF]
  • with Jocelyn Simmonds, Jessica Davies and Arie Gurfinkel. "VaqTree: Efficient Vacuity Detection for Bounded Model Checking", in Tools and Posters track of Formal Methods 2006, 4 pages, August 2006. [PDF]
  • with Mehrdad Sabetzadeh, Shiva Nejati, and Steve Easterbrook. "TReMer: A Tool for Relationship-Driven Model Merging". in Tools and Posters track of Formal Methods 2006, 3 pages, August 2006. [PDF]
  • with Shiva Nejati, Mehrdad Sabetzadeh, Steve Easterbrook. "Identifying and Representing Requirements Variability in Families of Reactive Software". CS Technical Report, February 2006.
  • with Greg Brunet and Sebastian Uchitel. "Generating Unbiased Models from Temporal Properties". CS Technical Report, April 2006.
  • with Greg Brunet and Sebastian Uchitel. "Properties of Behavioural Model Merging", in Proceedings of Formal Methods (FM'06), LNCS 4085, pp. 98-114, August 2006. [abstract] [PDF].
  • with Arie Gurfinkel, Benet Devereux, Albert Lai and Steve Easterbrook, "Data Structures for Symbolic Multi-Valued Model-Checking", Formal Methods in Software Design, 29(3), pp. 295-344.. [abstract] [PDF],
  • with Greg Brunet, Steve Easterbrook, Shiva Nejati, Nan Niu and Marhdad Sabetzadeh. "A Manifesto for Model Merging", in 1st International Workshop on Global Integrated Model Management (ICSE'06 workshop), May 2006 [postscript].
  • with Shiva Nejati and Mihaela Gheorghiu. "Thorough Checking Revisited". In Proceedings of Formal Methods in Computer Aided Design (FMCAD'06), November 2006. [abstract] [PDF]
  • with Arie Gurfinkel and Ou Wei. "Yasm: A Software Model-Checker for Verification and Refutation", in Proceedings of CAV'06, LNCS 4144, pp. 170-174, August 2006. [postscript]
  • with Arie Gurfinkel and Ou Wei. "Systematic Construction of Abstractions for Model-Checking". In Proceedings of VMCAI'06, LNCS 3855, pp. 381-397, January 2006. [abstract] [PDF]
  • with Benet Devereux. "Automated Support for Building Behavioural Models of Event-Driven Systems", in Proceedings of FASE'06, LNCS 3922, pp. 122-138, April 2006. [postscript]
  • with Arie Gurfinkel. "Why Waste a Perfectly Good Abstraction?", in Proceedings of TACAS'06, LNCS 3920, pp. 212-226, April 2006. [postscript]
  • Greg Brunet. A Characterization of Merging Partial Behavioural Models. MS Thesis, University of Toronto, February 2006.

2005

  • with Arie Gurfinkel. "A Framework for Counterexample Generation and Exploration", LNCS 3442, pp. 217-233, Proceedings of FASE'05, Edinburgh, UK, April 2005. [abstract] [postscript]
  • with Arie Gurfinkel. "How Thorough is Thorough Enough". In CHARME 2005, October 2005. [abstract] [postscript]
  • with Shiva Nejati and Arie Gurfinkel. "Stuttering Abstraction for Model Checking", in Software Engineering and Formal Methods (SEFM'05), September 2005. [abstract] [postscript]
  • with Ou Wei and Arie Gurfinkel. "Identification and Counter Abstraction for Full Virtual Symmetry", in CHARME'05, October 2005. [abstract] [postscript]
  • with Shiva Nejati. "Let's Agree to Disagree". In Proceedings of Automated Software Engineering, November 2005. [abstract] [postscript] [full version].
  • with Arie Gurfinkel. "Model-Checking Software Using Precise Abstractions", in IFIP WC on Verified Software: Tools, Techniques, and Experiments, October 2005. [postscript]

2004

  • Benet Devereux and Arie Gurfinkel. "Irrelevance and Vacuity in SAT-Based Model-Checking". University of Toronto Technical Report. May 2004. [ps]
  • with Benet Devereux, Arie Gurfinkel and Steve Easterbrook, "Multi-Valued Symbolic Model-Checking". ACM Transactions on Software Engineering and Methodology, Vol. 12, No. 4, October 2003, pages 1-38. [abstract] [PDF].
  • with Sergey Berezin, Clark Barrett, Igor Shikanian, Arie Gurfinkel and David Dill. "Logic with Partial Functions in CVC Lite", in Proceedings of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, July 2004. [abstract] [postscript].
  • with Sebastian Uchitel. "Merging Partial Behavioural Models", in Proceedings of FSE'04, November 2004. [abstract] [postscript].
  • with Arie Gurfinkel. "Extending Extended Vacuity", in Proceedings of FMCAD'04, LNCS 3312, November 2004. [abstract] [postscript]
  • with Arie Gurfinkel. "How Vacuous is Vacuous?", in Proceedings of TACAS'04, March 2004, LNCS Vol. 2988, pp. 451-466, Springer. [abstract] [postscript].

2003

  • Shiva Nejati. "Refinement Relations on Partial Specifications", University of Toronto MS. Thesis, June 2003.
  • with Arie Gurfinkel, "Proof-Like Counter-Examples", in Proceedings of TACAS'03, LNCS 2619, pp. 160-175, April 2003, Springer. [abstract] [postscript]
  • with Arie Gurfinkel, "Multi-Valued Model Checking via Classical Model Checking". In Proceedings of CONCUR'03 , LNCS 2761, September 2003. [abstract] [postscript]
  • with Arie Gurfinkel, "Generating Counterexamples for Multi-Valued Model-Checking". In Proceedings of Formal Methods Europe (FME'03), LNCS 2805, September 2003. [abstract] [postscript]
  • with Arie Gurfinkel and Benet Devereux. "Temporal Logic Query Checking: A Tool for Model Exploration". March 2003, updated July 2003. IEEE Transactions on Software Engineering, Vol. 29, No. 10, pp. 898-914, October 2003. [abstract] [postscript]
  • with Steve Easterbook, Benet Devereux, Arie Gurfinkel, Albert Lai, Chrostopher Thompson-Walsh, Anya Tefliovich, Victor Petrovykh. "XChek: A Model-Checker for Multi-Valued Reasoning". In Proceedings of ICSE'03, May 2003. [PDF-Long] [PDF-Short]
  • with Dimitrie Paun, "On Closure Under Stuttering", Formal Aspects of Computing, volume 14, pp. 342-368, 2003.[abstract] [postscript] Also available as CSRG Technical Report 394.
  • with Benet Devereux, "Edge-Shifted Decision Diagrams for Multiple-Valued Logic", in Journal of Multi-Valued Logic and Soft Computing, vol. 9, no. 1, pp. 59-86, Old City Publishing Inc., 2003. [abstract] [postscript]. Also available as CSRG Technical Report 444.
  • with Arie Gurfinkel, "TLQSolver: A Temporal Logic Query Checker". In Proceedings of 15th International Conference on Computer Aided Verification (CAV'03), LNCS 2725, pp. 210-214, July 2003. [postscript].
  • with Wendy MacCaull, "CTL Model-Checking Over Logics with Non-Classical Negations". In Proceedings of 33rd IEEE International Conference on Multi-Valued Logics (ISMVL'03), May 2003, pp. 293-300. [abstract] [postscript]

2002

  • Arie Gurfinkel. Multi-Valued Symbolic Model-Checking: Fairness, Counterexamples, Running Time. University of Toronto MS Thesis, 2002. [postscript]
  • with Steve Easterbrook, "Guest Editorial: Special Issue on Model Checking in Requirements Engineering". In Requirements Engineering, Volume 7, issue 4, pp. 221-224, 2002. Springer-Verlag. [PDF].
  • with Arie Gurfinkel and Benet Devereux, "Model Exploration with Temporal Logic Query Checking", in Proceedings of SIGSOFT Conference on Foundations of Software Engineering (FSE'02), November 2002, pp. 139-148. [abstract] [postscript] Also available as CSRG Technical Report 445.
  • with Andre Wong, "Formal Modeling in a Commercial Setting: A Case Study", Journal of Systems and Software, 60(1), pp. 57-80, January 2002. Also available as CSRG Technical Report 392. [abstract][postscript]
  • with Benet Devereux and Arie Gurfinkel, "XChek: A Multi-Valued Model-Checker", in Proceedings of Computer-Aided Verification (CAV'02), pp. 505-509, July 2002. [postscript] Also available as CSRG Technical Report 447.
  • with Wei Ding, "Lightweight Reasoning About Program Correctness". Information Systems Frontiers, vol. 4, no. 4, November 2002, pp. 363-377. (extended version of CASCON'01 paper). [abstract] [postscript].

2001

  • with Wei Ding, "Lightweight Reasoning About Program Correctness", in Proceedings of CASCON'01, November 2001. Also available as CSRG Technical Report 396. [abstract] [postscript]
  • with Benet Devereux, Albert Lai, Steve Easterbrook and Victor Petrovykh, "Efficient Multiple-Valued Model-Checking Using Lattice Representations", in Proceedings of CONCUR'01, August 2001. [abstract] [postscript] [extended version]. Also available as CSRG Technical Report 429.
  • with Steve Easterbrook, "Automated Paraconsistent Reasoning via Model Checking", in Proceedings of IJCAI Inconsistency Workshop, August 2001, 8 pages. [abstract] [postscript] Also available as CSRG Technical Report 428.
  • with J. Gannon, "Automatic Analysis of Consistency Between Requirements and Designs", IEEE Transactions in Software Engineering, volume 27, number 7, July 2001. [abstract] [PDF] Also available as CSRG technical Report 388.
  • with Steve Easterbrook, "Reasoning About Compositions of Concerns", position paper in Proceedings of ICSE Workshop on Advanced Separation of Concerns, May 2001, 5 pages. [abstract] [postscript] Also available as CRSG Technical Report 427.
  • with Steve Easterbrook, "A Framework to Handle Horizontal Inconsistency in Software", position paper in Proceedings of ICSE Workshop of Living with Inconsistency, May 2001, 3 pages. [abstract] [postscript].
  • with Kenneth Cheung, Yilan Gu, Arie Gurfinkel, Jiang Liu, Wendy Liu, Wei Tjioe, Hung Tran, Clement Yuen, "Automated Verification, Fall 2000: A Collection of Reports", March 2001, available as a CSRG Technical Report 425. [summary]
  • with Benet Devereux and Arie Gurfinkel, "Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN", in Proceedings of SPIN Workshop on Model-Checking Software, May 2001, 18 pages. [abstract] [postscript]. Also available as CRSG Technical Report 426.
  • with Steve Easterbrook and Benet Devereux, "Model Checking with Multi-Valued Temporal Logics", in Proceedings of International Symposium on Multi-Valued Logics (ISMVL'01), May 2001, 6 pages. [abstract] [PDF]. Also available as CSRG Technical Report 430.
  • with Benet Devereux and Steve Easterbrook, "Implementing a Multi-Valued Symbolic Model Checker", in Proceedings of TACAS'01, April 2001, 17 pages. [abstract] [postscript]. Also available as CSRG Technical Report 431.
  • with Steve Easterbrook, "A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints", in Proceedings of International Conference on Software Engineering (ICSE'01), May 2001, 11 pages. [abstract] [postscript]. Also available as CSRG Technical Report 419.
  • with Steve Easterbrook and Victor Petrovykh, "Model-Checking over Multi-Valued Logics", in Proceedings of Formal Methods Europe (FME'01), March 2001. 26 pages. [abstract] [postscript]. Also available as CSRG Technical Report 420.

2000

  • with William Andrepoulos, Bob Bernecky, Ariel Fuxman, Benet Devereux, Kristin Hofstee, Jingjing Lu, Tsuyoshi Morioka, Peeter Piegaze, Jeffrey Tang, Sean Thompson, Cosmin Truta, Yuxiang Zhu, Wei Zhou, "Automated Verification, Fall 1999: A Collection of Reports", March 2000, available as CSRG Technical Report 407. [summary]
  • with Hai Wang, "Feasibility of Bisimulation Analysis of Protocols Expressed in SDL", in Proceedings of CASCON'2000, pages 65-77, November 2000. Also available as CSRG Technical Report 382. [abstract] [postscript]

1999

  • with Ma Chuan, Veronika Cwir, Ken Pu, Su Rong, Yuwei Wang, "Automated Verification, Spring 1999: A Collection of Reports", June 1999, available as CSRG Technical Report 380. [summary]
  • with Dimi Paun, "Events in Property Patterns", in Theoretical and Practical Aspects of SPIN Model Checking, LNCS 1680, pp. 154-167, September 1999. [abstract] [postscript]. Also available as CSRG Technical Report 381.
  • with Andre Wong, "Formal Methods When Money Is Tight", position paper, in Proceedings of the 1st Workshop on Economics-Driven Software Engineering Research (EDSER-1), May 1999. [postscript] Also available as CSRG Technical Report 383.
  • with Andre Wong, "Formal Modeling in a Commercial Setting: A Case Study", Proceedings of World Congress in Formal Methods (FM'99), September 1999. [abstract] [postscript] Also available as CSRG Technical Report 385.
  • with Dimi Paun, "Events in Linear-Time Properties", in Proceedings of Requirements Engineering, June 1999. [abstract] [postscript] Also available as CSRG Technical Report 384.

1998

  • "Using SCR Requirements", position paper, in Proceedings of the 7th SCR workshop, October 1998. [postscript]
  • with Andre Wong, "Applying Formal Methods to a Telecommunications System in a Commercial Setting", position paper, in Proceedings of 11th International Conference on Software Engineering and Its Applications, December 1998. [abstract] [postscript] Also available as CSRG Technical Report 377.
  • "SC(R)3 - Towards Usability of Formal Methods", in Proceedings of CASCON, November 1998. [abstract] [postscript] Also available as CSRG Technical Report 386.
  • with Dimi Paun and Bernd Biechele, "Production Cell Revisited", in Proceedings of SPIN'98, November 1998. [abstract] [postscript] Also available as CSRG Technical Report 387.
  • with students of csc2108, Fall'97, "Automated Verification: A Collection of Reports", CSRG Technical Report 374, Department of Computer Science, University of Toronto, April, 1998. [summary]

1997

  • with S. Vallurupalli, "Checking Consistency Between Source Code and Annotations", CSRG technical report 373, University of Toronto, December 1997. [abstract]
  • Software Engineering Education at the University of Toronto, a position paper in Proceedings of the 4th Software Engineering Workshop, May 1997.

1996

  • Automatic Analysis of Consistency between Requirements and Designs, Ph.D. Thesis, University of Maryland, College Park, December 1996. [abstract] [postscript]
  • with J. Gannon, "Verification of Consistency Between Concurrent Program Designs and Their Requirements", in Proceedings of Symposium on Computer Assurance (COMPASS'96), Gathersburg, MD, June 1996. [abstract] [postscript]
  • with J. Atlee and J. Gannon, "Using Model Checking to Analyze Requirements and Designs", in Advances in Computers, Volume 43, Marv Zelkowitz, ed. Academic Press, 1996. [abstract] [postscript]

1995

  • with J. Gannon, "Automatic Analysis of Consistency Between Implementations and Requirements: A Case Study", in Proceedings of Symposium on Computer Assurance (COMPASS'95), pp. 123-132, Gathersburg, MD, June 1995. [abstract] [postscript]

1994

  • with J. Gannon, "Automatic Verification of Requirements Implementation", in Proceedings of International Symposium on Testing and Analysis (ISSTA'94), pp. 1-15, Seattle, August 1994. [abstract] [postscript]